\usepackagepifont
\definecolorfakeaaltobluelRGB00,141,229
\definecoloraaltoblueRGB00,101,189
\definecoloraaltoredRGB237,41,57
\definecolorMyBoxBackgroundrgb0.98,0.98,1.0
\definecolorMyBoxBorderrgb0.90,0.90,1.0
\definecolorbackgroundredrgb1.0,0.98,0.98
\definecolorshadowredrgb1.0,0.90,0.90
\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.