Multiple changes

  booktitle = {13th International Workshop on Satisfiability Modulo

  booktitle = {13th International Workshop on Satisfiability Modulo

                 Theories (SMT 2015)},

                 Theories (SMT 2015)},

  year = 	 2015}

  year = 	 2015}

@inproceedings{FKB13,

  author    = {Andreas Fr{\"{o}}hlich and

               Gergely Kov{\'{a}}sznai and

               Armin Biere},

  title     = {More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics

               with Binary Encoding},

  booktitle = {Computer Science - Theory and Applications - 8th International Computer

               Science Symposium in Russia, {CSR} 2013, Ekaterinburg, Russia, June

               25-29, 2013. Proceedings},

  pages     = {378--390},

  year      = {2013}

}

@MISC{BST10,

  author =	 {Clark Barrett and Aaron Stump and Cesare Tinelli},

  title =	 {{The Satisfiability Modulo Theories Library (SMT-LIB)}},

  howpublished = {{\tt www.SMT-LIB.org}},

  year =	 2010,

}

@INCOLLECTION{BHB14,

  author = {Petr Bauch and Vojt\v{e}ch Havel and Ji\v{r}\'{\i} Barnat},

  title = {{LTL Model Checking of LLVM Bitcode with Symbolic Data}},

  booktitle = {{MEMICS} 2014},

  publisher = {Springer},

  year = 2014,

  volume = 8934,

  series = {LNCS},

  pages = {47--59},

}

@article{Bry91,

 author = {Bryant, Randal E.},

 title = {{On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication}},

 journal = {IEEE Trans. Comput.},

 volume = {40},

 number = {2},

 year = {1991},

 issn = {0018-9340},

 pages = {205--213},

 publisher = {IEEE Computer Society},

}

@inproceedings{Rud93,

  author    = {Richard Rudell},

  title     = {Dynamic variable ordering for ordered binary decision diagrams},

  booktitle = {Proceedings of the 1993 {IEEE/ACM} International Conference on Computer-Aided

               Design, 1993},

  pages     = {42--47},

  year      = {1993}

}

 No newline at end of file

Notable examples of decidable first-order theories include

Notable examples of decidable first-order theories include

\begin{itemize}

\begin{itemize}

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

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

  $\teuf$, which contains all structures that interpret the predicate

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

  $=$ as a congruence with respect to all other functions,

  congruence with respect to all other functions,

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

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

  of all structures from $\teuf$ that are isomorphic to the set of

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

  integers and interpret the function $+$ as addition and the

  predicates $\leq$ and $=$,

  predicate $\leq$ as the integer comparison;

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

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

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

  all structures from $\teuf$ that are isomorphic to real numbers and

  predicates $\leq$ and $=$,

  interpret the function $+$ as addition, and the predicate $\leq$ as

  the real comparison;

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

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

    real arithmetic, integer arithmetic with multiplication was shown

    real arithmetic, integer arithmetic with multiplication was shown

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

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

  from $\teuf$ that are isomorphic to real numbers and interpret the

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

  function $+$ as addition, $\times$ as multiplication, and the

  predicates $\leq$ and $=$,

  predicate $\leq$ as the real comparison;

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

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

  from $\teuf$ isomorphic to the set of arrays with a binary function

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

  $read(a, i)$ interpreted as a value in the index $i$ of the array

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

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

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

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

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

\item the theory of fixed-size bit-vectors.

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

\end{itemize}

\end{itemize}

For a detailed description of these theories and implementation of the

For a detailed description of these theories and implementation of the

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

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

to the equivalent propositional formula, which is subsequently solved

to the equivalent propositional formula, which is subsequently solved

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

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

equivalent propositional formula is traditionally called

equivalent propositional formula is traditionally called

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

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

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

bit-blasting is benefitial when the theory combination is

bit-blasting is benefitial when the theory combination is

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

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

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

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

reasoning and if the sub-solvers are not sufficient for deciding the

reasoning and if the sub-solvers are not sufficient for deciding the

satisfiability of the formula, theory lemmas and propagated literals

satisfiability of the formula, theory lemmas and propagated literals

generated by the sub-solvers are added to the formula and a lazy

generated by the sub-solvers are added to the formula and a lazy

\dpllt bit-blasting solver is

\dpllt bit-blasting solver is employed~\cite{HBJBT14}.

employed~\cite{HBJBT14}. \marginpar{TODO: Nepřidat odstavec o

  propagating-complete \cnf encodings?}

\subsection{Word-level techinques}

\subsection{Word-level techinques}

Although bit-blasting is highly efficient for most of practical

Although bit-blasting is highly efficient for most of practical

expanding all quantifiers with all possible bit-vector values of the

expanding all quantifiers with all possible bit-vector values of the

corresponding bit-width, this is rarely practical approach. Instead,

corresponding bit-width, this is rarely practical approach. Instead,

the formula is usually converted to a equisatisfiable formula by

the formula is usually converted to a equisatisfiable formula by

Skolemization and then instances of the universal quantifiers are

Skolemization and then instances of the universally quantified

lazily added to the formula until a model is found by a solver for

formulas are lazily added to the formula until a model is found or the

quantifier-free bit-vector formulas or the formula is found to be

formula is found to be unsatisfiable by a \QFBV solver. There are

unsatisfiable. There are multiple ways to choose quantifier instances

multiple ways to choose quantifier instances that are sufficient to

that are sufficient to decide the satisfiability of the formula. For

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

the bit-vector theory, the most widely used approach is the

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

\emph{model-based quantifier instantiation} approach~\cite{GM09},

  instantiation} approach~\cite{GM09}, supported by Z3, CVC4, and

supported by Z3, CVC4, and Yices, combined by heuristics as E-matching

Yices, combined by heuristics as E-matching or symbolic quantifier

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

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

for dealing with quantifiers, CVC4 supports solving quantified

quantifiers, CVC4 supports solving quantified formulas by

formulas by \emph{counter-example guided quantifier

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

  instantiation}~\cite{RDKT15}.

% and \emph{finite model finding}~\cite{RTG13}.

% and \emph{finite model finding}~\cite{RTG13}.

However, we describe only the model-based quantifier instantiation in

However, we describe only the model-based quantifier instantiation in

detail, as the counter-example guided quantifier considers all

detail, as the counter-example guided quantifier considers all

\subsection{Model-based quantifier instantiation}

\subsection{Model-based quantifier instantiation}

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

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

the formula to the negation normal form and apply Skolemization to

the formula to the negation normal form and apply Skolemization to

obtain equisatisfiable formula of the form

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

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

\[

\[

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

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

\]

\]

number of distinct models $M$ of $\varphi$. However, in some cases

number of distinct models $M$ of $\varphi$. However, in some cases

exponentially many such models have to be ruled out before the solver

exponentially many such models have to be ruled out before the solver

is able to find a correct model or decide unsatisfiability of the

is able to find a correct model or decide unsatisfiability of the

whole formula. To overcome this issue, state-of-the-art SMT solvers do

whole formula. To overcome this issue, state-of-the-art \smt solvers

not use just instances of the form $\psi[v_1, \dots, v_n]$ with

do not use just instances of the form $\psi[v_1, \dots, v_n]$ with

concrete values, but employ heuristics such as

concrete values, but employ mentioned heuristics such as E-matching or

E-matching~\cite{DNS05,MB07} or symbolic quantifier

symbolic quantifier instantiation to choose instances with ground

instantiation~\cite{WHD13} to choose instances with ground terms which

terms that can potentially rule out more spurious models and thus

can potentially rule out more spurious models and thus significantly

significantly reduce the number of iterations of the algorithm. In

reduce the number of iterations of the algorithm. In practice,

practice, suitable ground terms substituted for quantified variables

suitable ground terms substituted for quantified variables are

are selected only from subterms of the input formula.

selected only from subterms of the input formula.

Note that Skolemization introduces uninterpreted functions to the

Note that Skolemization introduces uninterpreted functions to the

quantified formulas of form other than

quantified formulas of form other than

$\exists^*\forall^*\varphi$. This class of formulas is usually called

$\exists^*\forall^*\varphi$. This class of formulas is usually called

\emph{exists/forall}, or simply $\exists\forall$. Therefore, for the

\emph{exists/forall}, or simply $\exists\forall$. Therefore, for the

model-based quantifier instantiation approach to be usable for

model-based quantifier instantiation approach to be usable for

formulas not from the exists/forall class, the underlying

formulas not from the exists/forall class, the underlying \QFBV solver

quantifier-free bit-vector solver has to support reasoning about

has to support reasoning about uninterpreted functions. In case of Z3,

uninterpreted functions. In case of Z3, this is achieved by

this is achieved by \emph{template-based model finding} --

\emph{template-based model finding} -- uninterpreted functions are

uninterpreted functions are assigned templates and the \QFBV solver is

assigned templates and the quantifier-free \smt solver is used to find

used to find satisfying parameters of these templates. For example, an

parameters of these templates, which satisfy the formula. For example,

uninterpreted function $f$ may be assigned a template for linear

an uninterpreted function $f$ may be assigned a linear template

functions $f(x) = ax + b$ and finding a satisfying function $f$

$f(x) = ax + b$ and finding a model of $f$ reduces to finding

reduces to finding values $a$ and $b$.

parameters $a$ and $b$.

\section{Computational complexity}

\section{Computational complexity of bit-vector logics}

The propositional satisfiability problem is well known from the

The propositional satisfiability problem is well known from the

computational complexity perspective, as it is the first problem that

computational complexity perspective, as it is the first problem that

was shown to be \NP-complete. The complexity of the satisfiability

was shown to be \NP-complete. The complexity of the satisfiability

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

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

bit-widths are denoted by suffixes 1 and 2, respectively. For example,

bit-widths are denoted by suffixes 1 and 2, respectively. For example,

QF\_UFBV2 is the decision problem for quantifier free formulas with

QF\_UFBV2 is the decision problem for quantifier free formulas with

uninterpreted functions and binary encoded bit-withs.

uninterpreted functions and binary encoded bit-withs. The completeness

results for these classes are summarized in table

\ref{tbl:complexity}, and briefly explained in the rest of this section.

\begin{table}

\checkoddpage

\edef\side{\ifoddpage l\else r\fi}

\makebox[\textwidth][\side]{

\begin{minipage}[bt]{\fullwidth}

  \begin{center}

    \setlength{\tabcolsep}{0.6em}

    \begin{tabularx}{\textwidth}{l l l l X l r}

      \toprule

      & & \multicolumn{5}{c}{Quantifiers} \\

      \cmidrule(l){3-7}

      & & \multicolumn{2}{c}{No} & & \multicolumn{2}{c}{Yes} \\

      \cmidrule(l){3-4}

      \cmidrule(l){6-7}

      & & \multicolumn{2}{c}{Uninterpreted functions} & & \multicolumn{2}{c}{Uninterpreted functions} \\

      & & \multicolumn{1}{c}{No} & \multicolumn{1}{c}{Yes} & & \multicolumn{1}{c}{No} & \multicolumn{1}{c}{Yes} \\

      \midrule

      \multirow{2}{*}{Encoding~} & Unary & \NP & \NP & & \PSPACE & \NEXPTIME \\

       & Binary\hspace{2em} & \NEXPTIME & \NEXPTIME & & ? & \NNEXPTIME \\

      \bottomrule

    \end{tabularx}

  \end{center}

  \caption{Completeness results for various bit-vector logics and encodings~\cite{FKB13}.}

  \label{tbl:complexity}

\end{minipage}}

\end{table}

\paragraph{Unary encoded bit-widths} The bit-blasting yields a

\paragraph{Unary encoded bit-widths} The bit-blasting yields a

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

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

%\setcounter{page}{90}

%\setcounter{page}{90}

% use \cleardoublepage here to avoid problems with pdfbookmark

% use \cleardoublepage here to avoid problems with pdfbookmark

\cleardoublepage

\cleardoublepage

\newlength\fullmarginwidth

\fullmarginwidth=\marginparwidth

\advance\fullmarginwidth by \marginparsep

\newlength\fullwidth

\fullwidth=\textwidth

\advance\fullwidth by \fullmarginwidth

\include{Chapters/Chapter01}

\include{Chapters/Chapter01}

\include{Chapters/Chapter02}

\include{Chapters/Chapter02}

%\addtocontents{toc}{\protect\clearpage} % <--- just debug stuff, ignore

%\addtocontents{toc}{\protect\clearpage} % <--- just debug stuff, ignore

\thispagestyle{empty}

\thispagestyle{empty}

\hfill

%\hfill

\vfill

%\vfill

\noindent\myName: \textit{\myTitle,} \mySubtitle, %\myDegree, 

%\noindent\myName: \textit{\myTitle,} \mySubtitle, %\myDegree,

\textcopyright\ \myTime

%\textcopyright\ \myTime

%\bigskip

%\bigskip

%

%