First draft of unconstrained variables

which allows computing values of bit-vector variables.

\subsection{Preprocessing}

For both bit-blasting and word-level approaches, a preprocessing of

the input formula is necessary for the performance of the

solver. Therefore, modern SMT solvers employ hundreds of rewrite rules

in order to simplify the input formula. Franzén describes several

simplifications implemented in the MathSAT5 solver: canonization,

unconstrained variables propagation, packet splitting, and disjunctive

partitioning. From those simplifications, we describe propagation of

unconstrained variables in more detail, since it is highly relevant

for software verification.

A variable $x$ in the given formula is called \emph{unconstrained} if

it occurs only once in the formula. It was observed independently by

Brummayer~\cite{Brum10} and Bruttomesso~\cite{Bru08} that if an

unconstrained variable occurs as an argument to a function symbol,

which can be \emph{inverted} with respect to this argument, replacing

this function with a fresh variable yields a equi-satisfiable

formula. 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$. The

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 equi-satisfiable formula $v = 0$, where $v$

is a fresh variable, since $x$ is unconstrained in $\varphi$.

%Brummayer and Bruttomesso have

%independently observed that unconstrained variables can be used to

%simplify the given formula.

\section{Satisfiability of quantified bit-vector formulas}