Rewritten first-order preliminaries

\psi$. Formulas $\varphi$ and $\psi$ are called \emph{equisatisfiable}

if $\varphi$ is satisfiable precisely if $\psi$ is satisfiable.

\subsection{First-order quantifier-free formulas and theories}

In the following text, we suppose the knowledge of a standard

first-order logic and model theory, which is given for example by

Enderton~\cite{End01}.

Definitions for the first-order quantifier-free formulas are similar

to those from subsection \ref{prelim:prop}, except that the set $\P$

now contains a fixed finite set of first-order atoms that do not

contain free variables. For example, if we consider a set of atoms

$\P = \{ x \geq y + 1, x = 4 \}$, where $x, y, 1$, and $4$ are

constant symbols, $x \geq y + 1~\vee~\neg (x = 4)$ is a clause.

A \emph{theory} $T$ is a set of first-order structures.  A formula

$\varphi$ is $T$-\emph{satisfiable} or $T$-\emph{consistent} if there

is a structure $M \in T$ in which the formula $F$ holds in the

standard first-order sense. The formula $\varphi$ is

$T$-\emph{unsatisfiable} or $T$-\emph{inconsistent} otherwise. If the

distinction is necessary, we call literals over a specific background

theory $T$-literals. In the rest of this chapter, we consider only

theories for which the satisfiability of conjunctions of literals is

decidable and we call any decision procedure for conjunctions of

$T$-literals a $T$-\emph{solver}.

Using the same notation as in the propositional logic, a partial

assignment is a set of literals and can be therefore seen as a

conjunction of literals, i.e. a formula. If a partial assignment $M$

is a propositional model of a given formula $\varphi$ and the partial

assignment $M$ is $T$-consistent, we say that $M$ is a

$T$-\emph{model} of $\varphi$. If $\varphi$ and $\psi$ are formulas

such that $\varphi \wedge \neg \psi$ is $T$-inconsistent, we say that

\emph{$\varphi$ entails $\psi$ in $T$} and write it as

$\varphi \models_T \psi$.

\subsection{First-order quantified formulas}

As the first-order formulas containing quantifiers are concerned, we

impose no restrictions on their form. We again suppose the knowledge

and definitions from the standard first-order logic and model theory.

A first-order formula $\varphi$ is in a \emph{negation normal form},

if the only logical connectives in $\varphi$ are negations,

conjunctions, and disjunctions and all negations in $\varphi$ occur in

front of a literal. Every first-order formula can be transformed to a

formula without existential quantifiers by introducing uninterpreted

functions; this process is known as \emph{Skolemization}.

\subsection{First-order logic and theories}

A \emph{signature} $\Sigma$ consists of a set of \emph{function

  symbols} $\Sigma^f$ and a set of \emph{predicate symbols} $\Sigma^p$

and for each of the symbols a non-negative number called its

\emph{arity}. Given a signature $\Sigma$, \emph{$\Sigma$-terms},

\emph{$\Sigma$-atoms}, \emph{$\Sigma$-literals},

\emph{$\Sigma$-clauses}, and \emph{$\Sigma$-formulas} are defined as

usual. We are using the logic with equality, i.e. the set of

$\Sigma$-atoms contains elements $t_1 = t_2$ for each pair of

$\Sigma$-terms $t_1, t_2$. If the signature is clear from the context,

we drop the $\Sigma$- prefix and speak only of terms, atoms, literals,

and so on. We call terms and formulas \emph{ground} if they contain no

free variables.

A \emph{$\Sigma$-structure} $\mathcal{A}$ consists of a non-empty set

$A$, the \emph{universe} of the structure, and an assignment

$(\_)^\mathcal{A}$, which to each variable $x$ assigns an element

$x^\mathcal{A} \in A$, to each function symbol $f \in \Sigma^f$ of

arity $n$ assigns a function $f^\mathcal{A} \colon A^n \rightarrow A$,

and to each predicate symbol $P \in \Sigma^p$ of arity $n$ assigns a

relation $P^\mathcal{A} \subseteq A^n$. Given a $\Sigma$-structure

$\mathcal{A}$, there exists a unique homomorphic extension of

$(\_)^\mathcal{A}$, which to each ground term $t$ assigns an element

$t^\mathcal{A} \in A$, and which can be further extended in a standard

way to assign a truth value

$\varphi^\mathcal{A} \in \{ \true, \false \}$ to each ground formula

$\varphi$. A $\Sigma$-structure $\mathcal{A}$ is said to

\emph{satisfy} a ground $\Sigma$-formula $\varphi$ if

$\varphi^\mathcal{A} = \true$. In such case, the structure

$\mathcal{A}$ is also called a \emph{model} of the

formula $\varphi$.

A \emph{$\Sigma$-theory} $\mathcal{T}$ is a class of

$\Sigma$-structures closed under isomorphisms and variable

reassignment. A ground $\Sigma$-formula is said to be satisfiable in

the $\Sigma$-theory $\mathcal{T}$, or $\mathcal{T}$-satisfiable, if

there exists a $\Sigma$-structure $\mathcal{A} \in \mathcal{T}$ such

that $\mathcal{A}$ satisfies $\varphi$. The structure $\mathcal{A}$ is

then called a \emph{$\mathcal{T}$-model} of $\varphi$. If $\varphi$

and $\psi$ are ground $\Sigma$-formulas such that

$\varphi \wedge \neg \psi$ is $\mathcal{T}$-unsatisfiable, we say that

\emph{$\varphi$ entails $\psi$ in $\mathcal{T}$} and write it as

$\varphi \models_T \psi$. A $\Sigma$-formula $\varphi$ such that

$\neg \varphi$ is $\mathcal{T}$-unsatisfiable is called a \emph{theory

  lemma}.

For two signatures $\Sigma$ and $\Omega$, we call $\Omega$ a

\emph{sub-signature} of $\Sigma$ if $\Omega \subseteq \Sigma$,

i.e. $\Omega^f \subseteq \Sigma^f$ and $\Omega^p \subseteq

\Sigma^p$. Given a $\Sigma$-structure $\mathcal{A}$ and a signature

$\Omega$ that is a sub-signature of $\Sigma$, the \emph{reduct} of

$\mathcal{A}$ to a sub-signature $\Omega$ is a $\Omega$-structure

$\mathcal{A}'$ that coincides with $\mathcal{A}$ on all symbols from

$\Omega$. For a $\Sigma_1$-theory $\mathcal{T}_1$ and a

$\Sigma_2$-theory $\mathcal{T}_2$, their \emph{combination}

$\mathcal{T}_1 + \mathcal{T}_2$ is the largest

$(\Sigma_1 \cup \Sigma_2)$-theory that contains all

$(\Sigma_1 \cup \Sigma_2)$-structures $\mathcal{A}$ for which the

reduct of $\mathcal{A}$ to $\Sigma_1$ is in $\mathcal{T}_1$ and the

reduct of $\mathcal{A}$ to $\Sigma_2$ is in $\mathcal{T}_2$.

We use the notation $\varphi[x_1, \ldots, x_n]$ for a formula whose

free variables are from the set $\{x_1, \ldots, x_n \}$. If

$\varphi[x_1, \ldots, x_n]$ is a formula and $t_1, \ldots, t_n$ are

terms, $\varphi[t_1, \ldots, t_n]$ denotes a results of the

simultaneous substitution of every free variable $x_i$ in $\varphi$ by

the term $t_i$.

In the rest of this chapter, we consider only theories for which the

satisfiability of conjunctions of literals is decidable and we call

any decision procedure for conjunctions of $\mathcal{T}$-literals a

$\mathcal{T}$-\emph{solver}.

% In the following text, we suppose the knowledge of a standard

% first-order logic and model theory, which is given for example by

% Enderton~\cite{End01}.

% Definitions for the first-order quantifier-free formulas are similar

% to those from subsection \ref{prelim:prop}, except that the set $\P$

% now contains a fixed finite set of first-order atoms that do not

% contain free variables. For example, if we consider a set of atoms

% $\P = \{ x \geq y + 1, x = 4 \}$, where $x, y, 1$, and $4$ are

% constant symbols, $x \geq y + 1~\vee~\neg (x = 4)$ is a clause.

% A \emph{theory} $\mathcal{T}$ is a set of first-order structures.  A formula

% $\varphi$ is $\mathcal{T}$-\emph{satisfiable} or $\mathcal{T}$-\emph{consistent} if there

% is a structure $M \in T$ in which the formula $F$ holds in the

% standard first-order sense. The formula $\varphi$ is

% $\mathcal{T}$-\emph{unsatisfiable} or $\mathcal{T}$-\emph{inconsistent} otherwise. If the

% distinction is necessary, we call literals over a specific background

% theory $\mathcal{T}$-literals. In the rest of this chapter, we consider only

% theories for which the satisfiability of conjunctions of literals is

% decidable and we call any decision procedure for conjunctions of

% $\mathcal{T}$-literals a $\mathcal{T}$-\emph{solver}.

% Using the same notation as in the propositional logic, a partial

% assignment is a set of literals and can be therefore seen as a

% conjunction of literals, i.e. a formula. If a partial assignment $M$

% is a propositional model of a given formula $\varphi$ and the partial

% assignment $M$ is $\mathcal{T}$-consistent, we say that $M$ is a

% $\mathcal{T}$-\emph{model} of $\varphi$. If $\varphi$ and $\psi$ are formulas

% such that $\varphi \wedge \neg \psi$ is $\mathcal{T}$-inconsistent, we say that

% \emph{$\varphi$ entails $\psi$ in $\mathcal{T}$} and write it as

% $\varphi \models_T \psi$.

% \subsection{First-order quantified formulas}

% As the first-order formulas containing quantifiers are concerned, we

% impose no restrictions on their form. We again suppose the knowledge

% and definitions from the standard first-order logic and model theory.

% A first-order formula $\varphi$ is in a \emph{negation normal form},

% if the only logical connectives in $\varphi$ are negations,

% conjunctions, and disjunctions and all negations in $\varphi$ occur in

% front of a literal. Every first-order formula can be transformed to a

% formula without existential quantifiers by introducing uninterpreted

% functions; this process is known as \emph{Skolemization}.

\section{Propositional satisfiability}

\section{Satisfiability modulo theories}

Similarly to \sat, the \emph{satisfiability modulo theories problem}

(\smt) is for a given a \cnf formula $\varphi$ in a fixed theory $T$

decide whether it is $T$-satisfiable. Depending on the the theory $T$,

(\smt) is for a given a \cnf formula $\varphi$ in a fixed theory $\mathcal{T}$

decide whether it is $\mathcal{T}$-satisfiable. Depending on the the theory $\mathcal{T}$,

the complexity of the \smt problem ranges from polynomial to

undecidable. However, as the formula $\varphi$ can contain Boolean

connectives, the \smt problem is at least \NP-hard for non-trivial

Notable examples of decidable first-order theories include

\begin{itemize}

\item the theory of \emph{equality and uninterpreted functions}, which

  contains all structures that interpret the predicate $=$ as a

  congruence with respect to all other functions,

\item the theory of \emph{linear integer arithmetic}, which consists

  of all structures isomorphic to integers with the function $+$ and

  predicates $\leq$ and $=$,

\item the theory of \emph{linear real arithmetic}, which consists

  of all structures isomorphic to real numbers with the function $+$ and

  predicates $\leq$ and $=$,

  for a given signature contains all structures over this signature

  and therefore imposes no restriction on the interpretation of

  function and predicate symbols;

\item the theory of \emph{linear integer arithmetic} over the

  signature $\{ +, \leq \}$, which consists of all structures

  isomorphic to integers with the function $+$ and the relation

  $\leq$;

\item the theory of \emph{linear real arithmetic} over the signature

  $\{ +, \leq \}$, which consists of all structures isomorphic to real

  numbers with the function $+$ and the relation $\leq$;

\item the theory of \emph{real arithmetic} \marginpar{In contrast to

    real arithmetic, integer arithmetic with multiplication was shown

    to be undecidable by Gödel.}, which consists of all structures

  isomorphic to real numbers with functions $+$ and $\times$ and

  predicates $\leq$ and $=$,

\item the theory of \emph{arrays}, which consists of all structures

  isomorphic to the set of arrays with a binary function $read(a, i)$

  interpreted as a value in the index $i$ of the array $a$, and a

  ternary function $write(a, i, v)$ interpreted as an array $a$

  modified to contain the value $v$ on the index $i$;

    to be undecidable by Gödel.} over the signature

  $\{ +, \times, \leq \}$, which consists of all structures isomorphic

  to real numbers with functions $+$ and $\times$ and the relation

  $\leq$,

\item the theory of \emph{arrays} over the signature $\{ read, write \}$,

  which consists of all structures isomorphic to the set of arrays

  with a binary function $read(a, i)$ interpreted as a value in the

  index $i$ of the array $a$, and a ternary function $write(a, i, v)$

  interpreted as an array $a$ modified to contain the value $v$ on the

  index $i$;

\item the theory of \emph{fixed-size bit-vectors}. \marginpar{TODO: describe}

\end{itemize}

For a detailed description of these theories and implementation of the

respective $T$-solvers, we refer the reader for example to the book of

Bradley and Manna~\cite{BM07}.\marginpar{TODO: paragraph about combination of theories}

respective $\mathcal{T}$-solvers, we refer the reader for example to the book of

Bradley and Manna~\cite{BM07}.

In pracitce, a satisfiability of formulas using a combination of

theories is often needed. For example, one formula may be using

integers, arrays, and uninterpreted functions. In their seminal work,

Nelson and Oppen have shown that satisfiability of combination of

stably infinite theories with disjoint signatures can be solved by

using separate satisfiability solvers for the respective theories,

which interchange implied equalities and disequalities between shared

variables. A theory $\mathcal{T}$ is \emph{stably infinite} for every

$\mathcal{T}$-satisfiable formula exists a $\mathcal{T}$ model, whose

universe is infinite. For a theory over a multi-sorted logic, the

theory is \emph{stably infinite} for every $\mathcal{T}$-satisfiable

formula exists a $\mathcal{T}$ model, whose every sort is interpreted

as infinite. This is not a strong restriction, almost all

\subsection{DPLL modulo theories}

On the other hand, the lazy \smt approach uses a \sat solver to reason

about the Boolean structure of the formula and a specialized

$T$-solver to reason about conjunctions of $T$-literals. There are two

variants of the lazy approach to the \smt solving -- \emph{online} and

\emph{offline}~\cite{FJOS03}.

$\mathcal{T}$-solver to reason about conjunctions of

$\mathcal{T}$-literals. There are two variants of the lazy approach to

the \smt solving -- \emph{online} and \emph{offline}~\cite{FJOS03}.

\paragraph{Offline approach}

In the offline approach, the input formula $\varphi$ is first

$\varphi^p$. If $\varphi^p$ is unsatisfiable, the input formula

$\varphi$ is also unsatisfiable. On the other hand, if $\varphi^p$ is

satisfiable, the \sat solver returns its propositional model $M^p$,

and the $T$-solver can be used to determine $T$-satisfiability of the

corresponding set of literals $M$. If the $T$-solver decides $M$ to be

$T$-satisfiable, the formula $\varphi$ is also $T$-satisfiable. If the

propositional model is not $T$-satisfiable, the corresponding theory

lemma $\neg M^p$ is added to the formula and the procedure is

repeated. This variant of the lazy \smt approach is called offline,

because it uses the \sat solver as a black box and employs the \smt

solver only to check satisfiability of a complete Boolean assignment.

and the $\mathcal{T}$-solver can be used to determine

$\mathcal{T}$-satisfiability of the corresponding set of literals

$M$. If the $\mathcal{T}$-solver decides $M$ to be

$\mathcal{T}$-satisfiable, the formula $\varphi$ is also

$\mathcal{T}$-satisfiable. If the propositional model is not

$\mathcal{T}$-satisfiable, the corresponding theory lemma $\neg M^p$

is added to the formula and the procedure is repeated. This variant of

the lazy \smt approach is called offline, because it uses the \sat

solver as a black box and employs the \smt solver only to check

satisfiability of a complete Boolean assignment.

\paragraph{Online approach}

In contrast to the offline approach, the \sat and \smt solvers can

not only to check validity of total Boolean assignments, but it is

also used to check the validity of partial assignments during the

\dpll search (known as \emph{early pruning}~\cite{ABCKS02}), to assign

values of literals which are $T$-entailed by the current assignment

(known as \emph{theory propagation}~\cite{ACG99}), and to provide

smaller theory lemmas that explain the conflict. In order for this

combination to be efficient, the $T$-solver should provide several

important features. Namely, it should be \emph{incremental}, so it

does not restart the computation after every decided literal, it

should be able to provide small theory lemmas explaining conflicts and

theory propagations, so the \sat solver can backtrack to a relevant

decision literal, and it should be able to efficiently unassign the

values of literals during backtracking. In most of the cases, the

$T$-solver is also required to be able to provide models for the

satisfiable formulas.

This \smt approach, in which the $T$-solver is used to guide the

search of the underlying \dpll solver has been named

values of literals which are $\mathcal{T}$-entailed by the current

assignment (known as \emph{theory propagation}~\cite{ACG99}), and to

provide smaller theory lemmas that explain the conflict. In order for

this combination to be efficient, the $\mathcal{T}$-solver should

provide several important features. Namely, it should be

\emph{incremental}, so it does not restart the computation after every

decided literal, it should be able to provide small theory lemmas

explaining conflicts and theory propagations, so the \sat solver can

backtrack to a relevant decision literal, and it should be able to

efficiently unassign the values of literals during backtracking. In

most of the cases, the $\mathcal{T}$-solver is also required to be

able to provide models for the satisfiable formulas.

This \smt approach, in which the $\mathcal{T}$-solver is used to guide

the search of the underlying \dpll solver has been named

\dpllt~\cite{NOT06}. For the detailed description of \dpllt and

further improvements, we refer the reader to survey on the

topic~\cite{Seb07}, or to the abstract description of the underlying

\dpll approach allows the solver to be modular, it can be also

restricting in some cases. In particular, \dpllt based solvers can not

directly reason about values of first-order variables, but have to

rely on the $T$-solver guiding the search over Boolean

rely on the $\mathcal{T}$-solver guiding the search over Boolean

valuations. While there are some techniques like \emph{splitting on

  demand}~\cite{BNOT06} , which allow the $T$-solver to add new atoms

to the formula and delegate the case splitting to the underlying \sat

solver, their performance depends on the internal heuristics of the

\sat solver. To overcome this issue, Cotton has proposed \emph{Natural

  domain \smt} approach, which allows the \smt solver to reason

directly about the natural domains of variables like integers or reals

instead of merely choosing Boolean valuations of existing

literals~\cite{Cot10}. This has led to two main techniques of \smt

solving -- \emph{abstract conflict-driven clause learning} and

  demand}~\cite{BNOT06} , which allow the $\mathcal{T}$-solver to add

new atoms to the formula and delegate the case splitting to the

underlying \sat solver, their performance depends on the internal

heuristics of the \sat solver. To overcome this issue, Cotton has

proposed \emph{Natural domain \smt} approach, which allows the \smt

solver to reason directly about the natural domains of variables like

integers or reals instead of merely choosing Boolean valuations of

existing literals~\cite{Cot10}. This has led to two main techniques of

\smt solving -- \emph{abstract conflict-driven clause learning} and

\emph{model-constructing satisfiability calculus}~\cite{Mon16}.

\paragraph{Abstract \cdcl} Abstract conflict-driven clause learning

$F \models_T I$, $G \wedge I$ is unsatisfiable, and all uninterpreted

symbols in $I$ are contained in both $F$ and $G$. Following the work

of Pudlák~\cite{Pud97} or and McMillan~\cite{McM05}, an interpolant

for the pair $(F, G)$ over the theory $T$ can be computed from a

for the pair $(F, G)$ over the theory $\mathcal{T}$ can be computed from a

resolution proof of unsatisfiability of $F \wedge G$ by using a

combination of a propositional interpolating algorithm and a theory

specific interpolation procedure, which computes interpolants of

\subsection{Model-based quantifier instantiation}

Given a closed formula with quantifiers, the first step is to convert

the formula to the negation normal form and apply Skolemization to

obtain equisatisfiable formula of the form \marginpar{TODO: V

  preliminaries vysvětlit notaci $\psi[x_1, \ldots, x_n]$}

obtain equisatisfiable formula of the form

\[

   \varphi ~\wedge~ \forall x_1, x_2, \dots, x_n\, (\psi[x_1, \dots, x_n]),

\]

which was proposed for quantified bit-vector formulas by Wintersteiger

et al:

\[

  \forall x. \, (x \not = t ~\vee~ \varphi)~~\leadsto~~\varphi[x \leftarrow t],

  \forall x. \, (x \not = t ~\vee~ \varphi[x])~~\leadsto~~\varphi[t],

\]

where $t$ is an arbitrary term that does not contain $x$. As the

\der rule eliminates the quantified variable, it in many cases also

version of the \der rule, which we have called \emph{constructive

  equality resolution}:

\[

  \exists x. \, (x = t ~\wedge~ \varphi)~~\leadsto~~\varphi[x \leftarrow t],

  \exists x. \, (x = t ~\wedge~ \varphi[x])~~\leadsto~~\varphi[t],

\]

where $t$ is an arbitrary term that does not contain $x$.

\newcommand{\mcbv}{\textsc{mcbv}\xspace}

\newcommand{\nnf}{\textsc{nnf}\xspace}

\newcommand{\true}{\ensuremath{\texttt{true}}}

\newcommand{\false}{\ensuremath{\texttt{false}}}

%solvers

\newcommand{\uclid}{\textsc{uclid}\xspace}

\newcommand{\fpacdcl}{\textsc{fp-acdcl}\xspace}

\newcommand{\sort}[1]{\ensuremath{[#1]}}

\newcommand{\extract}[2]{\ensuremath{\texttt{extract}^{#1}_{#2}}}

\newcommand{\SymDivine}{\textsf{SymDIVINE}\xspace}

\newcommand{\der}{\textsc{der}\xspace}