On solving quantified bit-vector constraints using invertibility conditions

Abstract

We present a novel approach for solving quantified bit-vector constraints in Satisfiability Modulo Theories (SMT) based on computing symbolic inverses of bit-vector operators. We derive conditions that precisely characterize when bit-vector constraints are invertible for a representative set of bit-vector operators commonly supported by SMT solvers. We utilize syntax-guided synthesis techniques to aid in establishing these conditions and verify them independently by using several SMT solvers. We show that invertibility conditions can be embedded into quantifier instantiations using Hilbert choice expressions and give experimental evidence that a counterexample-guided approach for quantifier instantiation utilizing these techniques leads to performance improvements with respect to state-of-the-art solvers for quantified bit-vector constraints.

1 Introduction

Many applications in hardware and software verification rely on Satisfiability Modulo Theories (SMT) solvers for bit-precise reasoning. In recent years, the quantifier-free fragment of the theory of fixed-size bit-vectors has received a lot of interest. This is witnessed by the number of applications that generate problems in that fragment, and by past editions of the annual SMT competition where the corresponding division consistently attracts the highest number of solver and benchmark entries. Modeling properties of programs and circuits, e.g., universal safety properties and program invariants, however, often requires the use of quantified bit-vector formulas. Despite a multitude of applications, reasoning efficiently about such formulas is still a major challenge for automated tools.

The majority of solvers that support quantified bit-vector logics rely on instantiation-based techniques [8, 25, 27, 30], which aim to find conflicting quantifier-free instances of universally quantified formulas in the input problem, with the goal of proving the problem unsatisfiable. For that, it is crucial to select good instantiations for the quantified variables, or else the solver may be overwhelmed by the number of quantifier-free instances generated. For example, consider the (unsatisfiable) quantified formula

$$\begin{aligned} \psi = \forall x.\,(x + {s} \not \approx t) \end{aligned}$$

where x, s, and t denote bit-vectors of, say, size 32, and x occurs neither in s nor in t. To prove that $\psi$ is unsatisfiable we can instantiate x with all $2^{32}$ possible bit-vector values. However, ideally, we would like to find a proof that requires much fewer instantiations. In this example, if we instantiate x with the term $t - s$, denoting the unique solution of the equation $x + s \approx t$ for the variable x, we can immediately conclude that $\psi$ is unsatisfiable since $(t - s) + s \not \approx t$ simplifies to false.

If we look at the term $x + s$ above as the bit-vector function $\lambda x.\,{x + s}$, we observe that the function is invertible, with inverse $\lambda y.\,{y - s}$. Informally then, we say that the bit-vector operator $+$ is invertible in its first argument. In particular, it is always invertible in that argument since the equation ${x + s} \approx t$ is always solvable for x. Since the same argument applies to the term $s + x$, the operator $+$ is always invertible in its second argument as well.

Not all the operators in the theory of bit-vectors are invertible in this sense. However, it is possible to identify quantifier-free conditions on one of their arguments that precisely characterize when they are invertible in that argument. For example, the constraint $x \cdot s \approx t$ is solvable for x if and only if the constraint $(- s \mid s) \mathrel { \& } t \approx t$ is satisfiable. This is in fact a general property of bit-vector multiplication that always holds (for any bit-vector size n) for x, s and t [23]. The invertibility condition $(- s \mid s) \mathrel { \& } t \approx t$ essentially states that the value of t has at least as many right-most zeroes in its binary representation as the value of s.

We have identified invertibility conditions for a representative set of operators in the standard theory of bit-vectors supported by SMT solvers. We present a novel approach for quantifier instantiation of bit-vector formulas that utilizes those invertibility conditions to generate symbolic instantiations. As an example, consider the quantified formula $\varphi = \forall x.\,(x \cdot {s} \not \approx t)$. If the above invertibility condition $(- s \mid s) \mathrel { \& } t \approx t$ is unsatisfiable, we conclude that $\varphi$ is satisfiable since there is no x that makes its body $x \cdot {s} \not \approx t$ false. On the other hand, if the invertibility condition is satisfiable, we know there is some bit-vector value b such that ${b \cdot s \approx t}$ holds. Instantiating x in $\varphi$ with any term k denoting b to produce the quantifier-free formula ${k \cdot s \not \approx t}$ suffices to show that $\varphi$ is unsatisfiable. In general, the term k can be always generated automatically from the invertibility condition by using the Hilbert choice operator. Formally, we show that invertibility conditions can be embedded into quantifier instantiations using Hilbert’s choice function in a sound manner. This approach has compelling advantages with respect to previous approaches, as demonstrated by our experimental results.

More specifically, this paper makes the following contributions.

• We derive and present invertibility conditions for a representative set of bit-vector operators that allow us to model all bit-vector constraints in the theory of bit-vectors defined by the SMT-LIB standard. [3].

• We provide details on how invertibility conditions can be automatically synthesized using syntax-guided synthesis (SyGuS) [1] techniques, and make public 162 available challenge problems for SyGuS solvers that are encodings of this task.

• We prove that our approach can efficiently reduce a class of quantified formulas, which we call unit linear invertible, to quantifier-free constraints.

• Leveraging invertibility conditions, we implement a novel quantifier instantiation scheme as an extension of the SMT solver CVC4 [2], which shows substantial improvements over state-of-the-art solvers for quantified bit-vector constraints.

An earlier version of this work appeared at CAV 2018, held as part of FLOC, in Oxford, UK [22]. This article extends that work with a more thorough description and listing of invertibility conditions in Sect. 3, formal proofs of all lemmas and theorems throughout, new implementation details in Sect. 4.2 and further details on our evaluation in Sect. 5.

Related work. Quantified bit-vector logics are currently supported by the state-of-the-art SMT solvers Boolector [19], CVC4 [2], Yices 2 [7], and Z3 [6] and a Binary Decision Diagram (BDD)-based tool called Q3B [16]. Out of these, only CVC4 and Z3 provide support for combining quantified bit-vectors with other theories, e.g., the theories of arrays or real arithmetic. Arbitrarily nested quantifiers are handled by all but Yices 2, which only supports bit-vector formulas of the form $\exists \varvec{x} \forall \varvec{y}.\,Q[\varvec{x}, \varvec{y} ]$ [8]. For quantified bit-vectors, CVC4 employs counterexample-guided quantifier instantiation (CEGQI) [27], where concrete models of a set of quantifier-free instances and the negation of the input formula (the counterexamples) serve as instantiations for the universal variables. In Z3, model-based quantifier instantiation (MBQI) [12] is combined with a template-based model finding procedure [30]. In contrast to CVC4, Z3 not only relies on concrete counterexamples as candidates for quantifier instantiation but generalizes these counterexamples to generate symbolic instantiations by selecting quantifier-free terms with the same model value. Boolector employs a syntax-guided synthesis approach to synthesize interpretations for Skolem functions based on a set of quantifier-free instances of the formula, and uses a counterexample refinement loop similar to MBQI [25]. Other counterexample-guided approaches for quantified formulas in SMT solvers have been considered by Bjørner and Janota [4] and by Reynolds et al. [28], but they have mostly targeted quantified linear arithmetic and do not specifically address bit-vectors. Quantifier elimination for a fragment of bit-vectors that covers modular linear arithmetic has been recently addressed by John and Chakraborty [15]. We do not explore approaches for quantifier elimination in this paper.

2 Preliminaries

We assume the usual notions and terminology of many-sorted first-order logic with equality (denoted by $\approx$) (see, e.g., [11, 18]). Let $S$ be a set of sort symbols, and for every sort ${\sigma \in S}$, let $X _{\sigma }$ be an infinite set of variables of sort $\sigma$. We assume that sets $X _{\sigma }$ are pairwise disjoint and define $X$ as the union of sets $X _{\sigma }$. Let $\varSigma$ be a signature consisting of a set $\varSigma ^s \!\subseteq S$ of sort symbols and a set $\varSigma ^f$ of interpreted (and sorted) function symbols $f^{\sigma _1 \cdots \sigma _n \sigma }$ with arity $n \ge 0$ and $\sigma _1, ..., \sigma _n, \sigma \in \varSigma ^s$. We assume that a signature $\varSigma$ includes a Boolean sort $\mathsf {Bool}$ and the Boolean constants $\top$ (true) and $\bot$ (false). A $\varSigma$-interpretation maps: each $\sigma \in \varSigma ^s$ to a non-empty set $\sigma ^{{\mathcal {I}}}$ (the domain of ${{\mathcal {I}}}$), with $\mathsf {Bool} ^{{\mathcal {I}}} = \{ \top , \bot \}$; each $x \in X _{\sigma }$ to an element ${x^{{\mathcal {I}}} \in \sigma ^{{\mathcal {I}}} }$; and each $f^{\sigma _1 \cdots \sigma _n \sigma } \in \varSigma ^f$ to a total function $f^{{\mathcal {I}}} \!\!: \sigma _1^{{\mathcal {I}}} \times ... \times \sigma _n^{{\mathcal {I}}} \rightarrow \sigma ^{{\mathcal {I}}}$ if $n > 0$, and to an element in $\sigma ^{{\mathcal {I}}}$ if $n = 0$. If $x \in X_\sigma$ and $v \in \sigma ^{{\mathcal {I}}}$, we denote by ${{\mathcal {I}}} [x \mapsto v]$ the interpretation that maps x to v and is otherwise identical to ${{\mathcal {I}}}$. We assume the usual definition of well-sorted terms, literals, and formulas (where formulas are terms of sort $\mathsf {Bool}$) with variables in $X$ and symbols in $\varSigma$, and refer to them as $\varSigma$-terms, $\varSigma$-atoms, and so on. We also assume the usual definition of free variables of a formula. A closed formula is a $\varSigma$-formula without free variables. We adopt the usual inductive definition of the meaning, or value, $t^{{\mathcal {I}}}$ of a $\varSigma$-term t in a $\varSigma$-interpretation ${{\mathcal {I}}}$ and of the satisfiability relation $\models$ between $\varSigma$-interpretations and $\varSigma$-formulas.

2.1 Notation

We denote by $\mathrm {Lit}(\varphi )$ the set of $\varSigma$-literals that either appear in, or are negations of atomic formulas appearing in, $\varSigma$-formula $\varphi$. Let $\varvec{x} = (x_1, ..., x_n)$ be a (possibly empty) tuple of distinct variables. We write $Q\varvec{x}.\varphi$ with $Q \in \{ \forall , \exists \}$ for a quantified formula $Qx_1 \cdots Qx_n. \varphi$. For a $\varSigma$-term or $\varSigma$-formula e, we denote the free variables of e (defined as usual) as ${FV}(e)$; we write $e[\varvec{x} ]$ to indicate that the variables of $\varvec{x}$ occur free in e (i.e., $\varvec{x} \subseteq {FV}(e)$); in addition, if $\varvec{t} = (t_1, ..., t_n)$ is a tuple of $\varSigma$-terms, $e\{\varvec{x} \mapsto \varvec{t} \}$ denotes the term or formula obtained from e by simultaneously replacing each occurrence of $x_i$ in e by $t_i$ for $i=1,\ldots ,n$. Abusing the notation, when the relevant free variables $\varvec{x}$ of e are clear from context, we write $e[\varvec{t} ]$ as an abbreviation of $e\{\varvec{x} \mapsto \varvec{t} \}$. When convenient, we identify a finite set of formulas with the conjunction of its elements.

Given a $\varSigma$-formula $\varphi [x]$ with $x \in X _{\sigma }$, we use Hilbert’s choice operator $\varepsilon$ [14] to describe values (i.e. domain elements) for x for which $\varphi [x]$ is satisfiable. Formally, we define a choice term $\varepsilon x.\,\varphi$ as a term of sort $\sigma$ where x is bound by $\varepsilon$. In every interpretation ${{\mathcal {I}}}$, $\varepsilon x.\,\varphi$ denotes some value $v \in \sigma ^{{\mathcal {I}}}$ such that ${{\mathcal {I}}} [x \mapsto v]$ satisfies $\varphi$ if such values exist, and denotes an arbitrary element of $\sigma ^{{\mathcal {I}}}$ otherwise. This means that the formula $\exists x.\,\varphi [x] \Leftrightarrow \varphi [\varepsilon x.\,\varphi ]$ is satisfied by every interpretation. For example, in any interpretation ${{\mathcal {I}}}$ extending the standard interpretation of integer arithmetic, $\varepsilon x.\,x > 0$ denotes some integer greater than 0; $\varepsilon x.\,x > y$ denotes some value greater than $y^{{\mathcal {I}}}$. We remark that in the standard definition of the choice binder, the meaning of $\varepsilon x.\,\varphi$ is invariant modulo logical equivalence, that is, the equality $\varepsilon x.\,\varphi \approx \varepsilon x.\,\psi$ is satisfied by every interpretation in which the formulas $\varphi$ and $\psi$ are equivalent. However, the correctness of the work we present here does not rely on this invariant property.

We say that a formula is quantifier-free if it contains no quantifiers and is binder-free if it contains no quantifiers and no choice operators.

2.2 Theories

A theory T is a pair $(\varSigma , {I})$, where $\varSigma$ is a signature and ${I}$ is a non-empty class of $\varSigma$-interpretations (the models of T) that is closed under variable reassignment, i.e., every $\varSigma$-interpretation that only differs from an ${{{\mathcal {I}}} \in {I}}$ in how it interprets variables is also in ${I}$. A $\varSigma$-formula $\varphi$ is T-satisfiable (resp. T-unsatisfiable) if it is satisfied by some (resp. no) interpretation in ${I}$; it is T-valid if it is satisfied by all interpretations in ${I}$. Two $\varSigma$-formulas $\varphi$ and $\psi$ are T-equivalent if the formula $\varphi \Leftrightarrow \psi$ is T-valid. A set $\varGamma$ of $\varSigma$-formulas is T-satisfiable (resp., T-unsatisfiable) if there is an interpretation (resp., no interpretation) in ${I}$ that satisfies all the formulas in $\varGamma$. The set $\varGamma$ T-entails $\varphi$ if $\varGamma \cup \{ \lnot \varphi \}$ is T-unsatisfiable. A theory T is a complete theory if for all closed $\varSigma$-formulas $\varphi$, $\varphi$ is either T-valid or T-unsatisfiable. A choice term $\varepsilon x.\,\varphi$ is T-valid if $\exists x.\,\varphi$ is T-valid. We refer to a term t as $\varepsilon$-T-valid if all occurrences of choice terms in t are T-valid. We will sometimes omit T from the definitions above when the theory T is understood from context.

2.3 The theory of fixed-size bit-vectors

We will focus on the theory $T_{BV} = (\varSigma _{BV}, {I} _{BV})$ of fixed-size bit-vectors as defined by the SMT-LIB 2 standard [3]. The signature $\varSigma _{BV}$ includes a unique sort for each positive bit-vector width n, denoted here as $\sigma _{[n]}$. Similarly, $X _{[n]}$ is the set of bit-vector variables of sort $\sigma _{[n]}$, and $X _{BV}$ is the union of all sets $X _{[n]}$. We assume that $\varSigma _{BV}$ includes all bit-vector constants of sort $\sigma _{[n]}$ for each n and represent those constants as bit-strings of 0s and 1s. All interpretations ${{\mathcal {I}}} \in {I} _{BV}$ are identical except for the value they assign to variables.¹ They interpret sort and function symbols as specified in SMT-LIB 2. All function symbols in $\varSigma ^f _{BV}$ are overloaded for every $\sigma _{[n]} \! \in \varSigma ^s _{BV}$. We denote a $\varSigma _{BV}$-term (or bit-vector term) t of width n as $t_{[n]}$ when we want to specify its bit-width explicitly. We use $\text {max}_{s{[n]}}$ or $\text {min}_{s{[n]}}$ for the maximum or minimum signed value of width n, e.g., $\text {max}_{s{[4]}} = 0111$ and $\text {min}_{s{[4]}}=1000$. To simplify the notation we will sometimes denote bit-vector constants by the corresponding natural number in $\{0, \ldots , 2^{n-1}\}$ (with a number c corresponding to a bit-string b if b has value c when seen as a binary number), adding the bit-width as a subscript; e.g., we will use $2_{[4]}$ for 0010. The width of a bit-vector sort or term is given by the function $\kappa$, e.g., $\kappa (\sigma _{[n]}) = n$ and $\kappa (t_{[n]}) = n$. We will omit the bit-width from the notation when it is clear from the context or not important. We will use the letters s and t to denote bit-vector terms in general and the letters x and y to denote bit-vector variables.

Without loss of generality, we consider a restricted set of bit-vector function symbols (or bit-vector operators) $\varSigma ^f _{BV}$ as listed in Table 1. The selection of operators in this set is arbitrary but complete in the sense that it suffices to express all bit-vector operators defined in SMT-LIB 2. This means that our approach is not really restricted to this particular set of operators as it can be lifted to any other set of bit-vector operators.

Table 1 Set of considered bit-vector operators with SMT-LIB 2 syntax

3 Invertibility conditions for bit-vector constraints

This section formally introduces the concept of an invertibility condition and shows that such conditions can be used to construct symbolic solutions for a class of quantifier-free bit-vector constraints that satisfy a syntactic condition we call linearity.

Definition 1

(Linear Literal) A $\varSigma _{BV}$-literal $\ell [x]$ is linear in variable x if it has a single occurrence of x.

Consider a bit-vector literal $x + s \approx t$ and assume that we want to solve for x. If the literal is linear in x, a general solution for x is given by the inverse of bit-vector addition over equality: $x = t - s$. Computing the inverse of a bit-vector operation is not always possible. For example, recalling that the semantics of arithmetic operators over bit-vectors of size n is that of integer arithmetic modulo n, for literals of the form $x \cdot s \approx t$, an inverse always exists provided that s always evaluates to a bit-vector denoting an odd integer.² Otherwise, there are values for s and t where no such inverse exists, e.g., $x \cdot 2 \approx 3$.

Even if a bit-vector operation may admit no unconditional inverse in general, it is possible to identify the condition under which the operation is invertible. For instance, as we mentioned earlier, it is possible to prove that the multiplication constraint $x \cdot s \approx t$ with $x \notin {FV}(s) \cup {FV}(t)$ is invertible for x exactly when the number of right-most zeroes in s is no greater than the number of right-most zeroes in t. This invertibility condition can be expressed by the formula $(- s \mid s) \mathrel { \& } t \approx t$. Note that the operators $-$, ${\sim }\,$, and $+$ for which a general inverse always exists can be seen as having $\top$ as their invertibility condition.

Definition 2

(Invertibility Condition) Let $\ell [x]$ be a $\varSigma _{BV}$-literal. A binder-free $\varSigma _{BV}$-formula $\phi$ is an invertibility condition for x in $\ell$ if ${FV}(\phi ) \subseteq {FV}(\ell ) \setminus \{x\}$ and the formula $\phi \Leftrightarrow \exists x.\,\ell$ is $T_{BV}$-valid.

An invertibility condition for a literal $\ell [x]$ provides the exact conditions under which $\ell$ is solvable for x. We call it an “invertibility” condition because we can use Hilbert choice terms to express all such conditional solutions with a single symbolic term, that is, a term whose possible values are exactly the solutions for x in $\ell$. Recall that a choice term $\varepsilon x.\,\varphi$ denotes a solution of the formula $\varphi [x]$ for x if the formula is satisfiable, and denotes an arbitrary value otherwise. We can use the choice term $\varepsilon x.\,(\phi \Rightarrow \ell )$ to describe inverse solutions of a literal $\ell [x]$ with invertibility condition $\phi$. For example, for the general case of bit-vector multiplication over equality the choice term is defined as $\varepsilon x.\,((- s \mid s) \mathrel { \& } t \approx t \;\Rightarrow \; x \cdot s \approx t)$. We favor the choice term $\varepsilon x.\,(\phi \Rightarrow \ell )$ over the simpler choice term $\varepsilon x.\,\ell$ because $\phi \Rightarrow \ell$ has a solution in every model of $T_{BV}$, whereas $\ell$ may have no solution.

Lemma 3

Let $\phi$ be an invertibility condition for an $\varepsilon$-valid $\varSigma _{BV}$-literal $\ell [x]$ and let r be the term $\varepsilon x.\,(\phi \Rightarrow \ell )$. The term r is $\varepsilon$-valid and $\ell [r] \Leftrightarrow \exists x.\,\ell$ is $T_{BV}$-valid.

Proof

First, we show that $r = \varepsilon x.\,(\phi \Rightarrow \ell )$ is $\varepsilon$-valid, where $\phi$ is an invertibility condition for x in $\ell [x]$. To do so, since $\ell$ is $\varepsilon$-valid, we only need to show that $\exists x.\,\phi \Rightarrow \ell$ holds in all models of $T_{BV}$. Since $\phi$ is an invertibility condition for $\ell$, we have that $x \not \in {FV}(\phi )$, and hence, this formula is equivalent to $\phi \Rightarrow \exists x.\,\ell$. Let ${{\mathcal {I}}}$ be any model of $T_{BV}$ that satisfies $\phi$. Since $\phi$ is an invertibility condition for $\ell$, by Definition 2, ${{\mathcal {I}}}$ satisfies $\exists x.\,\ell$ as well. Thus, $\exists x.\,\phi \Rightarrow \ell$ holds in all models of $T_{BV}$, and hence, r is $\varepsilon$-valid.

To show $\ell [r] \Leftrightarrow \exists x.\,\ell$ where r is $\varepsilon x.\,(\phi \Rightarrow \ell )$, first consider direction $\exists x.\,\ell \Rightarrow \ell [r]$. Let ${{\mathcal {I}}}$ be any model of $T_{BV}$ that satisfies $\exists x.\,\ell$. By definition of $\varepsilon$, ${{\mathcal {I}}}$ also satisfies $\ell [\varepsilon x.\,\ell ]$. Since $\phi$ is an invertibility condition for $\ell$, from Def. 2 we have that $\phi \Leftrightarrow \exists x.\,\ell$ holds in all models of $T_{BV}$, and thus ${{\mathcal {I}}}$ also satisfies $\phi$. Hence, since ${{\mathcal {I}}}$ satisfies $\ell [\varepsilon x.\,\ell ]$, it also satifies $\ell [\varepsilon x.\,(\phi \Rightarrow \ell ) ]$, which is $\ell [r]$. Thus, $\exists x.\,\ell \Rightarrow \ell [r]$ is $T_{BV}$-valid. The other direction $\ell [r] \Rightarrow \exists x.\,\ell$ trivially holds in all models of $T_{BV}$.

$\square$

Intuitively, when $\ell [x]$ is satisfiable in some model of the theory, the value of the choice term $\varepsilon x.\,(\phi \Rightarrow \ell )$ in that model is a value for x that is a solution of $\ell$. Conversely, if $\ell$ is satisfiable under no conditions in some model, then the value of $\varepsilon x.\,(\phi \Rightarrow \ell )$ is still a solution for $\phi \Rightarrow \ell$ because $\phi$ is false in that model.

3.1 Solving linear invertible constraints

Now, suppose a $\varSigma _{BV}$-literal $\ell$ is linear in variable x, but x occurs arbitrarily deep in it. Consider, for example, a literal $s_1 \cdot (s_2 + x ) \approx t$ where x does not occur in $s_1$, $s_2$ or t. We can solve this literal for x by recursively computing the (possibly conditional) inverses of all bit-vector operations that involve x. That is, first we solve $s_1 \cdot x' \approx t$ for $x'$, where $x'$ is a fresh variable abstracting $s_2 + x$, which yields the choice term

$$ \begin{aligned} x' = \varepsilon y.\,((- s_1 \mid s_1) \mathrel { \& } t \approx t \Rightarrow s_1 \cdot y \approx t)\ . \end{aligned}$$

Then, we solve $s_2 + x \approx x'$ for x, which yields the solution

$$ \begin{aligned} x = x' - s_2 = \varepsilon y.\,((- s_1 \mid s_1) \mathrel { \& } t \approx t \Rightarrow s_1 \cdot y \approx t) - s_2\ . \end{aligned}$$

Fig. 1

Function $\mathsf {solve}$ for constructing a symbolic solution for x given a linear literal $e[x] \bowtie t$

Figure 1 describes in pseudocode the procedure to solve for x in an arbitrary literal $\ell [x] = e[x] \bowtie t$ that is linear in x. We assume that e[x] is built over the set of bit-vector operators listed in Table 1. Function $\mathsf {solve}$ recursively constructs an analytic solution by computing (conditional) inverses as follows. Let function $\mathsf {getInverse} (x, \ell [x])$ (see Table 2) return a term $t'$ that is the inverse of x in $\ell$, i.e., such that the equivalence $\ell \Leftrightarrow x \approx t'$ is valid. Furthermore, let function $\mathsf {getIC} (x, \ell [x])$ return the invertibility condition $\phi$ for x in $\ell$. If e[x] has the form $\diamond (e_1, \ldots , e_n)$ with $n > 0$, x must occur in exactly one of the subterms $e_1, \ldots , e_n$ given that e is linear in x. Let d be the term obtained from e by replacing $e_i$ (the subterm containing x) with a fresh variable $x'$. We solve for subterm $e_i[x]$, treating it as a variable $x'$, and compute an inverse $\mathsf {getInverse} (x', d[x'] \approx t)$, if it exists. Note that for a disequality $e \not \approx t$, it suffices to compute the inverse over equality and propagate the disequality down. (For example, for $e_i[x] + s \not \approx t$, we compute the inverse $t' = \mathsf {getInverse} (x', x'+ s \approx t) = t - s$ and recurse on $e_i[x] \not \approx t'$.) If no inverse for $e[x] \bowtie t$ exists, we determine the invertibility condition $\phi$ for $d[x']$ via $\mathsf {getIC} (x', d[x'] \bowtie t)$, construct the choice term $\varepsilon y.\,(\phi \Rightarrow d[y] \bowtie t)$, and set it equal to $e_i[x]$, before recursively solving for x. If $e = x$ and the given literal is an equality, we have reached the base case and return t as the solution for x. Note that in Fig. 1, for simplicity, we omitted one case for which an inverse can be determined, namely $x \cdot c \approx t$ where c is an odd constant.

Definition 4

(Linear Invertible Literal) Literal $\diamond (e_1, \ldots , e_i[x], \ldots , e_n) \bowtie t$ is linear invertible in x if it is linear in x and if for each function application in $e_i[x]$, if one of its arguments contains x, then the function operator is in $\{ -, +, {\sim }\, \}$.

In other words, only the topmost function symbol $\diamond$ in a linear invertible literal may be conditionally invertible. For example, $(s+x) \cdot t \approx r$ and $s \cdot (t + x) <_\mathrm {u} r$ are linear invertible in x whereas $(s \mid x) \cdot t \approx r$ and $(s \cdot x)+t <_\mathrm {u} r$ are not. Note that some equalities such as $(x \cdot s)+t \approx r$ are not linear invertible by this definition, but can easily be shown to be equivalent to linear invertible ones, i.e. $x \cdot s \approx r-t$.

Lemma 5

If x occurs only beneath operators that are always invertible in e[x], then for any term t not containing x, $\exists x.\,e[x] \approx t$ is equivalent to $\top$.

Proof

The proof is by induction on the structure of e[x]. In the base case, if e[x] is x, then the statement holds trivially. For the inductive case, assume it is true for some e[x]. Let $e'[x]$ be $\diamond (\ldots , e[x], \ldots )$. Since $\diamond$ is always invertible, $\exists x.\,e'[x] \approx t$ is equivalent to $\exists x.\,e[x] \approx t'$, for some $t'$ not containing x. But this is equivalent to $\top$ by the induction hypothesis.

$\square$

The procedure $\mathsf {solve}$ is correct in the following sense.

Theorem 6

Let $\ell [x]$ be an $\varepsilon$-valid $\varSigma _{BV}$-literal linear in x, and let $r = \mathsf {solve} (x,\ell )$ be the term returned by function $\mathsf {solve}$. Then (i) r is $\varepsilon$-valid, (ii) ${FV}(r) \subseteq {FV}(\ell ) \setminus \{ x \}$ and (iii) $\ell [r] \Leftrightarrow \exists x.\,\ell$ is $T_{BV}$-valid when $\ell [x]$ is linear invertible in x.

Proof

We assume without loss of generality that $\ell [x]$ is of the form $e[x] \bowtie t$. Since $\ell$ is linear with respect to x, we have that $x \not \in {FV}(t)$. We show all statements of the theorem by structural induction on the term e[x].

Consider the case when e is x, which implies that $e \bowtie t$ is linear invertible in x. If $\bowtie$ is $\approx$, then r is t. We have that r is $\varepsilon$-valid, $x \not \in {FV}(r)$ since $x \not \in {FV}(t)$ and $t \approx t \Leftrightarrow \exists x.\, x \approx t$ holds, i.e. is satisfied, by all models of $T_{BV}$. Otherwise, when $\bowtie$ is not $\approx$, we have that r is $\varepsilon y.\,(\psi \Rightarrow y \bowtie t)$ where $\psi$ is $\mathsf {getIC} (x', x' \bowtie t)$. By definition of $\mathsf {getIC}$, we have that ${FV}(\psi ) \subseteq {FV}(t)$, and hence, ${FV}(r)$ is a subset of ${FV}(t)$, which is equal to ${FV}( \ell [x] ) \setminus \{ x \}$. Furthermore, since $\psi$ is an invertibility condition for $x'$ in $x' \bowtie t$, by Lemma 3, r is $\varepsilon$-valid and $r \bowtie t \Leftrightarrow \exists x.\,x \bowtie t$ is $T_{BV}$-valid.

Otherwise, e must be of the form $\diamond (e_1, ..., e_i[x], ..., e_n)$ for $n > 0$, where $x \not \in {FV}(e_j)$ for each $i \ne j$. Let $d[x']$ be $\diamond (e_1, ..., e_{i-1}, x', e_{i+1}, ... e_n)$, where notice that $x \not \in {FV}(d[x'])$. We have that r is $\mathsf {solve} (x, e_i[x] \bowtie _i t_i )$ for some relation $\bowtie _i$ and term $t_i$, where $t_i$ is $\mathsf {getInverse} (x', d[x'] \approx t)$ or $\varepsilon y.\,(\mathsf {getIC} (x', d[x'] \bowtie t) \Rightarrow d[y] \bowtie t)$. In both cases, by definition of $\mathsf {getInverse}$ (see Table 2) and $\mathsf {getIC}$, we have that $t_i$ is $\varepsilon$-valid due to Lemma 3 and since $\ell$ is $\varepsilon$-valid. Also, in both cases, we have that ${FV}(t_i) \subseteq {FV}(t) \cup {FV}(d[x']) \setminus \{ x' \} \subseteq {FV}(\ell ) \setminus \{ x \}$. Since $e \bowtie t$ is $\varepsilon$-valid and linear invertible in x and $x \not \in {FV}(t_i)$, the literal $e_i \bowtie _i t_i$ is $\varepsilon$-valid and linear invertible in x as well. Thus, by the induction hypothesis, we have that r is $\varepsilon$-valid, ${FV}(r) \subseteq {FV}(e_i[x] \bowtie _i t_i) \setminus \{ x \}$ and the formula $e_i[r] \bowtie _i t_i \Leftrightarrow \exists x.\,e_i[x] \bowtie _i t_i$ holds in all models of $T_{BV}$.

Property (i) holds since r is $\varepsilon$-valid. To show property (ii), since ${FV}(r) \subseteq {FV}(e_i \bowtie _i t_i) \setminus \{ x \}$ and since ${FV}(e_i) \subseteq {FV}(\ell )$ and ${FV}(t_i) \subseteq {FV}(\ell )$, we have that ${FV}(r) \subseteq {FV}(\ell ) \setminus \{ x \}$.

It remains to show property (iii), that $e[r] \bowtie t \Leftrightarrow \exists x.\,e \bowtie t$ is $T_{BV}$-valid when $e[x] \bowtie t$ is linear invertible in x. In the case that $\bowtie \;\in \{\approx , \not \approx \}$ and $\diamond \in \{ {\sim }\,, -, + \}$, we have that $\bowtie _i$ is $\bowtie$ and $t_i$ is $\mathsf {getInverse} (x', d[x'] \approx t)$. By definition of $\mathsf {getInverse}$ and since $\bowtie \;\in \{\approx , \not \approx \}$, we have that $e_i \bowtie t_i$ and $d[e_i] \bowtie t$ are equivalent. Since $d[e_i] = e$, the latter literal is $e \bowtie t$. Thus, since $e_i[r] \bowtie t_i \Leftrightarrow \exists x.\,e_i \bowtie t_i$, we have that $e[r] \bowtie t \Leftrightarrow \exists x.\,e \bowtie t$. Otherwise, let $\psi = \mathsf {getIC} (x', d[x'] \bowtie t)$; we have that $\bowtie _i$ is $\approx$ and $t_i$ is $\varepsilon y.\,(\psi \Rightarrow d[y] \bowtie t)$. Since $\psi$ is an invertibility condition for $x'$ in $d[x'] \bowtie t$, by Lemma 3, we have that $d[t_i] \bowtie t \Leftrightarrow \exists x'.\,d[x'] \bowtie t$ holds in all models of $T_{BV}$. Clearly $e[r] \bowtie t \Rightarrow \exists x.\,e \bowtie t$ holds in all models of $T_{BV}$. To show the other direction of the implication, consider any model ${{\mathcal {I}}}$ of $T_{BV}$ that satisfies $\exists x.\,e \bowtie t$. Since $e = d[e_i]$, we have that ${{\mathcal {I}}}$ satisfies $\exists x'.\,d[x'] \bowtie t$ as well. Thus, since $d[t_i] \bowtie t \Leftrightarrow \exists x'.\,d[x'] \bowtie t$ holds in all models of $T_{BV}$, we have that ${{\mathcal {I}}}$ satisfies $d[t_i] \bowtie t$. Since e[x] is linear invertible in x, we have that x occurs only under operators that are always invertible in $e_i[x]$, and thus by Lemma 5, $\exists x.\,e_i[x] \approx t_i$ is equivalent to $\top$. Since $e_i[r] \approx t_i \Leftrightarrow \exists x.\,e_i[x] \approx t_i$ holds by the induction hypothesis, we have that ${{\mathcal {I}}}$ satisfies $e_i[r] \approx t_i$. Since ${{\mathcal {I}}}$ satisfies $d[t_i] \bowtie t$, we have that it also satisfies $d[e_i[r]] \bowtie t$, which is $e[r] \bowtie t$. Thus, $e[r] \bowtie t \Leftarrow \exists x.\,e \bowtie t$ holds in all models of $T_{BV}$. $\square$

We will use $\mathsf {solve}$ for choosing terms for quantifier instantiation, where the above properties are important for the correctness and completeness properties of our algorithm. Notice that this method may be applied to any literal that is linear in x, although it only has the third property when that literal is linear invertible. In the context of quantifier instantiation, the $\mathsf {solve}$ method is generally only effective when used on literals that are linear invertible.

3.2 Invertibility conditions

Table 2 shows the rules for inverse computation for bit-vector operators $-$, ${\sim }\,$, $+$, and $\cdot$ over equality. Note that for the first three operators, these inverses are general inverses. For bit-vector multiplication, however, the given inverse is not, since it is tied to the condition that s evaluates to an odd value.

Tables 3, 4, 5, 6 and 7 list the invertibility conditions for linear literals in x with bit-vector operators from the set $\{-, {\sim }\,, +, \cdot , \bmod , \div , \mathrel { \& }, \mid , \mathop {>>}, \mathop {>>_a}, \mathop {<<}, \circ \}$ and relational operators $\bowtie$ from the set $\{\approx , \not \approx ,<_\mathrm {u},>_\mathrm {u}, \le _\mathrm {u}, \ge _\mathrm {u}, <_\mathrm {s}, >_\mathrm {s}, \le _\mathrm {s}, \ge _\mathrm {s} \}$. Some invertibility conditions are $\top$, meaning that the literal is always solvable for x. Others have an invertibility condition that is the same as the literal itself but with x replaced by a term not containing x. For example, the invertibility condition for equality with division $x \div s \approx t$ is $(s \cdot t) \div s \approx t$. In other words, $x \div s \approx t$ is solvable for x if and only if $(s \cdot t)$ is a solution. Other invertibility conditions have no structural similarities with their corresponding literal. For example, the invertibility condition for multiplication with equality does not itself involve multiplication. A majority of the invertibility conditions for disequalities state explicit corner cases where the constraint is not solvable, whereas for inequalities the majority encode boundary checks. We discuss in Sect. 3.3 how we determined these invertibility conditions.

The idea of computing the inverse of bit-vector operators has been used successfully in a recent local search approach for solving quantifier-free bit-vector constraints by Niemetz et al. [20]. There, target values are propagated via inverse value computation. In contrast, our approach does not determine single inverse values based on concrete assignments, but rather aims at finding analytic, i.e., symbolic, solutions through the generation of conditional inverses. In an extended version of that work [21], the same authors present rules for inverse value computation over equality but they provide no proof of correctness for them. Here, we define invertibility conditions not only over equality but also disequality and (un)signed inequality, and verify their correctness up to a certain bit-width.

Table 2 Inverse computation for bit-vector operators $\{-, {\sim }\,, +, \cdot \}$ over equality (given modulo commutativity for addition and multiplication)

Table 3 Conditions for the invertibility of bit-vector operators over equality and disequality (given modulo commutativity for operators $+$, $\cdot$, $\mathrel { \& }$ and $\mid$)

Table 4 Conditions for the invertibility of bit-vector operators over unsigned inequalities $<_\mathrm {u}$ and $>_\mathrm {u}$ (given modulo commutativity for operators $+$, $\cdot$, $\mathrel { \& }$ and $\mid$)

Table 5 Conditions for the invertibility of bit-vector operators over unsigned inequalities $\le _\mathrm {u}$ and $\ge _\mathrm {u}$ (given modulo commutativity for operators $+$, $\cdot$, $\mathrel { \& }$ and $\mid$)

Table 6 Conditions for the invertibility of bit-vector operators over signed inequalities $<_\mathrm {s}$ and $>_\mathrm {s}$ (given modulo commutativity for operators $+$, $\cdot$, $\mathrel { \& }$ and $\mid$)

Table 7 Conditions for the invertibility of bit-vector operators over signed inequalities $\le _\mathrm {s}$ and $\ge _\mathrm {s}$ (given modulo commutativity for operators $+$, $\cdot$, $\mathrel { \& }$ and $\mid$)

3.3 Synthesizing invertibility conditions

We have identified invertibility conditions for all bit-vector operators in $\varSigma _{BV}$ where no general inverse exists (162 in total). A noteworthy aspect of this work is that we were able to leverage syntax-guided synthesis (SyGuS) technology [1] to help us do that. The reason is that the problem of finding invertibility conditions for a literal of the form $x \diamond s \bowtie t$ (or, symmetrically, $s \diamond x \bowtie t$) linear in x can be recast as a SyGuS problem by asking whether there exists a binary Boolean function C such that the (second-order) bit-vector formula

$$\begin{aligned} \exists C\forall s\forall t.\,(\exists x.\,x \diamond s \bowtie t )\Leftrightarrow C(s,t) \end{aligned}$$

is satisfiable. If a SyGuS solver succeeds in synthesizing the function C, we can use it as the invertibility condition for $x \diamond s \bowtie t$. To simplify the SyGuS problem we chose a bit-width of 4 for x, s, and t and eliminated the quantification over x in the formula above by by expanding it to

$$\begin{aligned} \exists C\forall s\forall t.\, \left( \bigvee \limits _{i=0}^{15} i \diamond s \bowtie t \right) \Leftrightarrow C(s,t) \end{aligned}$$

(1)

Since the search space for SyGuS solvers heavily depends on the input grammar (which defines the solution space for C), we decided to use two grammars with the same set of Boolean connectives but different sets of bit-vector operators:

$$ \begin{aligned} O_r= & {} \{ \lnot , \wedge , \approx ,<_\mathrm {u},<_\mathrm {s}, 0, \text {min}_s, \text {max}_s, s, t, {\sim }\,, -, \mathrel { \& }, \mid \} \\ O_g= & {} \{ \lnot , \wedge , \vee , \approx ,<_\mathrm {u},<_\mathrm {s}, \ge _\mathrm {u}, \ge _\mathrm {s}, 0, \text {min}_s, \text {max}_s, s, t, {\sim }\,, +, -, \mathrel { \& }, \mid , \mathop {>>}, \mathop {<<} \} \end{aligned}$$

Note that s and t, which we have used until now as metavariables denoting arbitrary terms, as in (1), are to be understood as free (i.e., uninterpreted) constants in the two sets above. We call $O_r$ the restricted grammar and $O_g$ the general grammar.

The selection of bit-vector constants in the grammar turned out to be crucial for finding solutions; for example, by adding $\text {min}_s$ and $\text {max}_s$ we were able to synthesize substantially more invertibility conditions for signed inequalities. For each of the two sets of operators, we generated 140 SyGuS problems,³ one for each combination of bit-vector operator $\diamond \in$ {$\cdot$, $\bmod$, $\div$, $\mathrel { \& }$, $\mid$, $\mathop {>>}$, $\mathop {>>_a}$, $\mathop {<<} \}$ over relation $\bowtie \;\in$ {$\approx$, $\not \approx$, $<_\mathrm {u}$, $\le _\mathrm {u}$, $>_\mathrm {u}$, $\ge _\mathrm {u}$, $<_\mathrm {s}$, $\le _\mathrm {s}$, $>_\mathrm {s}$, $\ge _\mathrm {s} \}$, and used the SyGuS extension of the CVC4 solver [26] to solve these problems.

Using operators $O_r$ ($O_g$) we were able to synthesize 98 (116) out of 140 invertibility conditions, with 118 unique solutions overall. When we found more than one solution for a condition (either with operators $O_r$ and $O_g$, or manually) we chose the one that involved the smaller number of operator applications. Thus, we ended up using 79 out of 118 synthesized conditions and 83 manually crafted conditions.

In some cases, the SyGuS approach was able to synthesize invertibility conditions that were smaller, in the sense of containing a smaller number of operator applications, than those we had manually crafted. For example, we manually defined the invertibility condition for $x \cdot s \approx t$ as $(t \approx 0)\,\vee \,( (t \mathrel { \& } - t ) \ge _\mathrm {u} (s \mathrel { \& } - s ) \,\wedge \,(s \not \approx 0))$. With SyGuS we obtained $((- s \mid s) \mathrel { \& } t) \approx t$. For some other cases, however, the synthesized solution involved more bit-vector operators than needed. For example, for ${x \bmod s \not \approx t}$ we manually defined the invertibility condition ${(s \not \approx 1)\,\vee \,(t \not \approx 0)}$, whereas SyGuS produced the solution ${\sim }\, \!(- s) \mid t \not \approx 0$. For the majority of invertibility conditions, finding a solution did not require more than one hour of CPU time on an Intel Xeon E5-2637 with 3.5GHz and a memory limit of 8GB. Interestingly, the most time-consuming synthesis task (over 107 hours of CPU time) was finding the condition $((t + t) - s) \mathrel { \& } s \ge _\mathrm {u} t$ for ${s \bmod x \approx t}$. A small number of synthesized solutions were correct only for bit-width 4 (we explain how solutions were checked in Sect. 3.4 below). An example incorrect solution is $({\sim }\, \!s \mathop {<<} s) \mathop {<<} s <_\mathrm {s} t$ for $x \div s <_\mathrm {s} t$. In total, we found 6 width-dependent synthesized solutions, all of them for bit-vector operators $\div$ and $\bmod$. For those, we used the manually crafted invertibility conditions instead.

3.4 Verifying invertibility conditions

We verified the correctness of all 162 invertibility conditions for bit-widths from 1 to 65 by checking, for each bit-width, the $T_{BV}$-unsatisfiability of the (quantified) formula

$$\begin{aligned} \lnot (\phi \Leftrightarrow \exists x.\,\ell [x]) \end{aligned}$$

where $\ell$ ranges over the literals in Tables 3, 4, 5, 6 and 7 with s and t replaced by fresh variables, and $\phi$ is the corresponding invertibility condition.

In total, we generated 12,980 verification problems. To verify them we used all participating solvers of the quantified bit-vector division of SMT-competition 2017, namely Boolector [19], CVC4, Q3B [16], and Z3 [6]. For each solver/benchmark pair we used a CPU time limit of one hour and a memory limit of 8GB on the same machines as those mentioned in the previous section. All solvers that did not time out on a given benchmark agreed on the satisfiability status of that benchmark. We considered an invertibility condition to be verified for a certain bit-width if at least one of the solvers was able to report unsatisfiable for the corresponding formula within the given time limit. Out of the 12,980 instances, we were able to verify 12,277 (94.6%).

Overall, all verification tasks (including timeouts) required a total of 275 days of CPU time. The success rate of each individual solver was 91.4% for Boolector, 85.0% for CVC4, 50.8% for Q3B, and 92% for Z3. We observed that on 30.6% of the problems, Q3B exited with a Python exception without returning any result. For bit-vector operators {${\sim }\,$, $-$, $+$, $\mathrel { \& }$, $\mid$, $\mathop {>>}$, $\mathop {>>_a}$, $\mathop {<<}$, $\circ \}$, over all relations, and for operators {$\cdot$, $\div$, $\bmod \}$ over relations $\{\not \approx , \le _\mathrm {u}, \le _\mathrm {s} \}$, we were able to verify all invertibility conditions for all bit-widths in the range 1–65. Interestingly, no solver was able to verify the invertibility conditions for $x \bmod s <_\mathrm {s} t$ with a bit-width of 54 and $s \bmod x <_\mathrm {u} t$ with bit-widths 35-37 within the allotted time. We attribute this to the underlying heuristics used by the SAT solvers in these systems. All other conditions for $<_\mathrm {s}$ and $<_\mathrm {u}$ were verified for all bit-vector operators up to bit-width 65. The remaining conditions for operators {$\cdot$, $\div$, $\bmod \}$ over relations {$\approx$, $>_\mathrm {u}$, $\ge _\mathrm {u}$, $>_\mathrm {s}$, $\ge _\mathrm {s} \}$ were verified up to at least a bit-width of 14. We discovered 3 conditions for $s \div x \bowtie t$ with $\bowtie \;\in \{\not \approx , >_\mathrm {s}, \ge _\mathrm {s} \}$ that were not correct for a bit-width of 1. For each of these cases, we added an additional invertibility condition that correctly handles that case.

Further work Formally proving that our invertibility conditions are correct for all bit-widths is beyond the scope of this paper. We have tackled this challenge in other work [23] by recasting the problem to that of checking the unsatisfiability of certain quantified formulas over the combined theory of non-linear integer arithmetic and uninterpreted functions, based on several encodings of bit-vectors in that theory. In that work too, we used SMT solvers to prove the generated formulas. The approach was only partially successful as it failed to verify about a quarter of the invertibility conditions. Most of these remaining conditions, however, were later verified interactively in the Coq proof assistant by Ekici et al. [10], leveraging previous work [9] that had developed a formalization in Coq of the SMT-LIB theory of bit-vectors.

4 Counterexample-guided instantiation for bit-vectors

In this section, we define a novel instantiation-based technique for quantified bit-vector formulas. At a high level, we are interested in determining the satisfiability of a quantified formula $\varphi$ in some background theory T. We use a counterexample-guided approach for quantifier instantiation [27] that adds new instances of $\varphi$ to a set of quantifier-free clauses based on models for the negation of $\lnot \varphi$. The procedure terminates if it constructs a set of instances that is T-unsatisfiable or is T-satisfiable and entails $\varphi$.

Approaches for quantifier instantiation crucially depend on having a good strategy for choosing terms to be used in instantiations. We leverage techniques from the previous section to develop one such strategy for the theory of bit-vectors. Specifically, recall that the procedure $\mathsf {solve}$ in Fig. 1 returns a symbolic solution to a (linear) bit-vector literal. This procedure uses invertibility conditions for expressing the conditions under which such a solution exists. Intuitively, our quantifier instantiation procedure identifies literals whose solved forms correspond to relevant instantiations, and uses the terms returned by $\mathsf {solve}$ to instantiate quantified formulas. These symbolic instantiations are combined as necessary with other instantiation techniques.

Fig. 2

A counterexample-guided quantifier instantiation procedure $\mathsf {CEGQI}_{{\mathcal {S}}}$, parameterized by a selection function ${\mathcal {S}}$, for determining the T-satisfiability of $\forall \varvec{x}.\,\psi$ with $\psi$ binder-free

Our counterexample-guided approach for quantifier instantiation is exemplified by the procedure $\mathsf {CEGQI}_{{\mathcal {S}}}$ in Fig. 2. To simplify the exposition here, we focus on input problems expressed as a single formula in prenex normal form and with up to one quantifier alternation. We stress, though, that the approach applies in general to arbitrary sets of quantified formulas in any theory T with signature $\varSigma$ and a decidable binder-free (and hence quantifier-free) fragment. The procedure checks via instantiation the T-satisfiability of a quantified input formula $\varphi$ of the form $\forall \varvec{x}.\,\psi [\varvec{x} ]$ where $\psi$ is binder-free.⁴ It maintains an evolving set $\varGamma$, initially empty, of binder-free instances of the input formula.

During each iteration of the procedure’s loop, there are three possible cases:

• 1. $\varGamma$ is T-unsatisfiable: then the input formula $\varphi$ is also T-unsatisfiable and “unsat” is returned;

• 2. $\varGamma$ is T-satisfiable but not together with $\lnot \psi$, the negated body of $\varphi$: then $\varGamma$ T-entails $\varphi$, hence $\varphi$ is T-satisfiable and “sat” is returned;

• 3. $\varGamma \cup \{\lnot \psi \}$ is T-satisfiable: $\varGamma$ is extended with an instance of $\psi$ obtained by replacing the variables $\varvec{x}$ with some terms $\varvec{t}$, and the computation continues.

The procedure $\mathsf {CEGQI}_{}$ is parametrized by a selection function ${\mathcal {S}}$ that generates the terms $\varvec{t}$.

Definition 7

(Selection Function [28]) A selection function takes as input a tuple of variables $\varvec{x}$, a model ${{\mathcal {I}}}$ of T, a binder-free $\varSigma$-formula $\psi [\varvec{x} ]$, and a set $\varGamma$ of $\varSigma$-formulas such that $\varvec{x} \cap {FV}(\varGamma ) = \emptyset$ and ${{\mathcal {I}}} \models \varGamma \cup \{ \lnot \psi \}$. It returns a tuple $\varvec{t}$ of $\varepsilon$-valid terms of the same type as $\varvec{x}$ such that ${FV}(\varvec{t}) \subseteq {FV}(\psi ) \setminus \varvec{x}$.

Definition 8

Let $\psi [\varvec{x} ]$ be a binder-free $\varSigma$-formula. A selection function is:

• 1. Finite for $\varvec{x}$ and $\psi$ if there is a finite set ${\mathcal {S}}^*$ such that ${\mathcal {S}}( \varvec{x}, \psi , {{\mathcal {I}}}, \varGamma ) \in {\mathcal {S}}^*$ for all legal inputs ${{\mathcal {I}}}$ and $\varGamma$.

• 2. Monotonic for $\varvec{x}$ and $\psi$ if for all legal inputs ${{\mathcal {I}}}$ and $\varGamma$, ${\mathcal {S}}(\varvec{x}, \psi , {{\mathcal {I}}}, \varGamma ) = \varvec{t}$ only if $\psi [ \varvec{t} ] \not \in \varGamma$.

Above, we refer to a legal input as one where ${{\mathcal {I}}}$ is a model for $T \wedge \varGamma \wedge \lnot \psi$, and $\varGamma$ does not contain any free variables in $\varvec{x}$. An invariant of the procedure $\mathsf {CEGQI}_{{\mathcal {S}}}$ is that it calls ${\mathcal {S}}$ only with legal inputs. This procedure is refutation-sound and model-sound for any selection function ${\mathcal {S}}$, and terminating for selection functions that are finite and monotonic.⁵ The following theorem is adapted from previous work [28].

Theorem 9

(Correctness of $\mathsf {CEGQI}_{{\mathcal {S}}}$) Let ${\mathcal {S}}$ be a selection function and let $\varphi = \forall \varvec{x}.\,\psi$ with $\psi$-binder-free. Then the following hold.

• 1. If $\mathsf {CEGQI}_{{\mathcal {S}}}( \varphi )$ returns “unsat”, then $\varphi$ is T-unsatisfiable.

• 2. If $\mathsf {CEGQI}_{{\mathcal {S}}}( \varphi )$ returns “sat” for some final $\varGamma$, then $\varphi$ is T-satisfiable and T-equivalent to $\varGamma$.

• 3. If ${\mathcal {S}}$ is finite and monotonic for $\varvec{x}$ and $\psi$, then $\mathsf {CEGQI}_{{\mathcal {S}}}( \varphi )$ terminates.

Proof

We show each part of the theorem below. Let $\varvec{y} = {FV}(\psi ) \setminus \varvec{x}$. Note that by the definition of $\mathsf {CEGQI}_{{\mathcal {S}}}$ and since ${\mathcal {S}}$ is a selection function, all inputs ${{\mathcal {I}}}$ and $\varGamma$ given to ${\mathcal {S}}$ in the loop of this function are legal inputs. Also note that for the first two parts, we have that $\mathsf {CEGQI}_{{\mathcal {S}}}( \varphi )$ terminates in a state where $\varGamma$ is a set of instances of $\psi [\varvec{x} ]$ of the form $\psi [\varvec{t} ]$ where, since ${\mathcal {S}}$ is a selection function, $\varvec{t}$ is a tuple of $\varepsilon$-valid terms and ${FV}(\varvec{t}) \subseteq \varvec{y}$.

Part 1) By definition of $\mathsf {CEGQI}_{{\mathcal {S}}}$, if $\mathsf {CEGQI}_{{\mathcal {S}}}( \varphi )$ returns “unsat,” then $\varGamma$ is T-unsatisfiable. By construction, $\varGamma$ consists of instances $\psi [ \varvec{t} ]$ of $\psi$. Since $\varGamma$ is T-unsatisfiable, it follows by the semantics of $\forall$ that $\forall \varvec{x}.\,\psi [ \varvec{x} ]$ is T-unsatisfiable.

Part 2) By definition of $\mathsf {CEGQI}_{{\mathcal {S}}}$, if $\mathsf {CEGQI}_{{\mathcal {S}}}( \varphi )$ returns “sat,” then $\varGamma$ is T-satisfiable and $\varGamma ' = \varGamma \cup \{ \lnot \psi [ \varvec{x} ] \}$ is T-unsatisfiable. The latter implies that $\varGamma$ T-entails $\psi [\varvec{x} ]$. Since, by construction of $\varGamma$, no variables of $\varvec{x}$ occur in $\varGamma$ we have that $\varGamma$ T-entails $\forall \varvec{x}.\,\psi [\varvec{x} ]$. The equivalence between the two follows from the fact that, again by construction of Gamma, $\forall \varvec{x}.\,\psi [\varvec{x} ]$ T-entails $\varGamma$.

Part 3) Assume ${\mathcal {S}}$ is monotonic and finite for $\psi [ \varvec{x} ]$. Since it is finite, let ${\mathcal {S}}^*$ be a finite set such that ${\mathcal {S}}( \varvec{x}, \psi , {{\mathcal {I}}}, \varGamma ) \in {\mathcal {S}}^*$ for all valid inputs ${{\mathcal {I}}}, \varGamma$. Since it is monotonic, each iteration of the loop adds a new formula from ${\mathcal {S}}^*$ to $\varGamma$. Since ${\mathcal {S}}^*$ is finite, the number of iterations of this loop is bounded by the size of ${\mathcal {S}}^*$. Hence, $\mathsf {CEGQI}_{{\mathcal {S}}}( \varphi )$ terminates.

$\square$

Thanks to this theorem, it suffices to define a selection function satisfying the criteria of Definitions 7 and 8 to define a T-satisfiability procedure for quantified $\varSigma$-formulas. We do that in the following section for $T_{BV}$.

Fig. 3

Selection functions ${\mathcal {S}}^{BV}_{c}$ for binder-free bit-vector formulas. The procedure is parameterized by a configuration c, one of either ${\mathbf {m}}$ (model value), ${\mathbf {k}}$ (keep), ${\mathbf {s}}$ (slack), or ${\mathbf {b}}$ (boundary)

4.1 Selection functions for bit-vectors

In this subsection, we provide several selection functions to be used for bit-vector formulas in the framework described above. Some of these selection functions may return terms containing choice terms based on the procedure $\mathsf {solve}$ from Sect. 3. Recall that this procedure uses invertibility conditions to express symbolic solutions to bit-vector literals. There are several possible strategies that one can use in the design of a selection function; we discuss a few alternatives next.

Figure 3 describes a class of selection functions ${\mathcal {S}}^{BV}_{c}$ for binder-free bit-vector formulas depending on a configuration c. The parameter c ranges over the enumeration type {${\mathbf {m}}$, ${\mathbf {k}}$, ${\mathbf {s}}$, ${\mathbf {b}}\}$ whose values are short respectively for “model value”, “keep”, “slack”, and “boundary.” We consider multiple configurations because there are many possible choices of terms to use for quantifier instantiation.⁶

The selection function of Fig. 3 collects in the set M all the literals occurring in $\psi$ that are satisfied by ${{\mathcal {I}}}$. Then, it collects in the set N a projected form of each literal in M. This form is computed by the function $\mathsf {project}_{c}$, parameterized by configuration c,

which transforms its input literal into a form suitable for procedure $\mathsf {solve}$ from Fig. 1. We discuss the intuition for projection operations in more detail below.

Example 10

Consider the $\varSigma _{BV}$-literal $a \ge _\mathrm {u} b$ and the interpretation ${{\mathcal {I}}}$, where $a^{{\mathcal {I}}} = 5$ and $b^{{\mathcal {I}}} = 3$. With input ${{\mathcal {I}}}$ and $a \ge _\mathrm {u} b$, the function $\mathsf {project}_{c}$ returns the literals: $\top$ for $c = {\mathbf {m}}$; $a \ge _\mathrm {u} b$ for $c = {\mathbf {k}}$; $a \approx b + 2$ for $c = {\mathbf {s}}$; and $a \approx b + 1$ for $c = {\mathbf {b}}$. In the context of Fig. 3, the above choices impact whether a solved form can be computed for a in the literals returned above, and what that solved form is. In the case of $c = {\mathbf {m}}$, the literal $\top$ cannot be solved for a, and hence its model value must be selected in the function ${\mathcal {S}}^{BV}_{c}$. On the other hand, in the case of $c = {\mathbf {b}}$, the literal $a \approx b + 1$ leads to the solved form $b+1$ for a.   $\triangle$

After constructing set N, the selection function computes a term $t_i$ for each variable $x_i$ in tuple $\varvec{x}$, which we call the solved form of $x_i$. To do that, it first constructs a set of literals $N_i$ all linear in $x_i$. It considers literals $\ell$ from N and replaces all previously solved variables $x_1, \ldots , x_{i-1}$ by their respective solved forms to obtain the literal $\ell ' = \ell [ t_1, \ldots , t_{i-1} ]$. It then calls function $\mathsf {linearize}$ on literal $\ell '$ which returns a set of literals, each obtained by replacing all but one occurrence of $x_i$ in $\ell$ with the value of $x_i$ in ${{\mathcal {I}}}$.⁷

Example 11

Consider an interpretation ${{\mathcal {I}}}$ where $x^{{\mathcal {I}}} = 1$, and $\varSigma _{BV}$-terms a and b with $x \not \in {FV}(a) \cup {FV}(b)$. We have that $\mathsf {linearize}(x, {{\mathcal {I}}}, x \cdot ( x + a ) \approx b)$ returns the set $\{ 1 \cdot ( x + a ) \approx b, x \cdot ( 1 + a ) \approx b \}$; $\mathsf {linearize}(x, {{\mathcal {I}}}, x \ge _\mathrm {u} a)$ returns the singleton set $\{ x \ge _\mathrm {u} a \}$; $\mathsf {linearize}(x, {{\mathcal {I}}}, a \not \approx b)$ returns the empty set.   $\triangle$

If the set $N_i$ is non-empty, the selection function heuristically chooses a literal from $N_i$, indicated in Fig. 3 with $\mathsf {choose}(N_i)$. It then computes a solved form $t_i$ for $x_i$ by solving the chosen literal for $x_i$ with the function $\mathsf {solve}$ described in the previous section. By construction of $N_i$, the chosen literal is guaranteed to be linear in $x_i$; our heuristic is most effective if the chosen literal is moreover linear invertible in $x_i$. If $N_i$ is empty, $t_i$ is simply (the constant denoting) the value of $x_i$ in the given model ${{\mathcal {I}}}$. After that, $x_i$ is eliminated from all the previous terms $t_1, \ldots , t_{i-1}$ by replacing it with $t_i$. After processing all n variables of $\varvec{x}$, the tuple $( t_1, \ldots , t_n )$ is returned.

The configuration of selection function ${\mathcal {S}}^{BV}_{c}$ determines how literals in M are modified by the $\mathsf {project}_{c}$ function prior to computing solved forms, based on the current model ${{\mathcal {I}}}$. With the model value configuration ${\mathbf {m}}$, the selection function effectively ignores the structure of all literals in M and (because the set $N_i$ is empty) ends up choosing the value $x_i^{{\mathcal {I}}}$ as the solved form of variable $x_i$, for each i. On the other end of the spectrum, the configuration ${\mathbf {k}}$ keeps all literals in M unchanged. The remaining two configurations have an effect on how disequalities and inequalities are handled by $\mathsf {project}_{c}$. They are are inspired by quantifier elimination techniques for linear arithmetic [5, 17]. With configuration ${\mathbf {s}}$, $\mathsf {project}_{c}$ normalizes any kind of literal (equality, inequality or disequality) $s \bowtie t$ to an equality by adding the slack value $(s - t)^{{\mathcal {I}}}$ to t. With configuration ${\mathbf {b}}$ it maps equalities to themselves and inequalities and disequalities to an equality corresponding to a boundary point of the relation between s and t based on the current model. Specifically, it adds 1 to t if s is greater than t in ${{\mathcal {I}}}$, it subtracts 1 if s is smaller than t, and returns $s \approx t$ if their value is the same. In the following, we provide an end-to-end example of our technique for quantifier instantiation that makes use of selection function

Example 12

Consider formula $\varphi = \forall x_1.\,(x_1 \cdot a \le _\mathrm {u} b)$ where a and b are terms with no free occurrences of $x_1$. To determine the satisfiability of $\varphi$, we invoke$\mathsf {CEGQI}_{{\mathcal {S}}^{BV}_{c}}$ on $\varphi$ for some configuration c. Say that in the first iteration of the loop, we find that $\varGamma ' = \emptyset \cup \{ x_1 \cdot a>_\mathrm {u} b \}$⁸ is satisfied by some model ${{\mathcal {I}}}$ of $T_{BV}$ such that $x_1^{{\mathcal {I}}} = 1$, $a^{{\mathcal {I}}} = 1$, and $b^{{\mathcal {I}}} = 0$. We invoke ${\mathcal {S}}^{BV}_{c} ((x_1), \psi , {{\mathcal {I}}}, \varGamma )$, where $\psi = (x_1 \cdot a \le _\mathrm {u} b)$, and first compute $M = \{ x_1 \cdot a >_\mathrm {u} b \}$, the subset of $\mathrm {Lit}(\psi )$ that is satisfied by ${{\mathcal {I}}}$. The table below summarizes the values of the internal variables of ${\mathcal {S}}^{BV}_{c}$ for the various configurations:

config	$N_1$	$t_1$
${\mathbf {m}}$	$\emptyset$	1
${\mathbf {k}}$	{ $x_1$ $\cdot$ a$>_\mathrm {u}$ b }	$\varepsilon z.\,(b <_\mathrm {u} - a \mid a ) \Rightarrow z \cdot a >_\mathrm {u} b$
${\mathbf {s}}$, ${\mathbf {b}}$	{ $x_1$ $\cdot$ a$\approx$ b+1 }	$\varepsilon z.\,((- a \mid a) \mathrel { \& } b+1 \approx b+1) \Rightarrow z \cdot a \approx b+1$

In each case, ${\mathcal {S}}^{BV}_{c}$ returns tuple $( t_1 )$, and we add instance $t_1 \cdot a \le _\mathrm {u} b$ to $\varGamma$. Consider configuration ${\mathbf {k}}$ where $t_1$ is the choice expression $\varepsilon z.\,((b <_\mathrm {u} - a \mid a ) \Rightarrow z \cdot a >_\mathrm {u} b)$. Since $t_1$ is $\varepsilon$-valid, due to the semantics of $\varepsilon$, this instance is equisatisfiable with

$$\begin{aligned} ((b <_\mathrm {u} - a \mid a ) \Rightarrow v \cdot a >_\mathrm {u} b) \wedge v \cdot a \le _\mathrm {u} b \end{aligned}$$

(2)

where v is a fresh variable. This formula is $T_{BV}$-satisfiable if and only if literal $\ell = \lnot (b <_\mathrm {u} - a \mid a )$ is $T_{BV}$-satisfiable. In the second iteration of the loop in $\mathsf {CEGQI}_{{\mathcal {S}}^{BV}_{c}}$, set $\varGamma$ contains formula (2) above.

We have two possible outcomes, depending on the satisfiability of $\ell$: (i) if $\ell$ is $T_{BV}$-unsatisfiable, then (2) and hence $\varGamma$ are $T_{BV}$-unsatisfiable, and the procedure terminates with “unsat”; (ii) if $\ell$ is satisfied by some model ${{\mathcal {J}}}$ of $T_{BV}$, then the formula $\exists z. z \cdot a>_\mathrm {u} b$ is false in ${{\mathcal {J}}}$, since the invertibility condition of $z \cdot a>_\mathrm {u} b$ is false in ${{\mathcal {J}}}$. Hence, $\varGamma ' = \varGamma \cup \{ x_1 \cdot a>_\mathrm {u} b \}$ is unsatisfiable, and the algorithm terminates with “sat”.

As we argue later, quantified bit-vector formulas like $\varphi$ above, which contain only one occurrence of a universal variable in a linear invertible literal, require at most one instantiation before $\mathsf {CEGQI}_{{\mathcal {S}}^{BV}_{{\mathbf {k}}}}$ terminates. The same guarantee does not hold with the other configurations, however. In particular, configuration ${\mathbf {m}}$ generates the instance where $t_1$ is 1, which simplifies to $a \le _\mathrm {u} b$. This may not be sufficient to show that $\varGamma$ or $\varGamma '$ is unsatisfiable in the second iteration of the loop, and the algorithm may resort to enumerating a repeating pattern of instantiations, such as $x_1 \mapsto 1, 2, 3, \ldots$ and so on. This obviously does not scale for problems with large bit-widths.   $\triangle$

Example 13

As the previous example demonstrates, $\mathsf {CEGQI}_{{\mathcal {S}}^{BV}_{{\mathbf {k}}}}$ may terminate after one instance for input formulas whose body has just one literal and a single occurrence of each universal variable. However, consider extending the quantified formula from that example to a disjunction of two literals for some literal $\ell [x_1]$: $\forall x_1.\,(x_1 \cdot a \le _\mathrm {u} b \vee \ell [x_1])$. Assume that our selection function chooses the same $t_1$ as in the previous example. The corresponding instance is equisatisfiable with:

$$\begin{aligned} ((b <_\mathrm {u} - a \mid a )\Rightarrow v \cdot a >_\mathrm {u} b) \wedge ( v \cdot a \le _\mathrm {u} b \vee \ell [v] ) \end{aligned}$$

(3)

with v a fresh variable. In contrast to Example 12, the second iteration of the loop from Fig. 2 is now not guaranteed to terminate. Formula (3) may be satisfied by a model ${{\mathcal {J}}}$ where $v \cdot a >_\mathrm {u} b$ and $\ell [v]$ hold. Note that ${{\mathcal {J}}}$ may also satisfy $b <_\mathrm {u} - a \mid a$, meaning it may still be the case that $\lnot (x_1 \cdot a \le _\mathrm {u} b)$ together with the above instance is satisfied by ${{\mathcal {J}}}$. In such a case, we may invoke $\mathsf {CEGQI}_{{\mathcal {S}}^{BV}_{{\mathbf {k}}}}$ again, which may produce the same solved form for $x_1$ if it constructs a solved form for $x_1$ again based on the literal $x_1 \cdot a \le _\mathrm {u} b$. By the terminology from Definition 8, this means that the selection function ${\mathcal {S}}^{BV}_{{\mathbf {k}}}$ is not monotonic for quantified formulas with more than one occurrence of a universal variable.   $\triangle$

If the literals of the input formula have multiple occurrences of $x_1$, then multiple instances may be returned by the selection function, since the literals returned by $\mathsf {linearize}$ in Fig. 3 depend on the model value of $x_1$, and hence more than one possible instance may be considered in loop in Fig. 2.

The following theorem summarizes the properties of our selection functions. In the following, we say a quantified formula is unit linear invertible if it is of the form $\forall x.\,\ell [x]$ where $\ell$ is a linear invertible literal with respect to x. We say a selection function is n-finite for a quantified formula if the number of possible instantiations it returns is at most n for some positive integer n.

Theorem 14

Let $\psi [\varvec{x} ]$ be a binder-free formula in the signature of $T_{BV}$.

• 1. ${\mathcal {S}}^{BV}_{c}$ is a finite selection function for $\varvec{x}$ and $\psi$ for all $c \in \{{\mathbf {m}}, {\mathbf {k}}, {\mathbf {s}}, {\mathbf {b}}\}$.

• 2. ${\mathcal {S}}^{BV}_{{\mathbf {m}}}$ is monotonic.

• 3. ${\mathcal {S}}^{BV}_{{\mathbf {k}}}$ is 1-finite if $\ \forall \,\varvec{x}.\,\psi$ is unit linear invertible.

• 4. ${\mathcal {S}}^{BV}_{{\mathbf {k}}}$ is monotonic if $\ \forall \,\varvec{x}.\,\psi$ is unit linear invertible.

Proof

Let $\varvec{x} = ( x_1, \ldots , x_n )$ be a tuple of variables and let $\psi$ be a binder-free $T_{BV}$-formula. We show each part for the case where $n=1$; the arguments below can be lifted to $n>1$ in a straightforward way. Let $\varGamma$ be a set of formulas such that $x_1 \not \in {FV}(\varGamma )$, let ${{\mathcal {I}}}$ be a model of $T_{BV}$ such that ${{\mathcal {I}}} \models \varGamma \cup \{ \lnot \psi \}$, and let $t_1$ be ${\mathcal {S}}^{BV}_{c} ( (x_1), {{\mathcal {I}}}, \psi , \varGamma )$.

Part 1) To show that ${\mathcal {S}}^{BV}_{c}$ is a selection function, we must show that $t_1$ is $\varepsilon$-valid and ${FV}(t_1) \subseteq {FV}(\psi ) \setminus \{ x_1 \}$. Notice that for all configurations, the value $( t_1 )$ returned by ${\mathcal {S}}^{BV}_{c}$ is either of the form $x_1^{{\mathcal {I}}}$ or $\mathsf {solve} ( x_1, \ell ' )$ where $\ell '$ is the result of calling $\mathsf {linearize}$ and $\mathsf {project}_{c}$ on some $\ell \in \mathrm {Lit}(\psi )$. In the former case, we have that $t_1$ is clearly $\varepsilon$-valid and ${FV}(t_1) = \emptyset$. In the latter case, as a consequence of Theorem 6, and since $\ell '$ is $\varepsilon$-valid and linear by definition of $\mathsf {linearize}$ and $\mathsf {project}_{c}$, we have that $t_1$ is $\varepsilon$-valid and ${FV}(t_1) \subseteq {FV}(\ell ') \setminus \{ x_1 \}$. By the definition of $\mathsf {linearize}$ and $\mathsf {project}_{c}$ for each configuration c, and since each element of M is from $\mathrm {Lit}(\psi )$, we have that ${FV}(\ell ') \subseteq {FV}(\psi )$. Thus, in either case, we have ${FV}(t_1) \subseteq {FV}(\psi ) \setminus \{ x_1 \}$. Hence, ${\mathcal {S}}^{BV}_{c}$ is a selection function for $c={\mathbf {m}}$, ${\mathbf {k}}$, ${\mathbf {s}}$, ${\mathbf {b}}$. To show these selection functions are finite for $\psi$, note that the number of terms of form $x_1^{{\mathcal {I}}}$ is finite (because a bit-vector sort only has a finite number of possible values). Also note that the number of literals in $\mathrm {Lit}(\psi )$ is finite. For c and $\ell \in \mathrm {Lit}(\psi )$, the set of literals of the form $\mathsf {project}_{c} ( {{\mathcal {I}}}, \ell )$, call this set $N'$, is finite. Now, for any specific $N \subseteq N'$, consider the loop in Fig. 3. The loop consists of substitutions, calls to $\mathsf {linearize}$, choices from $N_i$, and calls to $\mathsf {solve}$. Given that we start with a finite set, each of these opearations still has only a finite number of possible outcomes. The number of possible return values of ${\mathcal {S}}^{BV}_{c}$ is thus finite for $( x_1 )$ and $\psi$ for $c={\mathbf {m}}$, ${\mathbf {k}}$, ${\mathbf {s}}$, ${\mathbf {b}}$.

Part 2) Assume that $\mathsf {project}_{{\mathbf {m}}}$ is not monotonic for $( x_1 )$, meaning that $\psi [t_1] \in \varGamma$. Since $\mathsf {project}_{{\mathbf {m}}}$ is a selection function by Part 1, and ${{\mathcal {I}}}, \varGamma$ are legal inputs to $\mathsf {project}_{{\mathbf {m}}}$, it must be the case that ${{\mathcal {I}}} \models \varGamma \wedge \lnot \psi$. So ${{\mathcal {I}}} \models \psi [t_1]$. However, since $\mathsf {project}_{{\mathbf {m}}} ( {{\mathcal {I}}}, \ell ) = \top$, it must be the case that $t_1 = x_1^{{\mathcal {I}}}$, and we have that ${{\mathcal {I}}} \models \lnot \psi [x_1]$, which is a contradiction. Hence, $\mathsf {project}_{{\mathbf {m}}}$ is monotonic for $\psi$.

Part 3) Assume $\psi$ is the linear invertible literal $\ell$. Since ${{\mathcal {I}}} \models \lnot \ell$, and by the definition of $\mathsf {project}_{{\mathbf {k}}}$, we must have that $M = N = \{\lnot \ell \}$. Then, by definition of $\mathsf {linearize}$, and since $\ell$ is linear with respect to $x_1$, we have that $t_1$ must be the term returned by $\mathsf {solve} ( x_1, \lnot \ell )$. Hence, ${\mathcal {S}}^{BV}_{{\mathbf {k}}}$ has only one possible return value and hence is 1-finite.

Part 4) Assume $\psi$ is the linear invertible literal $\ell [ x_1 ]$. The return value of ${\mathcal {S}}^{BV}_{{\mathbf {k}}}$ is the tuple $( t_1 )$, where by the reasoning in Part 3, we have that $t_1$ is the term returned by $\mathsf {solve} ( x_1, \lnot \ell [ x_1 ] )$. Note that the negation of a linear invertible literal is still linear invertible as the set of relational operators we are using is closed under negation. Thus, by Theorem 6, and since $\ell$ is linear invertible with respect to $x_1$, we have that $\lnot \ell [t_1] \Leftrightarrow \exists z.\,\lnot \ell [z]$ holds in all models of $T_{BV}$. Now, assume that $\mathsf {project}_{{\mathbf {k}}}$ is not monotonic for $( x_1 )$ and $\ell [ x_1 ]$, meaning that $\ell [t_1]\in \varGamma$. Since $\mathsf {project}_{{\mathbf {k}}}$ is a selection function by Part 1 and ${{\mathcal {I}}}, \varGamma$ are legal inputs to $\mathsf {project}_{{\mathbf {k}}}$, it must be the case that ${{\mathcal {I}}} \models \varGamma \wedge \lnot \psi$. So, ${{\mathcal {I}}} \models \ell [t_1]$. But then, since $\lnot \ell [t_1] \Leftarrow \exists z.\,\lnot \ell [z]$ holds in all models of $T_{BV}$, we have that ${{\mathcal {I}}}$ must satisfy $\lnot \exists z.\,\lnot \ell [z]$, which is $\forall z.\,\ell [z]$. However, we also have that ${{\mathcal {I}}} \models \lnot \ell [ x_1 ]$, which is a contradiction. Hence, it must instead be the case that $\ell [ t_1 ] \not \in \varGamma$ and thus $\mathsf {project}_{{\mathbf {k}}}$ is monotonic for $\psi$.

$\square$

Theorem 14 implies that the application of counterexample-guided instantiation to arbitrary bit-vector formulas using selection function ${\mathcal {S}}^{BV}_{{\mathbf {m}}}$ is a decision procedure for quantified bit-vectors. Unfortunately, the worst-case number of instances considered for a variable $x_{[n]}$ by this selection function is proportional to the number of its possible values ($2^n$), which makes the decision procedure impractical for sufficiently large n. More interestingly, counterexample-guided instantiation using selection function ${\mathcal {S}}^{BV}_{{\mathbf {k}}}$ is a decision procedure for quantified formulas that are unit linear invertible. Moreover, using this selection function has the guarantee that at most one instantiation is returned. Hence, formulas in this fragment can be effectively reduced to quantifier-free bit-vector constraints in at most two iterations of the loop of procedure $\mathsf {CEGQI}_{{\mathcal {S}}}$ in Fig. 2. This was demonstrated by the use of this selection function in Example 12.

4.2 Implementation

We implemented the new instantiation techniques described in this section as an extension of CVC4, a DPLL$(T)$-based SMT solver [24] with support for quantifier-free bit-vector constraints, (arbitrarily nested) quantified formulas, and choice expressions. In CVC4, all choice terms $\varepsilon x.\,\varphi [x]$ are eliminated from assertions by replacing them with a fresh variable v of the same type and adding $\varphi [v]$ as a new assertion. This is sound since all choice expressions we consider are $\varepsilon$-valid. We point out that, since v is fresh, this treatment does not enforce that choice terms are unique up to logical equivalence. In other words, $\varepsilon x.\,\varphi [x]$ and $\varepsilon x.\,\psi [x]$ may be replaced by distinct variables even when $\varphi$ and $\psi$ are logically equivalent. This is done for performance reasons since the correctness of our procedure does not rely on this property. In the following, we discuss important implementation details of this extension.

4.2.1 Handling duplicate instantiations

The selection functions ${\mathcal {S}}^{BV}_{{\mathbf {s}}}$ and ${\mathcal {S}}^{BV}_{{\mathbf {b}}}$ are not guaranteed to be monotonic and neither is ${\mathcal {S}}^{BV}_{{\mathbf {k}}}$ for quantified formulas that are not unit linear invertible. Hence, when applying these strategies to arbitrary quantified formulas, we use a two-tiered strategy that invokes ${\mathcal {S}}^{BV}_{{\mathbf {m}}}$ as a second resort if the instance returned by a selection function already exists in $\varGamma$.

4.2.2 Linearizing rewrites

Our selection function in Fig. 3 uses the function $\mathsf {linearize}$ to compute literals that are linear in the variable $x_i$. The way we presently implement $\mathsf {linearize}$ makes those literals dependent on the value of $x_i$ in the current model ${{\mathcal {I}}}$, with the risk of overfitting to that model. To address this limitation, we use a set of equivalence-preserving rewrite rules, which apply basic algebraic manipulations with the goal of reducing, when possible, the number of occurrences of $x_i$ to one.

As a trivial example, consider a literal $x_i + x_i \approx a$, which can be rewritten to $2 \cdot x_i \approx a$. The rewritten literal is linear in $x_i$ if a does not contain $x_i$. If that is the case, there exists an invertibility condition for this literal as discussed in Sect. 3.

4.2.3 Variable elimination

We use procedure $\mathsf {solve}$ from Sect. 3 not only for selecting quantifier instantiations, but also for eliminating variables from quantified formulas. In particular, for a quantified formula of the form $\forall x \varvec{y}.\,\ell \Rightarrow \varphi [x, \varvec{y} ]$, if $\ell$ is linear in x and $\mathsf {solve} ( x, \ell )$ returns a term s not containing $\varepsilon$-expressions, we can replace this formula by $\forall \varvec{y}.\,\varphi [s,\varvec{y} ]$. When $\ell$ is an equality, this is known as destructive equality resolution (DER) in the literature and is an important implementation-level optimization in state-of-the-art bit-vector solvers [30].

As shown in Fig. 1, we use the $\mathsf {getInverse}$ function to increase the likelihood that $\mathsf {solve}$ returns a term that contains no $\varepsilon$-expressions. A common example is a literal $x \cdot c \approx t$ where c is an odd constant and $\kappa (c) = w$. The only solution for x in this case is $c^{-1} \cdot t$, with $c^{-1}$ the (unique) multiplicative inverse of c modulo $2^w$, which can be determined with the Extended Euclidean algorithm.

4.2.4 Handling extract

Consider formula $\forall x_{[32]}.\,(x[31:16] \not \approx a_{[16]} \vee x[15:0] \not \approx b_{[16]})$. Since all invertibility conditions for the extract operator are $\top$, rather than producing choice expressions, we have found it more effective to eliminate extracts via rewriting. As a consequence, we independently solve constraints for regions of quantified variables when they appear underneath applications of extract operations. In this example, we let the solved form of x be $y_{[16]} \circ z_{[16]}$ where y and z are fresh variables, and subsequently solve for these variables in $y \approx a$ and $z \approx b$. Hence, we may instantiate x with $a \circ b$, a term that we would not have found by considering the two literals independently in the negated body of the formula above.

4.2.5 Handling propositional structure and nested quantifiers

Figure 2 describes counterexample-guided quantifier instantiation for universal formulas of the form $\forall \varvec{x}.\,\psi$ with $\psi$ quantifier-free. Since $\psi$ can contain additional free variables besides those in $\varvec{x}$, this means effectively that the procedure can deal with formulas with one level of quantifier alternation; specifically, of the form $\exists \varvec{y}.\,\forall \varvec{x}.\,\psi$ where $\varvec{x} \cup \varvec{y} = {FV}(\psi )$. However, in practice, our techniques can be extended to problems with more than one level of quantifier alternation, and to problems not in prenex normal form. A thorough description of this is beyond the scope of this paper. In the following, we thus only provide some high level details. Further details can be found in Section 6 of [28].

In the DPLL$(T)$ setting, the SMT solver incrementally builds a truth assignment with the goal of finding a set M of literals that is T-satisfiable and, when seen as a truth assignment, propositionally satisfies all the formulas in the input set $\varDelta$. The SMT solver considers all quantified formulas $\forall \varvec{x}.\,\psi [ \varvec{x} ]$ in the current set M, and for each of these formulas, it may add formulas of these forms to $\varDelta$:

• (i) instantiation clauses $A \Rightarrow \psi [ \varvec{t} ]$

• (ii) Skolemization clauses $B \Rightarrow \lnot \psi [ \varvec{v} ]$, with $\varvec{v}$ a tuple of fresh variables, and

• (iii) connecting clauses $\forall \varvec{x}.\,\psi [ \varvec{x} ] \Rightarrow A$ and $\lnot \forall \varvec{x}.\,\psi [ \varvec{x} ] \Rightarrow B$,

where A and B are fresh Boolean constants, which we call the positive and negative instantiation guards of $\forall \varvec{x}.\,\psi$. Note that none of these clauses changes the satisfiability of $\varDelta$. The second and third kinds of clauses are added once, at the time the quantified formula first occurs in an assignment M. From then on, every occurrence of $\forall \varvec{x}.\,\psi$ in a formula of $\varDelta$ or M is treated abstractly, as if it were a propositional variable. The solver detects that the negation of a quantified formula along with the current set of clauses $\varDelta$ is T-unsatisfiable by checking which negative guards must be assigned $\bot$ (false). In practice, this is determined by a decision heuristic which, when faced with the choice of guessing the value of a negative instantiation guard, always tries $\top$ first. When a quantified formula $\forall \varvec{x}.\,\psi$ and its corresponding negative guard both end up being assigned value $\top$, the SMT solver adds an instantiation lemma to $\varDelta$ for $\forall \varvec{x}.\,\psi$ based on the selection function from Fig. 3. The process terminates as usual when the set $\varDelta$ is proved T-unsatisfiable, or when the solver finds a T-satisfiable satisfying assignment where either the quantified formula or its negative guard are assigned $\bot$.

This scheme allows us to handle multiple quantified formulas simultaneously. It further allows us to handle quantified formulas with arbitrary nesting by simply allowing formulas like $\psi [ \varvec{x} ]$ above to contain quantifiers. The resulting quantifiers in instantiation and Skolemization lemmas $A \Rightarrow \psi [ \varvec{t} ]$ and $B \Rightarrow \lnot \psi [ \varvec{v} ]$ are recursively handled by introducing instantiation and Skolemization lemmas for quantified formulas that appear in subsequent satisfying assignments as a result of processing those lemmas.

4.2.6 Negating the input formula

Our version of counterexample-guided quantifier instantiation is most effective for checking the T-satisfiability of closed universal formulas of the form $\forall \varvec{x}.\,\psi [\varvec{x} ]$. In the theory of bit-vectors $T_{BV}$, for a formula of the form $\exists \varvec{y}.\,\forall \varvec{x}.\,\psi [\varvec{x}, \varvec{y} ]$ (with $\varvec{y}$ non-empty) we consider instead the (closed) universal formula corresponding to its negation $\forall \varvec{y}.\,\exists \varvec{x}.\,\lnot \psi [\varvec{x}, \varvec{y} ]$. Although this does not permit Skolemization of the top-level quantification on $\varvec{y}$, the negated version of this formula may be significantly easier to solve, since our techniques may find an instantiation for $\varvec{y}$ that quickly leads to a proof of unsatisfiability.

Note that checking the satisfiability of the negated input formula is meaningful because $T_{BV}$ is complete, which guarantees that either the formula or its negation is $T_{BV}$-unsatisfiable. This means that if our procedure determines the negation of a formula is $T_{BV}$-unsatisfiable, we can conclude the original formula is $T_{BV}$-satisfiable, and vice versa.

5 Evaluation

We implemented our techniques in the solver $\mathbf{CVC4}$ and considered four configurations $\mathbf{\mathbf{CVC4}}_{c}$ with c one of {${\mathbf {m}}$, ${\mathbf {k}}$, ${\mathbf {s}}$, ${\mathbf {b}}$}, corresponding to the four selection function configurations described in Sect. 4. Out of these four configurations, $\mathbf{\mathbf{CVC4}}_{{\mathbf {m}}}$ is the only one that does not employ our new techniques but uses only model values for instantiation. It can thus be considered our base configuration. All configurations enable the optimizations described in Sect. 4.2 when applicable. We compared them against all entrants of the quantified bit-vector division of the 2017 SMT competition SMT-COMP: Boolector [19], CVC4 [2], Q3B [16] and Z3 [6]. With the exception of Q3B, all solvers are related to our approach since they are instantiation-based. However, none of these solvers utilizes invertibility conditions when constructing instantiations. We ran all experiments on the StarExec logic solving service [29] with a 300 second CPU and wall clock time limit, and a 100 GB memory limit. None of the solvers hit the memory limit on any benchmark.

Table 8 Results of the four CVC4 configurations {${\mathbf {m}}$, ${\mathbf {k}}$, ${\mathbf {s}}$, ${\mathbf {b}}$} and the SMT solvers Boolector, CVC4, Q3B, and Z3 on all 5151 BV benchmarks with a 300 second time limit

We evaluated our approach on all 5,151 benchmarks from the quantified bit-vector logic (BV) of SMT-LIB [3]. The results are summarized in Table 8 and Figs. 4, 5. Configuration $\mathbf{\mathbf{CVC4}}_{{\mathbf {b}}}$ solves the highest number of unsatisfiable benchmarks (4, 399), which is 30 more than the next best configuration $\mathbf{\mathbf{CVC4}}_{{\mathbf {s}}}$ and 37 more than the next best external solver, Z3. Compared to the instantiation-based solvers Boolector, CVC4 and Z3, the performance of $\mathbf{\mathbf{CVC4}}_{{\mathbf {b}}}$ is particularly strong on the h-uauto family, which consists of verification conditions from the Ultimate Automizer tool [13]. For satisfiable benchmarks, Boolector solves the most (581), which is 36 more than our best configuration $\mathbf{\mathbf{CVC4}}_{{\mathbf {b}}}$.

Fig. 4

Results on all BV benchmarks with a 300 second time limit

Fig. 5

(Un)satisfiable results on all BV benchmarks with a 300 second time limit

Overall, our best configuration $\mathbf{\mathbf{CVC4}}_{{\mathbf {b}}}$ solved 335 more benchmarks than our base configuration $\mathbf{\mathbf{CVC4}}_{{\mathbf {m}}}$. A more detailed runtime comparison between all configurations is provided by the scatter plots in Fig. 6. We add that $\mathbf{\mathbf{CVC4}}_{{\mathbf {b}}}$ solved 24 more benchmarks than the best external solver, Z3. Looking at uniquely solved instances, $\mathbf{\mathbf{CVC4}}_{{\mathbf {b}}}$ was able to solve 139 benchmarks that were not solved by Z3, whereas Z3 solved 115 benchmarks that $\mathbf{\mathbf{CVC4}}_{{\mathbf {b}}}$ did not. Overall, $\mathbf{\mathbf{CVC4}}_{{\mathbf {b}}}$ was able to solve 21 of the 79 benchmarks (26.6%) not solved by any of the other solvers. For 18 of these 21 benchmarks, it terminated after considering no more than 4 instantiations. These cases indicate that using symbolic terms for instantiation solves problems for which other techniques, such as those that enumerate instantiations based on model values, do not scale.

Interestingly, configuration $\mathbf{\mathbf{CVC4}}_{{\mathbf {k}}}$, despite having the strong guarantees given by Theorem 14, performed relatively poorly on this set (with 4, 571 solved instances overall). We attribute this to the fact that most of the quantified formulas in this set are not unit linear invertible. In total, we found that only 25.6% of the formulas considered during solving were unit linear invertible. However, only a handful of benchmarks were such that all quantified formulas in the problem were unit linear invertible. This might explain the superior performance of $\mathbf{\mathbf{CVC4}}_{{\mathbf {s}}}$ and $\mathbf{\mathbf{\mathbf{CVC4}}_{{\mathbf {b}}}}$ which use invertibility conditions but in a less monolithic way.

Fig. 6

Runtime comparison of base configuration $\mathbf{\mathbf{CVC4}}_{{\mathbf {m}}}$ against configurations $\mathbf{\mathbf{CVC4}}_{{\mathbf {b}}}$, $\mathbf{\mathbf{CVC4}}_{{\mathbf {s}}}$, and $\mathbf{\mathbf{CVC4}}_{{\mathbf {k}}}$

For some intuition on this, consider the problem $\forall x.\,(x > a \vee x < b)$ where a and b are such that $a>b$ is $T_{BV}$-valid. Intuitively, to show that this formula is unsatisfiable requires the solver to find an x between b and a. This is apparent when considering the dual problem $\exists x.\,(x \le a \wedge x \ge b)$. Configuration $\mathbf{\mathbf{CVC4}}_{{\mathbf {b}}}$ is capable of finding such an x, for instance, by considering the instantiation $x \mapsto a$ when solving for the boundary point of the first disjunct. Configuration $\mathbf{\mathbf{CVC4}}_{{\mathbf {k}}}$, on the other hand, would instead consider the instantiation of x for two terms that witness $\varepsilon$-expressions: some $k_1$ that is never smaller than a, and some $k_2$ that is never greater that b. Neither of these terms necessarily resides in between a and b since the solver may subsequently consider models where $k_1 > b$ and $k_2 < a$. This points to a potential use for invertibility conditions that solve multiple literals simultaneously, something we are currently investigating.

6 Conclusion

We have presented a new class of strategies for solving quantified bit-vector formulas based on invertibility conditions. We have derived invertibility conditions for the majority of operators in a standard theory of fixed-width bit-vectors. An implementation based on this approach solves over 25% of previously unsolved verification benchmarks from SMT LIB and outperforms all other state-of-the-art bit-vector solvers overall.

In future work, we plan to work on deriving invertibility conditions that are optimal for linear constraints, in the sense of admitting the simplest propositional encoding. We also intend to investigate conditions that cover additional bit-vector operators, some cases of non-linear literals, as well as conditions that cover multiple constraints. While this is a challenging task, we believe that efficient syntax-guided synthesis solvers can continue to help push progress in this direction. Finally, we plan to investigate the use of invertibility conditions for quantifier elimination in bit-vector constraints. This will most likely require a procedure for generating concrete witnesses from choice expressions.