\(%\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}{♣}\)

Theory Combination

So far we have considered only the case in which all the terms in the formulas are from a single theory. However, sometimes we would like to use several theories in a formula and write something like $${1 \le x} \land {x \le 2} \land {w_1 \Eq 1} \land {w_2 \Eq 2} \land {f(x) \Neq f(w_1)} \land {f(x) \Neq f(w_2)}$$ In the following introductory text, we consider satisfiability of quantifier-free conjunctions of literals; the approach generalizes to full Boolean case by using the CDCL(\( \Th \)) approach or DNF translation.

Sometimes combining theories is an easy task. Two theories, \( \ThI1 \) and \( \ThI2 \), are strongly disjoint if they do not share any sorts, and consequently no variables or function or predicate symbols. For such theories, one cannot mix different theories inside an atom. Thus the atoms can be fully separated into disjoint theory parts and the parts can be handled separately.

Example

In the formula $${x + 2y \le z} \land {y-z \Eq 0} \land {\Car(l) \Eq e} \land {\Cdr(l) \Eq l}$$ the linear arithmetic \( \TLIA \) part and the list \( \ThCons \) part (recall the exercise in Round 8) are fully separate if the element and list sorts in \( \ThCons \) are not \( \IntsSort \). Therefore, the formula is \( (\TLIA \TComb \ThCons) \)-satisfiable if and only if

  • ​ \( {x + 2y \le z} \land {y - z \Eq 0} \) is \( \TLIA \)-satisfiable and

  • ​ \( {\Car(l) \Eq e} \land {\Cdr(l) \Eq l} \) is \( \ThCons \)-satisfiable.

However, in general theory combination is a more complex topic.

The Nelson–Oppen Theory Combination Method

In many cases, the combined theories are not strongly disjoint but still have some properties that can be exploited when building solvers for the combined theory. Below we present the currently mostly used theory combination method that works for several theory combinations. To do that, we first need two additional definitions of “signature disjointness” and “stably infiniteness”.

Definition

Two theories, \( \ThI1 \) and \( \ThI2 \), are signature disjoint if they do not share any function or predicate symbols except for the equality symbol.

Example

Consider the theory \( \TLIA \) of linear arithmetic over integers and the theory \( \TEUF \) of uninterpreted functions with its element sort \( \ElemSort \) equal to \( \IntsSort \). One can now write formulas such as $${f(x+1) \le 3} \land {3f(y) \Eq 7}$$ The theories are signature disjoint as, intuitively,

  • ​ \( \TEUF \) does not place any restrictions on the element sort, and

  • ​ \( \TLIA \) does not consider the uninterpreted function and predicate symbols.

Formally, the axiomatic definition of \( \TEUF \) does not refer to the constants (\( 0 \) and \( 1 \)), functions (such as \( + \)), or predicates (\( < \)) other than the equality used in the axiomatic definition of \( \TLIA \). Vice versa, the axiomatic definition of \( \TLIA \) does not use the function symbols (such as \( f \)) or predicates appearing in the axiomatic definition of \( \TEUF \).

As shown in the next example, the straightforward combination of decision procedures does not work when variables or symbols are shared.

Example

Consider the conjunctive \( (\TEUF \TComb \TLIA) \)-formula $${1 \le x} \land {x \le 2} \land {w_1 \Eq 1} \land {w_2 \Eq 2} \land {f(x) \Neq f(w_1)} \land {f(x) \Neq f(w_2)}$$ where \( f: \IntsSort \to \IntsSort \). Now

  • ​ The “\( \TEUF \)-part” \( {f(x) \Neq f(w_1)} \land {f(x) \Neq f(w_2)} \) is satisfiable as \( \InterpI{1} = \{x \mapsto 3, w_1 \mapsto 1, w_2 \mapsto 2, f \mapsto \{1 \mapsto 4, 2 \mapsto 2, 3 \mapsto 6,…\}\} \) evaluates it to true.

  • ​ The “\( \TLIA \)-part” \( {1 \le x} \land {x \le 2} \land {w_1 \Eq 1} \land {w_2 \Eq 2} \) is satisfiable because \( \InterpI2 = \{x \mapsto 1, w_1 \mapsto 1, w_2 \mapsto 2\} \) evaluates it to true.

But these two interpretations are not compatible as they give different values to the variable \( x \).

In fact, the combination of the \( \TEUF \)- and \( \TLIA \)-parts, i.e. the whole formula, is unsatisfiable.

Definition: Stably Infiniteness

A theory \( \Th \) with signature \( \Sig \) is stably infinite if for every \( \Th \)-satisfiable \( \Sigma \)-formula \( \phi \) there is a \( \Th \)-model in which all the domains are infinite.

As an example, the theory of bit-vectors is not stably infinite while the theories \( \TEUF \), \( \TLIA \), \( \TLRA \) and so on are stably infinite. Intuitively, the stable infiniteness quarantees that combination method below always has enough “extra values” available.

The Abstract Method

As mentioned above, the Nelson–Oppen method is the current main method for combining theories. Its main idea is that for theories with some properties, it is enough to ensure that the different theory parts agree on the equalities between shared variables. In the following, we will gradully present an abstract version of the method for two theories, \( \ThI1 \) and \( \ThI2 \) with signatures \( \SigI1 \) and \( \SigI2 \), respectively, but the idea generalizes to multiple theories as well.

The goal of the method is to decide the \( (\ThI1 \TComb \ThI2) \)-satisfiability of a conjunction \( \phi \). The requirements are:

  1. \( \ThI1 \) and \( \ThI2 \) are signature disjoint

  2. \( \ThI1 \) and \( \ThI2 \) are stably infinite

  3. The conjunction \( \phi \) should be in form \( \phi_1 \land \phi_2 \), where

    • ​ \( \phi_1 \) is a \( \SigI1 \)-conjunction, and

    • ​ \( \phi_2 \) is a \( \SigI2 \)-conjunction

    This can be achieved with purification, explained next.

Purification

Given a \( (\SigI1 \cup \SigI2) \)-conjunction \( \phi \), purification transforms \( \phi \) into a \( \SigI1 \)-conjunction \( \phi_1 \) and a \( \SigI2 \)-conjunction \( \phi_2 \) such that \( \phi \) is \( (\ThI1 \cup \ThI2) \)-satisfiable if and only if \( \phi_1 \land \phi_2 \) is \( (\ThI1 \cup \ThI2) \)-satisfiable. That is, the conjunction will be divided in two parts that only concern a single theory but may share some variables. The diea of the purification process is simple: if an atom contains function or predicate symbols from two theories, substitute the other term with a new variable that is defined, in a separate atom, to be equal to that term. More precisely, the procedure can be described as follows. Let \( i,j \in \Set{1,2} \) with \( i \neq j \). Repeat the following as long as possible

  1. If \( f \in \SigI{i} \) and \( g \in \SigI{j} \) and \( f(…,g(…),…) \) is a term in \( \phi \), rewrite the term into \( f(…,t,…) \) and conjunct \( \phi \) with \( (t \Eq g(…)) \).

  2. If \( f \in \SigI{i} \) and \( g \in \SigI{j} \) and \( f(….) \Eq g(…) \) is a term in \( \phi \), rewrite the term into \( t \Eq g(…) \) and conjunct \( \phi \) with \( (t \Eq f(…)) \).

  3. If \( p \in \SigI{i} \), \( p \neq {\Eq} \) and \( f \in \SigI{j} \) and \( p(…,f(…),…) \) is an atom in \( \phi \), rewrite the atom into \( p(…,t,…) \) and conjunct \( \phi \) with \( (t \Eq f(…)) \).

In every step above, \( t \) is a new fresh variable not yet occurring in \( \phi \). Finally, \( \phi_1 \) is the conjunction of all the atoms in the resulting \( \phi \) that do not contain \( \SigI2 \)-symbols (and vice versa for \( \phi_2 \)).

Example

Consider the \( (\TLIA \TComb \TEUF) \)-conjunction $$\phi \quad\Def\quad {f(x+1) \le 3} \land {3f(y) \Eq 7}$$ Applying purification to it may produce $${t_2 \le 3} \land {3t_3 \Eq 7} \land {t_1 \Eq x+1} \land {t_2 \Eq f(t_1)} \land {t_3 \Eq f(y)}$$ and the theory parts are thus \begin{eqnarray*} \phi_\LIA &\Def& {t_2 \le 3} \land {3t_3 \Eq 7} \land {t_1 \Eq x+1}\\\\ \phi_\EUF &\Def& {t_2 \Eq f(t_1)} \land {t_3 \Eq f(y)} \end{eqnarray*}

In fact, purification can be applied to a non-conjunctive formulas as well, resulting in a formula where each atom contains symbols (other than \( \Eq \)) from a single theory only. Therefore, in the DPLL(\( \Th \)) framework one can apply the purification once in the beginning at the formula level. Furthermore, the size of the purified formula is linear in the size of the original formula.

Example

Consider the \( (\TLIA \TComb \TEUF) \)-formula $${f(x+1) \le 3} \Implies {3f(y) \Eq 7}$$ Applying purification to it may produce $$({t_2 \le 3} \Implies {3t_3 \Eq 7}) \land {t_1 \Eq x+1} \land {t_2 \Eq f(t_1)} \land {t_3 \Eq f(y)}$$

Shared variables, arrangements and the combination theorem

The set of shared variables of \( \phi_1 \land \phi_2 \) is \( \NOShared{\phi_1 \land \phi_2} = \VarsOf{\phi_1} \cap \VarsOf{\phi_2} \). For any partition \( \NOPart \) of \( \NOShared{\phi_1 \land \phi_2} \), the corresponding arrangement is the formula $$\NOArr = \bigwedge_{x_i \NOEq x_j} (x_i \Eq x_j) \land \bigwedge_{x_i \NOEqNot x_j} (x_i \Neq x_j)$$ where \( \NOEq \) is the equivalence relation induced by \( \NOPart \): \( x_i \NOEq x_j \) if and only if \( x_i \) and \( x_j \) belong to the same set in \( \NOPart \).

Theorem: Nelson–Oppen Theory Combination Theorem

\( \phi_1 \land \phi_2 \) is \( (\ThI1 \cup \ThI2) \)-satisfiable if and only if there exists a partition \( \NOPart \) of \( \NOShared{\phi_1 \land \phi_2} \) such that \( \phi_1 \land \NOArr \) is \( \ThI1 \)-satisfiable and \( \phi_2 \land \NOArr \) is \( \ThI2 \)-satisfiable.

Example

Consider the purified \( (\TEUF \TComb \TLIA) \)-conjunction \( \NOF \Def \NOFLIA \land \NOFEUF \) with

  • ​ \( \NOFLIA \Def {1 \le x} \land {x \le 2} \land {w_1 \Eq 1} \land {w_2 \Eq 2} \) and

  • ​ \( \NOFEUF \Def {{f(x) \Neq f(w_1)} \land {f(x) \Neq f(w_2)}} \).

The set of shared variables is \( \NOShared{\NOFLIA \land \NOFEUF} = \VarsOf{\NOFLIA} \cap \VarsOf{\NOFEUF} = \Set{x,w_1,w_2} \). The all possible partitions and arrangements over \( \NOShared{\NOFLIA \land \NOFEUF} \) are

  1. \( \NOPartI1 \Def \Set{\Set{x},\Set{w_1},\Set{w_2}} \) and \( \NOArrI1 \Def {x \Neq w_1} \land {x \Neq w_2} \land {w_1 \Neq w_2} \)

  2. \( \NOPartI2 \Def \Set{\Set{x},\Set{w_1,w_2}} \) and \( \NOArrI2 \Def {x \Neq w_1} \land {x \Neq w_2} \land {w_1 \Eq w_2} \)

  3. \( \NOPartI3 \Def \Set{\Set{x,w_1},\Set{w_2}} \) and \( \NOArrI3 \Def {x \Eq w_1} \land {x \Neq w_2} \land {w_1 \Neq w_2} \)

  4. \( \NOPartI4 \Def \Set{\Set{x,w_2},\Set{w_1}} \) and \( \NOArrI4 \Def {x \Neq w_1} \land {x \Eq w_2} \land {w_1 \Neq w_2} \)

  5. \( \NOPartI5 \Def \Set{\Set{x,w_1,w_2}} \) and \( \NOArrI5 \Def {x \Eq w_1} \land {x \Eq w_2} \land {w_1 \Eq w_2} \).

For each \( i \), either \( \NOFLIA \land \NOArrI{i} \) or \( \NOFEUF \land \NOArrI{i} \) is unsatisfiable; for instance,

  • ​ \( \NOFLIA \land \NOArrI1 \) is \( \TLIA \)-unsatisfiable as \( x \) must be either \( 1 \) or \( 2 \), i.e., equal to either \( w_1 \) or \( w_2 \), contradicting \( {x \Neq w_1} \land {x \Neq w_2} \) in \( \NOArrI1 \)

  • ​ \( \NOFEUF \land \NOArrI3 \) is \( \TEUF \)-unsatisfiable as \( x \Eq w_1 \) in \( \NOArrI3 \) implies \( f(x) \Eq f(w_1) \), contradicting \( f(x) \Neq f(w_1) \) in \( \NOFEUF \)

As a consequence, \( \NOFLIA \land \NOFEUF \) is \( (\TEUF \TComb \TLIA) \)-unsatisfiable.

Implementing the Abstract Method

Implementing the abstract method simply going through all the possible partitions is not practical at all. This is because the number of possible partitions of a set with \( n \) elements is known as the Bell number \( B_n \) and such numbers grow very fast, e.g., \( B_{20} = 51,724,158,235,372 \). So how can the abstract method be realized efficiently? There are basically two ways when we consider the CDCL(\( \Th \)) framework with a propositional SAT solver and theory solvers for the theories \( \ThI1 \) and \( \ThI2 \).

The Equality Detection and Propagation Method

In the first approach for implementing the abstract Nelson–Oppen method, one combines the solvers for the theories \( \ThI1 \) and \( \ThI2 \) into a new one for \( \ThI1 \cup \ThI2 \). The component theory solvers for \( \ThI{i} \), \( i \in \Set{1,2} \), shall implement detection of disjunctions of equalities: given a conjunction \( \phi_i \) of atoms, detect the (minimal) disjunctions \( (x_1 \Eq x’_1) \lor … \lor (x_k \Eq x’_k) \) such that

  • ​ \( x_1,…,x_k,x’_1,…,x’_k \) are shared variables, and

  • ​ \( \phi_i \ThIModels{i} (x_1 \Eq x’_1) \lor … \lor (x_k \Eq x’_k) \)

The detected disjunctions of equalities between shared variables are propagated to other theory solver. If the disjunction has more than one disjunct, case splitting must be done, i.e., the new combined theory solver tries to find a model by considering each disjunct \( x_j \Eq x’_j \) in turn. A high-level schematic picture of this approach is shown below.

_images/no-eq.png

Example

Consider the \( (\TEUF \TComb \TLIA) \)-conjunction \( \NOF \Def \NOFEUF \land \NOFLIA \) with

  • ​ \( \NOFEUF \Def {{f(x) \Neq f(w_1)} \land {f(x) \Neq f(w_2)}} \), and

  • ​ \( \NOFLIA \Def {1 \le x} \land {x \le 2} \land {w_1 \Eq 1} \land {w_2 \Eq 2} \).

In the combined theory solver,

  1. the literals in \( \NOFEUF \) are asserted in the \( \TEUF \)-solver: \( \TEUF \)-satisfiability but no implied equalities is reported

  2. the literals in \( \NOFLIA \) are asserted in the \( \TLIA \)-solver: \( \TLIA \)-satisfiability and the implied disjunction \( (x \Eq w_1) \lor (x \Eq w_2) \) over the shared variables is reported

  3. the combined theory solver performs case split:

    1. the equality \( (x \Eq w_1) \) is asserted in the \( \TEUF \)-solver: \( \TEUF \)-unsatisfiability is reported as \( {f(x) \Neq f(w_1)} \land {x \Eq w_1} \) is \( \TEUF \)-unsatisfiable

    2. the equality \( (x \Eq w_2) \) is asserted in the \( \TEUF \)-solver: \( \TEUF \)-unsatisfiability is reported as \( {f(x) \Neq f(w_2)} \land {x \Eq w_2} \) is \( \TEUF \)-unsatisfiable

  4. The combined solver deduces that \( \NOF \) is unsatisfiable

The drawback of this method is that one must augment the theory solvers with the capability of detecting (preferably minimal) implied disjunctions of equalities.

The Delayed Theory Combination Method

As mentioned above, building decision procedures that can detect (disjunctions of) equalities can be more challenging than the ones without this capability. In the “delayed theory combination” method, the idea is to use regular theory solvers and let the CDCL SAT solver take care of the equality literal handling as follows.

  • ​ Consider the CDCL(\( \Th \)) approach but now with two theory solvers, one for \( \ThI1 \) and one for \( \ThI2 \).

  • ​ In the beginning, introduce the \( \frac{n(n-1)}{2} \) possible interface equality atoms of the form \( x \Eq y \) over the \( n \) shared variables

  • ​ Let the SAT solver decide values for them (i.e., to guess an arrangement) and then pass them to the theory solvers as usual. In this way, the theory solvers don’t have to implement equality propagation because they receive the equalities from the SAT solver. Furthermore, the SAT solver can learn infeasible equality combinations because it receives conflicts involving the interface equalities from the theory solvers.

A high-level schematic picture of this approach is shown below.

_images/no-dtc.png

Example

Consider again the \( (\TEUF \TComb \TLIA) \)-conjunction \( \NOF \Def \NOFEUF \land \NOFLIA \) with

  • ​ \( \NOFEUF \Def {{f(x) \Neq f(w_1)} \land {f(x) \Neq f(w_2)}} \), and

  • ​ \( \NOFLIA \Def {1 \le x} \land {x \le 2} \land {w_1 \Eq 1} \land {w_2 \Eq 2} \).

In the beginning, the SAT solver introduces the 3 interface equalities $$x \Eq w_1, x \Eq w_2, w_1 \Eq w_2$$ Here is a possible run of the method:

  1. All the literals in the conjunction are asserted to true in the SAT solver.

  2. The literals in \( \NOFEUF \) are asserted in the \( \TEUF \)-solver: \( \TEUF \)-satisfiability is reported.

  3. The literals in \( \NOFLIA \) are asserted in the \( \TLIA \)-solver: \( \TLIA \)-satisfiability is reported.

  4. The SAT solver guesses that \( x \Eq w_1 \) is true.

  5. The literal \( x \Eq w_1 \) is asserted in the \( \TEUF \)-solver: \( \TEUF \)-unsatisfiability with the theory conflict \( {f(x) \Neq f(w_1)} \land {x \Eq w_1} \) is reported.

  6. The SAT solver analyzes the conflict clause \( {f(x) \Eq f(w_1)} \lor {x \Neq w_1} \), backtracks and unit propagates \( (x \Neq w_1) \).

  7. The literal \( x \Neq w_1 \) is asserted in the \( \TEUF \)-solver: \( \TEUF \)-satisfiability is reported.

  8. The literal \( x \Neq w_1 \) is asserted in the \( \TLIA \)-solver: \( \TLIA \)-satisfiability is reported.

  9. The SAT solver guesses that \( x \Eq w_2 \) is true.

  10. The literal \( x \Eq w_2 \) is asserted in the \( \TEUF \)-solver: \( \TEUF \)-unsatisfiability with the theory conflict \( {f(x) \Neq f(w_2)} \land {x \Eq w_2} \) is reported.

  11. The SAT solver analyzes the conflict clause \( {f(x) \Eq f(w_2)} \lor {x \Neq w_2} \), backtracks and unit propagates \( (x \Neq w_2) \).

  12. The literal \( x \Neq w_2 \) is asserted in the \( \TEUF \)-solver: \( \TEUF \)-satisfiability is reported.

  13. The literal \( x \Neq w_2 \) is asserted in the \( \TLIA \)-solver: \( \TLIA \)-unsatisfiability with the theory conflict \( {1 \le x} \land {x \le 2} \land {w_1 \Eq 1} \land {w_2 \Eq 2} \land {x \Neq w_1} \land {x \Neq w_2} \) is reported.

  14. The SAT solver analyzes the conflict and reports unsatisfiability.

Some notes: convexity and complexity

Convex theories are a special subclass for which the Nelson–Oppen combination with equality detection and propagation can be made simpler.

Definition: Convexity

A theory \( \Th \) is convex if $$\phi \ThModels \bigvee_{i=1}^n(u_i \Eq v_i) \text{ implies } \phi \ThModels (u_j \Eq v_j)\text{ for some \( j \in \Set{1,…,n} \)}$$ holds for all conjunctive \( \Sig \)-formulas \( \phi \), for all variables \( u_i \) and \( v_i \), and for all positive \( n \)

If both combined theories are convex, the equality detection and propagation approach has to only detect and propagate implied equalities, not disjunctions of equalities. As an example, linear arithmetic over reals and \( \EUF \) are convex theories.

Example

Linear arithmetic over integers is not convex as, for instance, $${0 \le x} \land {x \le 1} \land {y \Eq 0} \land {z \Eq 1} \LIAModels {x \Eq y} \lor {x \Eq z}$$ but neither

  • ​ \( {0 \le x} \land {x \le 1} \land {y \Eq 0} \land {z \Eq 1} \LIAModels {x \Eq y} \) nor

  • ​ \( {0 \le x} \land {x \le 1} \land {y \Eq 0} \land {z \Eq 1} \LIAModels {x \Eq z} \) holds

Assume that \( \ThI1 \) and \( \ThI2 \) are signature disjoint, stably infinite theories.

Theorem

If \( \ThI1 \) and \( \ThI2 \) are convex and both have polynomial time decision procedures, then the equality-propagating Nelson-Oppen procedure is a polynomial time decision procedure for \( \ThI1 \cup \ThI2 \).

Theorem

If \( \ThI1 \) and \( \ThI2 \) are non-convex and both have nondeterministic polynomial time decision procedures, then the equality-propagating Nelson-Oppen procedure is a nondeterministic polynomial time decision procedure for \( \ThI1 \cup \ThI2 \).

Combining EUF with another theory

One interesting special case is the combination \( \EUF \TComb \Th \) of the theory \( \EUF \) of uninterpreted functions with some other theory \( \Th \). Of course, one can use the Nelson–Oppen method as described earlier. But one can also use Ackermann’s reduction to get rid of the uninterpreted function and predicate symbols. That is, the \( (\EUF \TComb \Th) \)-satisfiability problem can be reduced to the \( \Th \)-satisfiability problem.

Given a formula \( \phi \) involving uninterpreted function and/or predicate symbols, Ackermann’s reduction translates \( \phi \) into a formula \( \phi’ \) that

  • ​ does not involve any uninterpreted function or predicate symbols, and

  • ​ is satisfiable if and only if \( \phi \) is.

The constructed formula \( \phi’ \) is of form \( \Flat \land \Cong \), where

  • ​ \( \Flat \Def \Ack{\phi} \) is a “flattened” version of \( \phi \), in which all the topmost uninterpreted function and predicate applications are replaced with new variables, and

  • ​ \( \Cong \) is a conjunction of implications that force function and predicate congruence.

Formally, the translation \( \Ack{\phi} \) is defined as follows:

  • ​ \( \Ack{p(t_1,…,t_n)} \) is a new Boolean variable \( \VVar{p(t_1,…,t_n)} \) for an uninterpreted \( n \)-ary predicate symbol \( p \),

  • ​ \( \Ack{f(t_1,…,t_n)} \) is a new variable \( \VVar{f(t_1,…,t_n)} \) of sort \( \Sort \) for an uninterpreted \( n \)-ary, \( n \ge 1 \), function symbol \( f \) of type \( \SortI{1} \times … \times \Sort_n \to \Sort \),

  • ​ \( \Ack{c} \Def c \) for each constant \( c \),

  • ​ \( \Ack{x} \Def x \) for each variable \( x \), and

  • ​ otherwise \( \Ack{\phi} \) is homomorphic wrt Boolean connectives, the equality symbol \( \Eq \), and interpreted functions \( f \) and \( p \), meaning that, e.g., \( \Ack{\phi_1 \land \phi_2} \Def \Ack{\phi_1} \land \Ack{\phi_2} \) and \( \Ack{t_1 + t_2} = {\Ack{t_1} + \Ack{t_2}} \).

The formula \( \Cong \) is a conjunction of implications that force function and predicate congruence:

  • ​ for each pair, \( f(t_1,…,t_n) \) and \( f(t’_1,…,t’_n) \) with \( n \ge 1 \), of uninterpreted function applications in \( \phi \), \( \Cong \) contains the implication $$(\bigwedge_{i=1}^n {\Ack{t_1} \Eq \Ack{t’_1}}) \Implies {\VVar{f(t_1,…,t_n)} \Eq \VVar{f(t’_1,…,t’_n)}}$$

  • ​ for each pair, \( p(t_1,…,t_n) \) and \( p(t’_1,…,t’_n) \), of uninterpreted predicate applications in \( \phi \), \( \Cong \) contains the implication $$(\bigwedge_{i=1}^n {\Ack{t_1} \Eq \Ack{t’_1}}) \Implies (\VVar{p(t_1,…,t_n)} \Iff \VVar{p(t’_1,…,t’_n)})$$

Example

Consider again the \( (\TLIA \TComb \TEUF) \)-formula $${f(x+1) \le 3} \Implies {3f(y) \Eq 7}$$ Applying Ackermann’s reduction to it produces $$({v_{f(x+1)} \le 3} \Implies {3v_{f(y)} \Eq 7}) \land ({x+1 \Eq y} \Implies {v_{f(x+1)} \Eq v_{f(y)}})$$ and thus the \( (\TLIA \TComb \TEUF) \)-satisfiability problem is reduced to a \( \TLIA \)-satisfiability problem

Example

If we apply the reduction to the formula \begin{eqnarray*} \phi &=&{\Out_1 \Eq \In} \land {\Out_2 \Eq f(\Out_1,\In)} \land {\Out_3 \Eq f(\Out_2,\In)} \land {}\\\\ &&{\Out’ \Eq f(f(\In,\In),\In)} \land {\Out_3 \Neq \Out’} \end{eqnarray*} discussed in Round 8, we get \begin{eqnarray} \Flat &\Def&{\Out_1 \Eq \In} \land {\Out_2 \Eq \VVar{f(\Out_1,\In)}} \land {\Out_3 \Eq \VVar{f(\Out_2,\In)}} \land {}\\\\ &&{\Out’ \Eq \VVar{f(f(\In,\In),\In)}} \land {\Out_3 \Neq \Out’}\\\\ \Cong &\Def& ({\Out_1 \Eq \Out_2} \land {\In \Eq \In} \Implies {\VVar{f(\Out_1,\In)} \Eq \VVar{f(\Out_2,\In)}}) \land {} \label{EX:fc1}\\\\ & & ({\Out_1 \Eq \In} \land {\In \Eq \In} \Implies {\VVar{f(\Out_1,\In)} \Eq \VVar{f(\In,\In)}}) \land {} \label{EX:fc2}\\\\ & & ({\Out_1 \Eq \VVar{f(\In,\In)}} \land {\In \Eq \In} \Implies {\VVar{f(\Out_1,\In)} \Eq \VVar{f(f(\In,\In),\In)}}) \land {}\\\\ & & ({\Out_2 \Eq \In} \land {\In \Eq \In} \Implies {\VVar{f(\Out_2,\In)} \Eq \VVar{f(\In,\In)}}) \land {}\\\\ & & ({\Out_2 \Eq \VVar{f(\In,\In)}} \land {\In \Eq \In} \Implies {\VVar{f(\Out_2,\In)} \Eq \VVar{f(f(\In,\In),\In)}}) \label{EX:fc5}\\\\ & & ({\In \Eq \VVar{f(\In,\In)}} \land {\In \Eq \In} \Implies {\VVar{f(\In,\In)} \Eq \VVar{f(f(\In,\In),\In)}}) \label{EX:fc6} \end{eqnarray} Now \( \Flat \land \Cong \) is unsatisfiable as

  1. \( \Out_1 \Eq \In \) in \( \Flat \) and \( {\Out_1 \Eq \In} \land {\In \Eq \In} \Implies {\VVar{f(\Out_1,\In)} \Eq \VVar{f(\In,\In)}} \) in \( \Cong \) imply \( \VVar{f(\Out_1,\In)} \Eq \VVar{f(\In,\In)} \),

  2. \( \VVar{f(\Out_1,\In)} \Eq \VVar{f(\In,\In)} \) and \( \Out_2 \Eq \VVar{f(\Out_1,\In)} \) in \( \Flat \) imply \( \Out_2 \Eq \VVar{f(\In,\In)} \),

  3. \( \Out_2 \Eq \VVar{f(\In,\In)} \) and \( {\Out_2 \Eq \VVar{f(\In,\In)}} \land {\In \Eq \In} \Implies {\VVar{f(\Out_2,\In)} \Eq \VVar{f(f(\In,\In),\In)}} \) in \( \Cong \) imply \( \VVar{f(\Out_2,\In)} \Eq \VVar{f(f(\In,\In),\In)} \), and

  4. \( \Out_3 \Eq \VVar{f(\Out_2,\In)} \), \( \Out’ \Eq \VVar{f(f(\In,\In),\In)} \), and \( \VVar{f(\Out_2,\In)} \Eq \VVar{f(f(\In,\In),\In)} \) imply \( \Out_3 \Eq \Out’ \),

which contradicts the conjunct \( \Out_3 \Neq \Out’ \) in \( \Flat \).

If we were interested in the \( \TEUF \)-validity of the formula \( \phi \) instead of \( \TEUF \)-satisfiability, we can use the same construction except that the reduced formula is $$\Cong \Implies \Flat$$ The intuition here is that all the models that respect function and predicate congruence should also satisfy the flattened formula.

For further details and analysis, see

Non-signature disjoint theories

In many interesting cases, one would like to combine theories that are not signature disjoint. For instance, combining linear arithmetic with acyclic lists extended with the length function $$… \land ({\Length(l) \le 3} \Implies {r_2 \Eq r_1 + \Length(l)}) \land …$$ Such a theory might include the following axioms in its definition

  • ​ \( \Length(\Nil) = 0 \)

  • ​ \( \A{l}{\ListSort}{\Length(\Cons(e,l)) = 1+\Length(l)} \)

Obviously, this is not signature disjoint with \( \TLIA \) and one cannot use the Nelson–Oppen method described earlier. Combining such theories is more complex and one can consult the references given below.

Some references