$%\usepackage{color}$

$%\usepackage{tcolorbox}$

$%\tcbuselibrary{skins}$

$\usepackage{pifont}$

$\definecolor{fakeaaltobluel}{RGB}{00,141,229} % 0065BD$

$\definecolor{aaltoblue}{RGB}{00,101,189} % 0065BD$

$\definecolor{aaltored}{RGB}{237,41,57} % ED2939$

$\definecolor{MyBoxBackground}{rgb}{0.98,0.98,1.0}$

$\definecolor{MyBoxBorder}{rgb}{0.90,0.90,1.0}$

$\definecolor{backgroundred}{rgb}{1.0,0.98,0.98}$

$\definecolor{shadowred}{rgb}{1.0,0.90,0.90}$

$%\newcommand{\subheading}[1]{\textbf{\large\color{fakeaaltobluel}#1}}$

$\newcommand{\subheading}[1]{\large{\usebeamercolor[fg]{frametitle} #1}}$

$%\newtcbox{\mybox}[1][red]{on line,arc=0pt,outer arc=0pt,colback=#1!10!white,colframe=#1!50!black,boxsep=0pt,left=1pt,right=1pt,top=2pt,bottom=2pt,boxrule=0pt,bottomrule=1pt,toprule=1pt}$

$%\newtcbox{\mybox}[1][MyBoxBackground]{on line,arc=0pt,outer arc=0pt,colback=#1!10!white,colframe=#1!50!black,boxsep=0pt,left=1pt,right=1pt,top=2pt,bottom=2pt,boxrule=0pt,bottomrule=1pt,toprule=1pt}$

$\newtcolorbox{MyBoxTitled}[1]{colback=MyBoxBackground!100!black,colframe=MyBoxBorder!100!black,boxsep=2pt,left=0pt,right=0pt,top=2pt,bottom=0pt,%enhanced,%\) \( coltitle=red!25!black,title=#1,boxrule=1pt}$

$\newtcolorbox{MyBox}[1][]{colback=MyBoxBackground!100!black,colframe=MyBoxBorder!100!black,boxsep=0pt,left=2pt,right=0pt,top=0pt,bottom=0pt,%enhanced,%\) \( coltitle=red!25!black,boxrule=1pt,#1}$

$\newenvironment{EqnBox}[1]{\begin{adjustbox}{valign=t}\begin{minipage}{#1}\begin{MyBox}[colback=backgroundred!100!black,colframe=shadowred!100!black]}{\end{MyBox}\end{minipage}\end{adjustbox}}$

$\newenvironment{topbox}[1]{\begin{adjustbox}{valign=t}\begin{minipage}{#1}}{\end{minipage}\end{adjustbox}}$

$\newcommand{\Blue}[1]{{\color{aaltoblue}#1}}$

$\newcommand{\Red}[1]{{\color{aaltored}#1}}$

$%\newcommand{\Emph}[1]{\emph{\color{aaltoblue}#1}}$

$\newcommand{\Emph}[1]{\emph{\usebeamercolor[fg]{structure} #1}}$

$\newcommand{\TextDef}[1]{{\bf\usebeamercolor[fg]{structure} #1}}$

$\newcommand{\todo}[1]{\textbf{\Red{\Pointer #1}}}$

$\newcommand{\TODO}[1]{\todo{#1}}$

$\newcommand{\Pointer}{\raisebox{-1ex}{\huge\ding{43}}\ }$

$%$

$% Common math definitions$

$%$

$\newcommand{\Set}[1]{\{#1\}}$

$\newcommand{\Setdef}[2]{\{{#1}\mid{#2}\}}$

$\newcommand{\PSet}[1]{\mathcal{P}(#1)}$

$\newcommand{\Pair}[2]{(#1,#2)}$

$\newcommand{\Card}[1]{{\vert{#1}\vert}}$

$\newcommand{\Tuple}[1]{(#1)}$

$\newcommand{\Seq}[1]{[#1]}$

$\newcommand{\bbZ}{\mathbb{Z}}$

$\newcommand{\Ints}{\mathbb{Z}}$

$\newcommand{\Reals}{\mathbb{R}}$

$\newcommand{\bbQ}{\mathbb{Q}}$

$\newcommand{\Rats}{\bbQ}$

$\newcommand{\bbN}{\mathbb{N}}$

$\newcommand{\Nats}{\bbN}$

$\newcommand{\Floor}[1]{\lfloor #1 \rfloor}$

$\newcommand{\Ceil}[1]{\lceil #1 \rceil}$

$\newcommand{\False}{\textsf{F}}$

$\newcommand{\True}{\textsf{T}}$

$\newcommand{\Implies}{\rightarrow}$

$\newcommand{\Iff}{\leftrightarrow}$

$%\newcommand{\Implies}{\Rightarrow}$

$%\newcommand{\Iff}{\Leftrightarrow}$

$\newcommand{\Xor}{\oplus}$

$\newcommand{\Equiv}{\equiv}$

$\newcommand{\Oh}[1]{O(#1)}$

$%\newcommand{\Theta}[1]{\Theta(#1)}$

$\newcommand{\PHP}[2]{\mathrm{php}_{#1,#2}}$

$\newcommand{\PH}[2]{\mathit{x}_{#1,#2}}$

$\newcommand{\NP}{\textbf{NP}}$

$\newcommand{\coNP}{\textbf{co-NP}}$

$\newcommand{\bnfdef}{\mathrel{\textup{::=}}}$

$\newcommand{\bnfor}{\mathrel{\mid}}$

$\newcommand{\Def}{\mathrel{:=}}$

$\newcommand{\LSF}{\alpha}$

$\newcommand{\RSF}{\beta}$

$\newcommand{\SF}{\phi}$

$\newcommand{\MF}{\gamma}$

$%\newcommand{\Abbrv}{\equiv}$

$\newcommand{\Abbrv}{\Def}$

$\newcommand{\AbbrvEq}{\equiv}$

$\newcommand{\Exists}[2]{\exists{#1}.\,#2}$

$%\newcommand{\E}[3]{\exists{#1{:}#2}.\,#3}$

$\newcommand{\E}[3]{\exists{#1{:}\,#3}}$

$\newcommand{\Forall}[2]{\forall{#1}.\,#2}$

$%\newcommand{\Furall}[3]{\forall{#1{:}#2}.\,#3}$

$%\newcommand{\A}[3]{\forall{#1{:}#2}.\,#3}$

$\newcommand{\A}[3]{\forall{#1{:}\,#3}}$

$\newcommand{\Models}{\models}$

$\newcommand{\NotModels}{\not\models}$

$\newcommand{\Substf}[3]{#1[#2 \mapsto #3]}$

$\newcommand{\Functions}[2]{[#1 \to #2]}$

$\newcommand{\Eq}{\approx}$

$\newcommand{\EqS}[1]{\approx_{#1}}$

$\newcommand{\Neq}{\not\approx}$

$%\newcommand{\Th}{\mathcal{T}}$

$\newcommand{\Th}{T}$

$\newcommand{\ThI}[1]{\Th_{#1}}$

$\newcommand{\Sig}{\Sigma}$

$\newcommand{\SigI}[1]{\Sigma_{#1}}$

$\newcommand{\Interp}{I}$

$%\newcommand{\Interp}{{\mathcal{I}}}$

$\newcommand{\InterpOf}[1]{#1^\Interp}$

$\newcommand{\InterpIOf}[2]{#2^{#1}}$

$\newcommand{\InterpRestr}[1]{\Interp^{#1}}$

$\newcommand{\InterpI}[1]{I_{#1}}$

$%\newcommand{\InterpI}[1]{{\mathcal{I}_{#1}}}$

$%\newcommand{\InterpIOf}[2]{#2^{\InterpI{#1}}}$

$\newcommand{\InterpDom}{D_{\Interp}}$

$\newcommand{\InterpSubst}[2]{\Interp[{#1}\mapsto{#2}]}$

$\newcommand{\ThModels}{\mathrel{\models_{\Th}}}$

$\newcommand{\ThIModels}[1]{\mathrel{\models_{\ThI{#1}}}}$

$% Example interpretations$

$\newcommand{\IInts}{\InterpI{\textrm{ints}}}$

$\newcommand{\IIntsOf}[1]{\InterpIOf{\IInts}{#1}}$

$\newcommand{\IMods}{\InterpI{\textrm{mod7}}}$

$\newcommand{\IModsOf}[1]{\InterpIOf{\IMods}{#1}}$

$\newcommand{\ISilly}{\InterpI{\textrm{silly}}}$

$\newcommand{\ISillyOf}[1]{\InterpIOf{\ISilly}{#1}}$

$%\newcommand{\El}[1]{\textup{e}_{#1}}$

$\newcommand{\ElemI}{\textup{\ding{40}}}$

$\newcommand{\ElemII}{\textup{\ding{41}}}$

$\newcommand{\ElemIII}{\textup{\ding{46}}}$

$\newcommand{\ElemA}{\circ}$

$\newcommand{\ElemB}{\bullet}$

$\newcommand{\AxiomMarg}[1]{\makebox{}\hfill(\Blue{#1})}$

$\newcommand{\Comment}[1]{\makebox{}\hfill\Blue{#1}}$

$\newcommand{\DLZ}{\mathit{DL}(\bbZ)}$

$\newcommand{\DLQ}{\mathit{DL}(\bbQ)}$

$\newcommand{\EUF}{\mathit{EUF}}$

$\newcommand{\TEUF}{\ThI{\mathit{EUF}}}$

$\newcommand{\LIA}{\mathit{LIA}}$

$\newcommand{\TLIA}{\ThI{\mathit{LIA}}}$

$\newcommand{\TNRA}{\ThI{\mathit{NRA}}}$

$\newcommand{\TNIA}{\ThI{\mathit{NIA}}}$

$\newcommand{\LRA}{\mathit{LRA}}$

$\newcommand{\TLRA}{\ThI{\mathit{LRA}}}$

$\newcommand{\IDL}{\mathit{IDL}}$

$\newcommand{\RDL}{\mathit{RDL}}$

$\newcommand{\EUFModels}{\mathrel{\models_{\TEUF}}}$

$\newcommand{\EUFModelsNot}{\mathrel{{\not\models}_{\TEUF}}}$

$\newcommand{\LIAModels}{\mathrel{\models_{\LIA}}}$

$\newcommand{\LIANotModels}{\mathrel{\not\models_{\LIA}}}$

$\newcommand{\LIAEntails}{\mathrel{\models_{\LIA}}}$

$\newcommand{\IDLEntails}{\mathrel{\models_{\IDL}}}$

$\newcommand{\NIAModels}{\mathrel{\models_{\TNIA}}}$

$\newcommand{\Div}[2]{{{#1}\mid{#2}}}$

$\newcommand{\Sort}{s}$

$\newcommand{\SortI}[1]{s_{#1}}$

$\newcommand{\Sorts}{S}$

$\newcommand{\Func}{f}$

$\newcommand{\Funcs}{F}$

$\newcommand{\Pred}{p}$

$\newcommand{\Preds}{P}$

$\newcommand{\SortName}[1]{\textsf{#1}}$

$\newcommand{\Var}{x}$

$\newcommand{\Vars}{X}$

$\newcommand{\BVar}{a}$

$\newcommand{\BVars}{\mathcal{B}}$

$\newcommand{\Val}{v}$

$\newcommand{\DomOf}[1]{D_{#1}}$

$\newcommand{\Term}{t}$

$\newcommand{\TermI}[1]{t_{#1}}$

$\newcommand{\TermP}[1]{t'}$

$\newcommand{\Atom}{A}$

$%$

$% EUF$

$%$

$\newcommand{\UFEq}{\equiv}$

$\newcommand{\UFEqP}{\mathrel{\equiv'}}$

$\newcommand{\UFEqNot}{\not\equiv}$

$\newcommand{\UFNeq}{\not\equiv}$

$%$

$% Arithmetics$

$%$

$\newcommand{\IntsSort}{\textrm{Int}}$

$\newcommand{\IntsSig}{\SigI{\textrm{Int}}}$

$\newcommand{\RealsSort}{\textrm{Real}}$

$\newcommand{\Mul}{\mathbin{*}}$

$%$

$% Arrays$

$%$

$\newcommand{\IndexSort}{\SortName{idx}}$

$%\newcommand{\IndexSort}{\SortName{index}}$

$\newcommand{\ElemSort}{\SortName{elem}}$

$%\newcommand{\ArraySort}{\SortName{array}}$

$\newcommand{\ArraySort}{\SortName{arr}}$

$\newcommand{\ArrSig}{\Sigma_{\mathit{arrays}}}$

$\newcommand{\ArrE}[1]{\textrm{a}_{#1}}$

$\newcommand{\TArrays}{\ThI{\mathit{arrays}}}$

$\newcommand{\TArraysExt}{\ThI{\mathit{arrays}}^{=}}$

$\newcommand{\ArrModels}{\mathrel{{\models_\mathit{arrays}}}}$

$%$

$% Theories of Lisp-like lists$

$%$

$\newcommand{\ThCons}{\ThI{\textrm{cons}}}$

$\newcommand{\ThConsAcyclic}{\ThI{\textrm{cons+}}}$

$\newcommand{\SigCons}{\SigI{\textrm{cons}}}$

$\newcommand{\Cons}{\FuncName{cons}}$

$\newcommand{\Car}{\FuncName{car}}$

$\newcommand{\Cdr}{\FuncName{cdr}}$

$\newcommand{\LAtom}{\PredName{atom}}$

$% Sorted version additions$

$\newcommand{\ListSort}{\SortName{list}}$

$\newcommand{\Nil}{\FuncName{nil}}$

$\newcommand{\Length}{\FuncName{length}}$

$\newcommand{\BVT}{\ThI{\mathsf{BV}}}$

$\newcommand{\BVSig}{\SigI{\mathsf{BV}}}$

$\newcommand{\BVS}[1]{\SortName{[}#1\SortName{]}}$

$%\newcommand{\BVS}[1]{[{#1}]}$

$\newcommand{\BVAdd}[1]{\mathbin{{+}_{\BVS{#1}}}}$

$\newcommand{\BVLE}[1]{\mathbin{{\le}_{\BVS{#1}}}}$

$\newcommand{\BVGE}[1]{\mathbin{{\ge}_{\BVS{#1}}}}$

$\newcommand{\BVSL}[1]{\mathbin{{\ll}_{\BVS{#1}}}}$

$\newcommand{\BVTermB}[1]{\hat{t}_{(#1)}}$

$%\newcommand{\BVTermBI}[2]{\hat{t}_{#1}^{(#2)}}$

$\newcommand{\BVAtom}{\hat{A}}$

$\newcommand{\BVXB}[1]{\hat{x}_{(#1)}}$

$\newcommand{\BVYB}[1]{\hat{y}_{(#1)}}$

$\newcommand{\BVVar}[1]{\hat{x}_{(#1)}}$

$% SMTLIB logics$

$\newcommand{\SMTLIBLogic}[1]{\textrm{#1}}$

$\newcommand{\QFUF}{\SMTLIBLogic{QF\_UF}}$

$\newcommand{\QFLIA}{\SMTLIBLogic{QF\_LIA}}$

$\newcommand{\QFUFLRA}{\SMTLIBLogic{QF\_UFLRA}}$

$\newcommand{\SMTLIBLIA}{\SMTLIBLogic{LIA}}$

$\newcommand{\CG}[1]{G_{#1}}$

$\newcommand{\DiffEdge}[1]{\overset{#1}{\longrightarrow}}$

$\newcommand{\FuncName}[1]{\textsf{#1}}$

$\newcommand{\PredName}[1]{\textsf{#1}}$

$\newcommand{\ReadF}{\FuncName{read}}$

$\newcommand{\Read}[2]{\ReadF(#1,#2)}$

$\newcommand{\WriteF}{\FuncName{write}}$

$\newcommand{\Write}[3]{\WriteF(#1,#2,#3)}$

$\newcommand{\Abs}[1]{\alpha_{#1}}$

$\newcommand{\Expl}[1]{\textit{explain}(#1)}$

$\newcommand{\SMTAssertF}{\textsf{assert}}$

$\newcommand{\SMTAssert}[1]{\SMTAssertF(#1)}$

$\newcommand{\UFRoot}{\textit{parent}}$

$\newcommand{\UFRootOf}[1]{{#1}.\UFRoot}$

$\newcommand{\UFRank}{\textit{rank}}$

$\newcommand{\UFRankOf}[1]{{#1}.\UFRank}$

$\newcommand{\UFFind}[1]{\textsf{find}(#1)}$

$\newcommand{\UFMerge}[2]{\textsf{merge}(#1,#2)}$

$\newcommand{\CCPending}{\textit{pending}}$

$%$

$% Theory solver interface$

$%$

$\newcommand{\TSinit}[1]{\mathop{init}(#1)}$

$\newcommand{\TSassert}[1]{\mathop{assert}(#1)}$

$\newcommand{\TSretract}{\mathop{retract}()}$

$\newcommand{\TSisSat}{\mathop{isSat}()}$

$\newcommand{\TSgetModel}{\mathop{getModel}()}$

$\newcommand{\TSgetImplied}{\mathop{getImplied}()}$

$\newcommand{\TSexplain}[1]{\mathop{explain}(#1)}$

$\newcommand{\VarsOf}[1]{\mathop{vars}(#1)}$

$\newcommand{\Dist}[1]{\mathit{dist}(#1)}$

$%\newcommand{\Dist}[1]{\mathit{dist}(#1)}$

$%$

$% Nelson-Oppen$

$%$

$\newcommand{\TComb}{\cup}$

$\newcommand{\NOShared}[1]{\mathop{\textrm{shared}}(#1)}$

$\newcommand{\NOPart}{P}$

$\newcommand{\NOPartI}[1]{P_{#1}}$

$%\newcommand{\NOEq}{\mathrel{\approx}}$

$%\newcommand{\NOEqNot}{\mathrel{\not\approx}}$

$\newcommand{\NOEq}{\mathrel{{\equiv_{P}}}}$

$%\newcommand{\NOEq}{\stackrel{\NOPart}{\equiv}}$

$\newcommand{\NOEqNot}{\mathrel{\not\equiv_{\NOPart}}}$

$%\newcommand{\NOEqNot}{\stackrel{\NOPart}{\not\equiv}}$

$\newcommand{\NOArr}{\mathop{arr}(P)}$

$\newcommand{\NOArrI}[1]{\mathop{arr}(P_{#1})}$

$%$

$% Example formulas in Nelson-Oppen part$

$%$

$\newcommand{\NOF}{\phi}$

$%\newcommand{\NOFA}{\phi_1}$

$%\newcommand{\NOFB}{\phi_2}$

$%\newcommand{\NOTA}{\ThI{1}}$

$%\newcommand{\NOTB}{\ThI{2}}$

$\newcommand{\NOFEUF}{\phi_\mathit{EUF}}$

$\newcommand{\NOFLIA}{\phi_\mathit{LIA}}$

$\newcommand{\NOFLRA}{\phi_\mathit{LRA}}$

$\newcommand{\NOFCons}{\phi_\textup{cons}}$

$%\newcommand{\Asgn}{\mathrel{:=}}$

$\newcommand{\Asgn}{\mathrel{\leftarrow}}$

$%\newcommand{\Engl}[1]{(engl.\ #1)}$

$\newcommand{\Ack}[1]{\mathop{ack}(#1)}$

$\newcommand{\VVar}[1]{v_{#1}}$

$\newcommand{\FVar}[2]{{#1}_{#2}}$

$\newcommand{\PVar}[2]{{#1}_{#2}}$

$\newcommand{\Flat}{{\phi_\textrm{flat}}}$

$\newcommand{\Cong}{{\phi_\textrm{cong}}}$

$\newcommand{\In}{\mathit{in}}$

$\newcommand{\Out}{\mathit{out}}$

$\newcommand{\SubType}{\FuncName{subtype}}$

$%$

$% Fourier-Motzkin elimination$

$%$

$\newcommand{\FM}{\phi}$

$\newcommand{\FMup}{\phi^\textrm{up}}$

$\newcommand{\FMlo}{\phi^\textrm{low}}$

$%\newcommand{\FMup}{\phi^{\le}}$

$%\newcommand{\FMlo}{\phi^{\ge}}$

$\newcommand{\FMindep}{\phi^{\ast}}$

$\newcommand{\Nup}{n^\textrm{up}}$

$\newcommand{\Nlo}{n^\textrm{low}}$

$%\newcommand{\Nup}{n^{\le}}$

$%\newcommand{\Nlo}{n^{\ge}}$

$\newcommand{\Rup}[1]{A^\textrm{up}_{#1}}$

$\newcommand{\Rlo}[1]{A^\textrm{low}_{#1}}$

$%\newcommand{\Rup}[1]{A^{\le}_{#1}}$

$%\newcommand{\Rlo}[1]{A^{\ge}_{#1}}$

$%\newcommand{\FMless}{\mathrel{\triangleleft}}$

$%\newcommand{\FMmore}{\mathrel{\triangleright}}$

$\newcommand{\ProblemName}[1]{\textup{#1}}$

$\newcommand{\ATM}{A_\textup{TM}}$

$\newcommand{\PCP}{\ProblemName{PCP}}$

$\newcommand{\MPCP}{\ProblemName{MPCP}}$

$\newcommand{\PCPAst}{\star}$

$\newcommand{\Eps}{\varepsilon}$

$\newcommand{\List}[1]{[#1]}$

$\newcommand{\Strings}[1]{\{#1\}^\star}$

$\newcommand{\StringsOver}[1]{{#1}^\star}$

$\newcommand{\SigmaStrings}{\Sigma^\star}$

$\newcommand{\GammaStrings}{\Gamma^\star}$

$\newcommand{\Complement}[1]{\overline{#1}}$

$%$

$% SSA example$

$%$

$\newcommand{\In}{\mathit{in}}$

$\newcommand{\Out}{\mathit{out}}$

$%$

$\newcommand{\DA}{♠}$

$\newcommand{\DB}{♥}$

$\newcommand{\DC}{♦}$

$\newcommand{\DD}{♣}$

Part I: Basic Definitions¶

As we have seen earlier in the course, propositional logic is an excellent tool for many problem domains as very efficient SAT-solvers exist. But in some applications, it lacks expressive power. For instance, how would one model time constraints, such as “B must happen between 2.5 and 5 seconds after A”, with propositional logic?

Satisfiability modulo theories allows one to mix propositional logic with non-Boolean terms, e.g., from linear arithmetic over reals. This allows one to write constraints such as $(t_{\textrm{B}} - t_{\textrm{A}} \ge 2.5) \land (t_{\textrm{B}} - t_{\textrm{A}} \le 5.0).$ One could define SMT as “automatic theorem proving for decidable fragments of first-order logic”.

In this course, the SMT content is divided into three parts:

Part I gives the basic definitions concerning first-order logic as well as introduces the practical use of SMT solvers,
Part II shows how satisfiability of SMT formulas can be solved, i.e. the basics of how SMT solvers work, and
Part III discusses some advanced topics. It is not included in the Autumn 2020 course version.

Contents of Part I: