Bit-vectors - work in progress

  year={2001},

  publisher={Harcourt/Academic Press}

}

@phdthesis{Had15,

  author       = {Liana Hadarean},

  title        = {{An Efficient and Trustworthy Theory Solver for Bit-vectors in Satisfiability Modulo Theories}},

  school       = {New York University},

  year         = 2015

}

@book{Kro08,

  author    = {Daniel Kroening and

               Ofer Strichman},

  title     = {Decision Procedures - An Algorithmic Point of View},

  series    = {Texts in Theoretical Computer Science. An {EATCS} Series},

  publisher = {Springer},

  year      = {2008},

  isbn      = {978-3-540-74104-6}

}

@inproceedings{HBJBT14,

  author    = {Liana Hadarean and

               Kshitij Bansal and

               Dejan Jovanovic and

               Clark Barrett and

               Cesare Tinelli},

  title     = {A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors},

  booktitle = {Computer Aided Verification - 26th International Conference, {CAV}

               2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,

               Austria, July 18-22, 2014. Proceedings},

  pages     = {680--695},

  year      = {2014}

}

@article{Boolector,

  title={Boolector 2.0 system description},

  author={Aina Niemetz and Mathias Preiner and Armin Biere},

  journal={Journal on Satisfiability, Boolean Modeling and Computation},

  volume={9},

  pages={53-58},

  year={2014 (published 2015)},

  publisher={IOS Press},

}

@inproceedings{ZWR16,

  author    = {Aleksandar Zeljic and

               Christoph M. Wintersteiger and

               Philipp R{\"{u}}mmer},

  title     = {Deciding Bit-Vector Formulas with mcSAT},

  booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2016 - 19th

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

  pages     = {249--266},

  year      = {2016}

}

@inproceedings{FBWH15,

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

               Armin Biere and

               Christoph M. Wintersteiger and

               Youssef Hamadi},

  title     = {Stochastic Local Search for Satisfiability Modulo Theories},

  booktitle = {Proceedings of the Twenty-Ninth {AAAI} Conference on Artificial Intelligence,

               January 25-30, 2015, Austin, Texas, {USA.}},

  pages     = {1136--1143},

  year      = {2015}

}

@inproceedings{NPBF15,

  author     = {Aina Niemetz and

                Mathias Preiner and

		Armin Biere and

		Andreas Fr{\"{o}}hlich},

  title      = {Improving Local Search For Bit-Vector Logics in {SMT} with Path Propagation},

  booktitle  = {Proc.~4th Intl.~Work.~on Design and Implementation of Formal Tools and Systems ({DIFTS'15})},

  pages      = {10 pages},

  year       = {2015},

}

@inproceedings{NPB16,

  author    = {Aina Niemetz and

               Mathias Preiner and

               Armin Biere},

  title     = {Precise and Complete Propagation Based Local Search for Satisfiability

               Modulo Theories},

  booktitle = {Computer Aided Verification - 28th International Conference, {CAV}

               2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part {I}},

  pages     = {199--217},

  year      = {2016}

}

 No newline at end of file

\section{Satisfiability of quantifier-free bit-vector formulas}

The \emph{theory of fixed sized bit-vectors (\BV)} is a multi-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$, representing equality,

unsigned inequality of binary-encoded natural numbers, and signed

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

respectively. Functions symbols in the theory are

$+, \times, \div, \&, \mid, \oplus, \ll, \gg, \cdot, \extract{n}{p}$,

representing 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 position $p$,

respectively. For 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

preprocessing, and eager or lazy translation of the bit-vector formula

to the equivalent propositional formula, which is subsequently solved

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

propositional formula is traditionally called

\emph{bit-blasting}~\cite{Kro08}. The lazy bit-blasting is benefitial

when the theory combination is required. For example, Z3 and Yices

apply bit-blasting to all operations except for the equality, which is

handled by a specialized solver, and dynamically add axioms of the

array theory~\cite{Z3,Yices}, and Boolector applies bit-blasting to

the bit-vector operations and lazily instantiates definitions of

macros and the array axioms~\cite{Boolector}. Furthermore, CVC4 uses

lazy and layered solver, which tries to decide the satisfiability

using possibly faster but incomplete sub-solvers for equality and

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

deciding the satisfiability of the formula, theory lemmas and

propagated literals generated by the sub-solvers are added to the

formula and a lazy \dpllt bit-blasting solver is

employed~\cite{HBJBT14}.

\subsection{Word-level techinques}

Although bit-blasting is highly effective for most of practical

problems, it can exhaust memory if the input formula contains complex

arithmetic or variables with large bit-width. Several techniques,

which operate on the word-level, have been proposed to alleviate this

problem.

Recently, an instance of the model-constructing satisfiability

calculus introduced in subsection ??? was implemented by Zeljić et

al. in the solver \mcbv~\cite{ZWR16}. They have extended the \mcsat

framework by the ability to perform partial assignments and proposed

heuristics for generalizing explanations of bit-vector conflicts. For

example, the \mcsat solver can perform the partial assignment

$\extract{2}{0}(x) \mapsto 10$, denoting that the two least

significant bits of $x$ are $10$. To be able to efficiently use such

partial assignments, the \mcbv solver mantains an over-approximation

of the set of models which are compatible with the current partial

assignment using bit-patterns and arithmetic intervals. Bit-patterns

are sequences of $0$, $1$ and $u$, which represent undefined bits, and

constrain the values of particular bits in the assignment. Arithmetic

intervals are pairs of bit-vector values representing lower and upper

bounds and constrain integral values of bit-vectors. Both bit-patterns

and arithmetic intervals can be ordered to form a lattice, in which

the solver performs a search if a conflict is detected in order to

generalize from the conflict.

Another word-level approach is \emph{stochastic local search} (\sls),

proposed for solving bit-vectors by Frohlich et al.~\cite{FBWH15} and

subsequently improved by Niemetz et al~\cite{NPBF15,NPB16}. In the

\sls approach, the solver randomly chooses initial values of

bit-vector variables and tries to find an satisfying assignment by

performing random bit changes guided by the scoring function based on

the satisfaction of subformulas of the input formula. Niemetz et

al. have improved the \sls technique with the propagation strategy,

which allows computing values of bit-vector variables.

\subsection{Preprocessing}

\section{Satisfiability of quantified bit-vector formulas}

\section{Computational complexity}

\newcommand{\bdd}{\textsc{bdd}\xspace}

\newcommand{\robdd}{\textsc{robdd}\xspace}

\newcommand{\dpllt}{\textsc{dpll(t)}\xspace}

\newcommand{\sls}{\textsc{sls}\xspace}

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

%solvers

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

\newcommand{\fail}{\textsf{Fail}\xspace}

\newcommand{\trans}[2]{#1 ~\Longrightarrow~ #2}

\newcommand{\transstar}[2]{#1 ~\Longrightarrow^*~ #2}

%bv

\newcommand{\BV}{\ensuremath{\mathcal{BV}}\xspace}

\newcommand{\QFBV}{\ensuremath{\mathcal{QFBV}}\xspace}

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

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

 No newline at end of file