Going to bed

This section introduces the notation used in the rest of this

chapter. The exposition of the propositional logic is mainly based on

the work of Nieuwenhuis et al.~\cite{NOT06}. The exposition of the

first-order logic is based on works of Enderton~\cite{End01} and of

Barrett et al.~\cite{BSST09}. Note that instead of following the

approach of Enderton, we follow the approach of Barrett et al. and

define the theory as a set of first-order \emph{structures}, rather

than a set of first-order sentences.

first-order logic is based mainly on works of Enderton~\cite{End01}

and of Barrett et al.~\cite{BSST09}. Note that instead of following

the approach of Enderton to the first-order theories, we follow the

approach of Barrett et al. and define the theory as a set of

first-order \emph{structures}, rather than a set of first-order

sentences.

\subsection{Propositional formulas, assignments, and satisfaction}

\label{prelim:prop}

variable $x \in \P$ there are two literals -- a \emph{positive

  literal} $x$ and a \emph{negative literal} $\overline{x}$. For a

given literal $l$, we define $\neg l$ as $\overline{l}$ if $l = x$ for

some variable $x$ and as $x$ if $l = \overline{x}$ for some variable

a variable $x$ and as $x$ if $l = \overline{x}$ for a variable

x. Literals $l$ and $\neg l$ are called \emph{complementary}. A

\emph{clause} is a finite disjunction of literals. The empty clause is

denoted by $\bot$. A formula in the \emph{conjunctive normal form}

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

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

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

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

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

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

\emph{$\Sigma$-clauses}, \emph{$\Sigma$-formulas}, and

that \emph{$\Gamma$ entails $\varphi$ in $\mathcal{T}$}, written

$\Gamma \models_\mathcal{T} \varphi$, if every $\Sigma$-structure that

satisfies all formulas in $\Gamma$ also satisfies $\varphi$. If

$\emptyset \models_\mathcal{T} \varphi$ for a $\Sigma$-formula

$\varphi$, the formula $\varphi$ is called \emph{$\mathcal{T}$-valid}

or a \emph{theory lemma}. A set $\Gamma$ of $\Sigma$-formulas is

called \emph{$\mathcal{T}$-inconsistent}, if

$\emptyset \models_\mathcal{T} \varphi$, the formula $\varphi$ is

called \emph{$\mathcal{T}$-valid} or a \emph{theory lemma}. A set

$\Gamma$ of $\Sigma$-formulas is called

\emph{$\mathcal{T}$-inconsistent}, if

$\Gamma \models_{\mathcal{T}} \bot$.

% If $\varphi$

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

satisfiability of conjunctions of $\Sigma$-literals is decidable and

we call any decision procedure for conjunctions of $\Sigma$-literals a

$\mathcal{T}$-\emph{solver}. Moreover, if the signature or the theory

is clear from the context, we drop the respective $\Sigma$- or

$\mathcal{T}$- prefixes.

\section{Propositional satisfiability}

\label{sec:sat}

A \emph{propositional satisfiability problem} (\sat) is, for a given

formula $\varphi$ in \cnf, to decide whether it is satisfiable. The

A \emph{propositional satisfiability problem} (\sat) is to decide for

a given formula $\varphi$ in \cnf, whether it is satisfiable. The

restriction to formulas in \cnf is without a loss of generality, as

the Tseytin transformation can be used to transform every formula to

an equisatisfiable formula in \cnf with only linear increase of its

clause $C$. Note that this literal does not have to be the last

decision literal in the search and therefore a bigger region of the

search space can be ruled out from the search, as it is known not to

contain any solution. There are multiple strategies of computing the

contain any solutions. There are multiple strategies of computing the

clausal reason for the conflict, but the majority of \cdcl based \sat

solvers are using the \emph{first unique implication point} based

learning scheme, which has been shown to produce small clauses in

combinations of the represented Boolean functions using the recursive

procedure \texttt{Apply}~\cite{Bry86}. The main idea of symbolic \sat

solvers is to convert a \cnf formula to the corresponding \robdd and

check the root of the resulting \bdd. If the resulting \bdd has the

root 0, the formula is unsatisfiable, and it is satisfiable

otherwise. However, in order to keep the size of the \bdd small, it is

necessary to existentially quantify the variables during the

computation. This technique is known as \emph{early

  quantification}~\cite{HKB96}. A simplified symbolic \sat algorithm

can be found for example in the survey of \sat solving by Darwiche and

Pipatsriswat~\cite{DP09}.

check the root of the resulting \bdd. If the resulting \bdd is

equivalent to the \bdd for the constant $0$ function, the formula is

unsatisfiable, and it is satisfiable otherwise. However, in order to

keep the size of the \bdd small, it is necessary to existentially

quantify the variables during the computation. This technique is known

as \emph{early quantification}~\cite{HKB96}. A simplified symbolic

\sat algorithm can be found for example in the survey of \sat solving

by Darwiche and Pipatsriswat~\cite{DP09}.

Look-ahead based algorithm, in contrast to the \cdcl, are employing

expensive heuristics to guide the \dpll search to a satisfying

  ternary function $\arwrite(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}, in which the

  structure contains all bit-vectors as an universe, ordering

  relations according to the corresponding integers, and interpreted

  functions are bit-wise operations on the bit-vectors and modular

  arithmetic operations on the corresponding integers. This theory is

  in detail described in section \ref{sec:qfbv}.

  structure contains set of all bit-vectors as an universe, bit-wise

  and arithmetic functions on those bit-vectors, and ordering

  relations on the corresponding integers. This theory is in detail

  described in section \ref{sec:qfbv}.

\end{itemize}

For a detailed description of these theories and implementation of the

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

infinite domain. Although almost all practically used theories are

stably infinite, this is not true for inherently finite theories like

the theory of bit-vectors. Therefore, variants of the theory

combinations in which one of the theories does not have to be stably

combination in which one of the theories does not have to be stably

infinite have been proposed~\cite{TZ05, RRZ05, JB10}.

\subsection{DPLL modulo theories}

is directly translated to an equivalent propositional formula and an

off-the-shelf \sat solver is used to decide satisfiability of this

formula. The eager \smt approach is implemented for example in the

\smt solver \uclid, which supports the combination of the theory of

uninterpreted functions and linear integer arithmetic~\cite{LS04}.

\smt solver \uclid for the combination of the theory of uninterpreted

functions and linear integer arithmetic~\cite{LS04}.

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

about the Boolean structure of the formula and a specialized

$\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}.

$\Sigma$-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$ is also unsatisfiable. On the other hand, if $\varphi^p$ is

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

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}$-satisfiability of the corresponding set of

$\Sigma$-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$

\subsection{Natural domain \smt}

\label{ssec:natDomainSat}

Although the separation of the propositional and theory reasoning in

the \dpllt 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 $\mathcal{T}$-solver guiding the search over Boolean

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

\dpllt 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

$\mathcal{T}$-solver guiding the search over Boolean valuations. While

there are some techniques like \emph{splitting on

  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

In thus specified framework, an abstract domain can be replaced by an

arbitrary domain that satisfies a certain set of requirements and this

yields an abstract conflict-driven clause learning \acdcl algorithm

using this particular domain. As an example, Brain et al. have

using this particular domain. For example, Brain et al. have

implemented the \fpacdcl solver for the floating point arithmetic

using an abstract interval domain and have shown that on a certain

class of formulas it significantly outperforms state-of the art \smt

selector variable and after a top level conflict, clauses whose

selector variable appears in the final conflict clause are returned as

an unsatisfiable core. Third approach consists in combination of an

\smt solver with an external propositional core~\cite{CGS07}.

\smt solver with an external propositional core

extractor~\cite{CGS07}.

A (Craig) interpolant for a pair of formulas $F$ and $G$ such that

$F \wedge G$ is unsatisfiable is a formula $I$ such that

$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 $\mathcal{T}$ can be computed from a

of Pudlák~\cite{Pud97} and McMillan~\cite{McM05}, an interpolant 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

The \emph{theory of fixed sized bit-vectors (\BV)} is a many-sorted

first-order theory with infinitely many sorts $\sort{n}$ corresponding

to bit-vectors of length $n$. The only predicate symbols in the \BV

theory are $=$, $\leq_u$, and $\leq_s$, interpreted as equality,

unsigned inequality of binary-encoded natural numbers, and signed

inequality of integers in $2$'s complement representation,

respectively. Function symbols in the theory are $+$, $\times$,

$\div$, $\&$, $\mid$, $\oplus$, $\ll$, $\gg$, $\cdot$,

$\extract{n}{p}$, interpreted as addition, multiplication, unsigned

division, bit-wise and, bit-wise or, bit-wise exclusive or,

left-shift, right-shift, concatenation, and extraction of $n$ bits

starting from the position $p$, respectively. For the detailed

description of the \BV theory syntax and semantics, see for example

Hadarean's PhD thesis~\cite{Had15}. This section focuses on the

problem of satisfiability of the quantifier-free fragment of the \BV

theory, denoted \QFBV. The the full \BV logic is treated in the next

section.

theory are $\leq_u$ and $\leq_s$, interpreted as inequality of

binary-encoded unsigned and signed integers, respectively. Function

symbols in the theory are $+$, $\times$, $\div$, $\&$, $\mid$,

$\oplus$, $\ll$, $\gg$, $\cdot$, $\extract{n}{p}$, interpreted as

addition, multiplication, unsigned division, bit-wise and, bit-wise

or, bit-wise exclusive or, left-shift, right-shift, concatenation, and

extraction of $n$ bits starting from the position $p$,

respectively. For the detailed description of the \BV theory syntax

and semantics, see for example Hadarean's PhD

thesis~\cite{Had15}. This section focuses on the problem of

satisfiability of the quantifier-free fragment of the \BV theory,

denoted \QFBV. The the full \BV logic is treated in the next section.

Current state-of-the-art \smt solvers for the \QFBV logic rely on

rewriting techniques used to simplify the formula during the

to the equivalent propositional formula, which is subsequently solved

by a \sat solver. The transformation of a bit-vector formula to the

equivalent propositional formula is traditionally called

\emph{bit-blasting}~\cite{Kro08}.  \marginpar{TODO: Nepřidat odstavec

  o propagating-complete \cnf encodings?} More lazy approach to the

\emph{bit-blasting}~\cite{Kro08}. More lazy approach to the

bit-blasting is beneficial when the theory combination is

required. For example, solvers Z3 and Yices apply bit-blasting to all

operations except for the equality, which is handled by a specialized

problems, it can exhaust memory of the solver if the input formula

contains complex arithmetic or variables with large bit-width. Several

techniques that avoid the bit-blasting and work directly on the level

of individual bit-vectors (\emph{word-level}) have been proposed to

of individual bit-vectors (\emph{word level}) have been proposed to

alleviate this problem.

Some useful fragments of the bit-vector theory can be solved by

specialized algorithms for deciding satisfiability. For example,

conjunctions of literals in the \emph{core theory of bit-vectors}

consisting of equality, concatenation and extraction, is decidable in

consisting of equality, concatenation and extraction, are decidable in

polynomial time by reduction to the theory of equality~\cite{CMR97,

  BS09}. Additionally, Babić and Musuvathi have described algorithms

for solving linear and non-linear modular arithmetic, which can be

verification of programs in a single static assignment form, such as

LLVM bit-code.

With a slight abuse of notation which identifies interpreted function

symbols with their intended interpretations, a simple definition of

invertibility for binary function symbols, which can be easily

generalized, is as follows. A binary function $f$ can be inverted with

respect to its first argument if for every two values $a_i, a_o$ there

exists a value $b$ such that $f(b,a_i) = a_o$. For example, as the

addition is invertible with respect to its first argument, the formula

With a slight abuse of notation which identifies function symbols with

their intended interpretations, a simple definition of invertibility

for binary function symbols is as follows. A binary function $f$ can

be inverted with respect to its first argument if for every two values

$a_i, a_o$ there exists a value $b$ such that $f(b,a_i) = a_o$. This

definition can be easily generalized to functions of different

arities. For example, as the addition is invertible with respect to

its first argument, the formula

$\varphi \equiv x + (y * y - 30 * z * y) = 0$ can be transformed to an

equisatisfiable formula $v = 0$, where $v$ is a fresh variable,

because $x$ is unconstrained in $\varphi$. Note that in contrast to

decide the satisfiability of the formula. For the bit-vector theory,

the most widely used approach is the \emph{model-based quantifier

  instantiation}~\cite{GM09}, implemented in Z3, CVC4, and Yices,

combined by heuristics as \emph{E-matching} or \emph{symbolic

combined with heuristics as \emph{E-matching} or \emph{symbolic

  quantifier instantiation}~\cite{WHD13,Dut15}. Additionally, for

dealing with quantifiers, CVC4 supports solving quantified formulas by

\emph{counter-example guided quantifier instantiation}~\cite{RDKT15}.

indeed a model of the formula $\forall x_1, x_2, \dots, x_n\,(\psi)$,

therefore the entire formula is satisfiable and $M$ is its model. If

$\neg \widehat{\psi}$ is satisfiable, we get values $v_1, \dots, v_n$

such that $\neg\widehat{\psi}[v_1, \dots, v_n]$ holds.  To rule out

$M$ as a model as the formula $\varphi$, the instance

$\psi[v_1, \dots, v_n]$ of the quantified formula is added to the

quantifier-free part, i.e.~the formula $\varphi$ is modified to

such that $\neg\widehat{\psi}[v_1, \dots, v_n]$ holds. To rule out $M$

as a model of the input formula, the instance $\psi[v_1, \dots, v_n]$

of the quantified formula is added to the quantifier-free part,

i.e.~the formula $\varphi$ is modified to

\[

   \varphi' ~\equiv~ \varphi \wedge \psi[v_1, \dots, v_n],

\]

of the bit-vector satisfiability problem differ in allowing

uninterpreted functions, allowing quantifiers, and in encoding of the

bit-widths (unary vs. binary). In the following, we follow the

notation of Kováznai et al~\cite{KFB16} -- decision problems for

notation of Kováznai et al.~\cite{KFB16} -- decision problems for

quantifier-free fragments are denoted by the prefix QF\_, the

combination with the theory of uninterpreted functions is denoted by

the prefix UF, and the problems with unary and binary encoded

polynomial time reduction from QF\_BV1 to \sat, showing that QF\_BV1

is in NP. A similar reduction from BV1 to \qbf can show that BV is in

\PSPACE. For lower bounds, \NP-hardness of QF\_BV1 follows from a

simple reduction from \sat, by encoding each propositional variable as

simple reduction from \sat by encoding each propositional variable as

a bit-vector of bit-width 1. Similarly, BV1 can be shown to be

\PSPACE-hard by considering every bit-vector as a quantified variable

of bit-width 1.

instantiation-based one is the ability of representing all models of a

universally quantified formula even in cases in which finding a

suitable set of quantifier instantiations would be infeasible. The

following formula, in which all variables have bit-with 32 bits, shows

this difference:

following formula, in which all variables have bit-width 32 bits,

shows this difference:

\[

  \varphi \equiv a=16 \cdot b \,+\, 16 \cdot c~\wedge~\forall (x :

  [32]) \, (a \not = 16 \cdot x).

The \bdd-based solver can quickly compute the \bdd for the quantified

subformula $\forall (x : [32]) \, (a \not = 16 \cdot x)$, which shows

that at least one of the last 4 bits of the variable $a$ has to be

$0$, i.e. the value of $a$ is not divisible by $16$. After conjoining

$1$, i.e. the value of $a$ is not divisible by $16$. After conjoining

this \bdd to the \bdd for $a=16 \cdot b \,+\, 16 \cdot c$, the formula

is decided unsatisfiable, as the resulting \bdd has root $0$. On the

other hand, if one considers only quantifier instantiations by the

subterm of the input formula, exponentially many quantifier instances

have to be added to the formula to show its unsatisfiability, as there

is no subterm of $\varphi$ that can be instantiated as $x$ to yield an

unsatisfiable quantifier-free formula.

is decided unsatisfiable, as the resulting \bdd represents the

constant $0$ function. On the other hand, if one considers only

quantifier instantiations by the subterm of the input formula,

exponentially many quantifier instances have to be added to the

formula to show its unsatisfiability, as there is no subterm of

$\varphi$ that can be instantiated as $x$ to yield an unsatisfiable

quantifier-free formula.

\subsection{Simplifications}

Moreover, universal quantification can distribute over disjunctions in

cases where the variable bound by the quantifier does not occur in one

of the conjuncts. This leads to the following rule and its dual

of the disjuncts. This leads to the following rule and its dual

version, which is known as \emph{miniscoping}:

\[

  \forall x. \, (\varphi ~\vee~ \psi)~~\leadsto~~(\forall x . \,

Ordering of \bdd variables is crucial for efficiency. The size of a

\bdd can differ exponentially when choosing a different

ordering. Therefore, besides well known methods of dynamic variable

reordering during the computation, Q3B precomputes

initial variable ordering, which is based on the dependencies among

the variables in the formula.

reordering during the computation, Q3B computes an initial variable

ordering, which is based on the syntactic dependencies among the

variables in the formula.

We have implemented and compared three different initial orderings,

which we denote $\leq_1, \leq_2, \leq_3$.

  \end{minipage}}

\end{table}

Recently, this results was confirmed by the \smt competition 2016 --

Recently, these results were confirmed by the \smt competition 2016 --

our solver is the winner of the quantified-bit vectors category. Table

\ref{tbl:smtcomp} shows official results for this category. The

benchmarks are divided into two groups, with \emph{known} and

with unknown status than any of the other solvers.

\section{Other areas of research}

Outside the field of \smt solving, my research also consists in

Outside the field of \smt solving, my research interests also include

software verification. In this field, I have co-authored the following

paper on the tool Symbiotic, which combines instrumentation, slicing

and, symbolic execution to allow verification of a real-world

    Formulas Using Binary Decision Diagrams.}" In: Theory and

  Applications of Satisfiability Testing -- SAT 2016 -- 19th

  International Conference, Bordeaux, France, July 5-8, 2016,

  Proceedings. 2016, pp. 267-283

  Proceedings. 2016, pp. 267-283~\cite{JS16}

  \smallskip

  I am the main author of the text of the paper. I have also

  Algorithms for the Construction and Analysis of Systems -- 22nd

  International Conference, TACAS 2016, Held as Part of the ETAPS

  2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings,

  pp. 946-949

  pp. 946-949~\cite{CJSSV16}

  \smallskip

developed by Zeljić et al. The \bdd representation can be added to the

currently used over-approximations by bit-patterns and arithmetic

intervals. Moreover, a tighter cooperation is possible -- if a value

of a variable is decided by during the \mcbv computation, it can be

used to partially instantiate a quantified part of the formula, for

which the \bdd will be computed.

As the part of my PhD study, an implementation of a solver using the

hybrid approach and its evaluation on the representative set of

benchmarks is expected. The hybrid approach to quantified bit-vectors

is the main aim of my PhD study.

of a variable is decided during the \mcbv computation, it can be used

to partially instantiate a quantified part of the formula, for which

the \bdd will be computed.

\subsection{Unconstrained variable propagation for quantified

  bit-vectors}

$k$. In particular, if $i$ is the largest number for which $2^i$

divides the constant $k$ and the unconstrained variable $x$ has

bit-width $n$, the term $k \times x$ can be rewritten to

$extract_0^{n-i}(x) \cdot 0^i$.. This approach can be also extended to

$extract_0^{n-i}(x) \cdot 0^i$. This approach can be also extended to

the multiplication of two variables from which one is unconstrained. I

plan to investigate further extensions to the terms containing

division and remainder operations and to publish a paper concerning

% 1. Configure classicthesis for your needs here, e.g., remove "drafting" below

% in order to deactivate the time-stamp on the pages

% ****************************************************************************************************

\PassOptionsToPackage{eulerchapternumbers,listings,drafting,dottedtoc,

\PassOptionsToPackage{eulerchapternumbers,listings,dottedtoc,

					 %floatperchapter,%linedheaders,%

					 subfig,beramono,eulermath,minionprospacing}{classicthesis}

% ********************************************************************