Abstract
The inference of program invariants over machine arithmetic, commonly called bitvector arithmetic, is an important problem in verification. Techniques that have been successful for unbounded arithmetic, in particular Craig interpolation, have turned out to be difficult to generalise to machine arithmetic: existing bitvector interpolation approaches are based either on eager translation from bitvectors to unbounded arithmetic, resulting in complicated constraints that are hard to solve and interpolate, or on bitblasting to propositional logic, in the process losing all arithmetic structure. We present a new approach to bitvector interpolation, as well as bitvector quantifier elimination (QE), that works by lazy translation of bitvector constraints to unbounded arithmetic. Laziness enables us to fully utilise the information available during proof search (implied by decisions and propagation) in the encoding, and this way produce constraints that can be handled relatively easily by existing interpolation and QE procedures for Presburger arithmetic. The lazy encoding is complemented with a set of native proof rules for bitvector equations and nonlinear (polynomial) constraints, this way minimising the number of cases a solver has to consider. We also incorporate a method for handling concatenations and extractions of bitvector efficiently.
Introduction
Craig interpolation is a commonly used technique to infer invariants or contracts in verification. Over the last 15 years, efficient interpolation techniques have been developed for a variety of logics and theories, including propositional logic [1, 2], uninterpreted functions [1, 3, 4], firstorder logic [5,6,7], algebraic datatypes [8, 9], linear real arithmetic [1], nonlinear real arithmetic [10], Presburger arithmetic [4, 11, 12], and arrays [13,14,15].
A theory that has turned out notoriously difficult to handle in Craig interpolation is bounded machine arithmetic, commonly called bitvector arithmetic. Decision procedures for bitvectors are predominantly based on bitblasting, in combination with sophisticated preprocessing and simplification methods, which implies that also extracted interpolants stay on the level of propositional logic and are difficult to map back to compact highlevel bitvector constraints. An alternative interpolation approach translates bitvector constraints to unbounded integer arithmetic formulas [16], but is limited to linear constraints and tends to produce integer formulas that are hard to solve and interpolate, due to the necessary introduction of additional variables and large coefficients to model wraparound semantics correctly.
In this article, we introduce a new Craig interpolation method for bitvector arithmetic, initially focusing on arithmetic bitvector operations including addition, multiplication, and division. Like [16], we compute interpolants by reducing bitvectors to unbounded integers; unlike in earlier approaches, we define a calculus that carries out this reduction lazily, and can therefore dynamically choose between multiple possible encodings of the bitvector operations. This is done by initially representing bitvector operations as uninterpreted predicates, which are expanded and replaced by Presburger arithmetic expressions on demand. The calculus also includes native rules for nonlinear constraints and bitvector equations, so that formulas can often be proven without having to resort to a full encoding as integer constraints. Our approach gives rise to both Craig interpolation and quantifier elimination (QE) methods for bitvector constraints, with both procedures displaying competitive performance in our experiments.
Reduction of bitvectors to unbounded integers has the additional advantage that integer and bitvector formulas can be combined efficiently, including the use of conversion functions between both theories, which are difficult to support using bitblasting. This combination is of practical importance in software verification, since programs and specifications often mix machine arithmetic with arbitraryprecision numbers; tools might also want to switch between integer semantics (if it is known that no overflows can happen) and bitvector semantics for each individual program instruction.
This is an extended version of a paper presented at FMCAD 2018 [17]. Compared to the conference version, this article considers an extended fragment of bitvector logic, including also concatenation and extraction operations on bitvectors, as well as bitwise operators like \(\mathsf {bvor}\) or \(\mathsf {bvnot}\). We show that the representation of concatenation and extraction using uninterpreted predicates is sufficient to obtain an interpolation procedure for the quantifierfree structural fragment of bitvector logic, i.e., bitvector constraints with only concatenation, extraction, and positive equations [18, 19]. Bitwise operations are handled via a direct translation to Presburger arithmetic akin to bitblasting.
The contributions of the article are: a new calculus for nonlinear integer arithmetic, which can eliminate quantifiers (in certain cases) and extract Craig interpolants (Sect. 3); a corresponding calculus for arithmetic bitvector constraints (Sect. 4); the extension of the calculus to handle concatenation, extraction, and bitwise operations (Sect. 5); an experimental evaluation using SMTLIB and model checking benchmarks (Sect. 6).
Example 1: Interpolating arithmetic bitvector operations
We start by considering one of the examples from [16], the interpolation problem \(A \wedge B\) defined by
where all variables range over unsigned 8bit bitvectors. The function \(\mathsf {bvadd}_8\) represents addition of two bitvectors, while the predicate \(\mathsf {bvule}_8\) is the unsigned \(\le \) comparison. An interpolant for \(A \wedge B\) is a formula I such that the implications \(A \Rightarrow I\) and \(B \Rightarrow \lnot I\) hold, and such that only variables common to A and B occur in I.
An eager encoding into Presburger arithmetic (linear integer arithmetic, LIA) would typically add variables to handle wraparound semantics, e.g., mapping \(y_4' =\mathsf {bvadd}_8(y_4, 1)\) to \(y_4' = y_4 + 1  2^8\sigma _1 \wedge 0 \le y_4' < 2^8 \wedge 0 \le \sigma _1 \le 1\). This yields a formula in Presburger arithmetic that exactly models the bitvector semantics, and can be solved and interpolated using existing methods implemented in SMT solvers. Interpolants can be mapped back to a pure bitvector formula if needed. However, additional variables and large coefficients tend to be hard both for solving and interpolation; the LIA interpolant presented in [16] for \(A \wedge B\) is the somewhat complicated formula \(I_{ LIA } = 255 \le y_2  y_3 + 256\lfloor 1 \frac{y_2}{256}\rfloor \).
Our approach translates bitvector formulas to our core language — an extension of Presburger arithmetic with constructs to express bitvector domains, wraparound semantics and operations that can be simplified in different ways, such as bvmul. For example, domain predicate \( in _{w}(x)\) expresses that variable x belongs to the value range of a bitvector of width w. Similarly, predicate \( ubmod_{w} (x, y)\) expresses the unsigned wraparound semantics without explicitly encoding it. Translating A and B to the core language yields:
where \(\psi _A = in _{8}(y_2) \wedge in _{8}(y_3) \wedge in _{8}(y_4) \wedge in _{8}(c_1)\) and \(\psi _B = in _{8}(y_2) \wedge in _{8}(y_3) \wedge in _{8}(y_7) \wedge in _{8}(c_2)\) capture the domain constraints.
The core language enables a layered calculus that encodes predicates on a case by case basis, preferring simpler encodings whenever possible. In our example, rule bmodsplit splits the \( ubmod_{8} (y_2 + 1, c_2)\) into the only two relevant cases based on the bounds of \(y_2\) implied by \(A_{\text {core}}, B_{\text {core}}\):
Due to \(y_7 =3 \wedge y_7 =c_2\), the cases reduce to \(y_2 =2\) and \(y_2 =258\), and immediately contradict \(A_{\text {core}}, B_{\text {core}}\).
When variable bounds are tight enough and there are only a few cases, case splits are more efficient than \(\sigma \) variables. However, that is not always the case and our calculus lazily decides how to handle each occurrence. Simpler proofs also lead to simpler and more compact interpolants; using our lazy approach, the final interpolant in the example is \(I_{ LAZY } = y_3 <y_2\), which is simple and avoids the division operator in \(I_{ LIA }\). We will revisit this example in Sect. 4.4 and explain in greater detail how this interpolant is obtained.
Example 2: Interpolating structural bitvector operations
We continue with a (reduced) example taken from [19], a formula of equalities between (slices of) bitvectors of length 8:
where x[u : l] is the extraction of the slice of bits from uth down to lth (inclusive). In the previous example the bitvector formula was translated to integer arithmetic, however this can sometimes be inefficient when dealing with structural bitvector operations, e.g., extractions and concatenations. A direct translation to integer arithmetic has a hard time to isolate the conflict, since integer operations cannot capture extractions in a natural way. Instead, it is possible to split the bitvectors into segments
x[5:0] = 22  y[7:2] = 6  x = y 

y[7:6] = 0  x[7:6] = y[7:6]  
x[5:2] = 5  y[5:2] = 6  x[5:2] = y[5:2] 
x[1:0] = 2  x[1:0] = y[1:0] 
Given this decomposition of the bitvectors, it is easy see the conflict \(x[5:2] = 5 \ne 6 = y[5:2]\) without a translation to integers. Interpolants can in this setting be extracted by referring to individual slices of bitvectors, with the help of the extraction operator. In Sect. 5 we show how bitvectors can be decomposed in this manner using an interpolating calculus.
Related work
Most SMT solvers handle bitvectors using bitblasting and SAT solving, and usually cannot extract interpolants for bitvector problems. The exception is MathSAT [20], which uses a layered approach [16] to compute interpolants: MathSAT first tries to compute interpolants by keeping bitvector operations uninterpreted; then using a restricted form of quantifier elimination; then by eager encoding into linear integer arithmetic (LIA); and finally through bitblasting. Our approach has some similarities to the LIA encoding, but can choose simpler encodings thanks to laziness, and also covers nonlinear arithmetic constraints.
A similarly layered approach, proposed in [21], can be used to compute function summaries in bounded model checking. When bounded model checking is able to prove (bounded) safety of a program, Craig interpolation can subsequently be used to extract function summaries; such summaries can later be useful to speed up other verification tasks. To handle bitvector constraints in this context, [21] successively applies more and more precise overapproximations of bitvectors: using uninterpreted functions, linear real arithmetic, and finally using precise bitblasting. Interpolants are computed in the coarsest theory that was able to prove safety of a verification task.
Other related work has focused on interpolation for fragments of bitvector logic. In [22], an algorithm is given for reconstructing bitvector interpolants from bitlevel interpolants, however restricted to the case of bitvector equalities. An interpolation procedure based on a set of tailormade (but incomplete) rewriting rules for bitvectors is given in [23].
Looking more generally at model checking for finitestate systems formulated over the theory of bitvectors (often called wordlevel model checking), lazy approaches to handle complex bitvector operations have been proposed. In [24], an approximation method for model checking RTL designs is defined that instantiates complex bitvector operations lazily. Initially, such operations are overapproximated by leaving the results unconstrained; when spurious counterexamples occur, the approximation is refined by adding additional constraints, or ultimately by precisely instantiating the operator. Such approaches are independent of the underlying finitestate model checking algorithm, and do not necessarily involve Craig interpolation, however.
The core logic of bitvectors (formulas with only concatenation, extraction, and positive equations) was identified in [18] to be solvable in polynomial time.^{Footnote 1} Our work is inspired by the decompositionbased decision procedure for this fragment developed in [19], where the authors present an algorithm together with a datastructure designed for solving formulas over the core logic of bitvectors efficiently. To the best of our knowledge, Craig interpolation for the structural fragment has not been considered previously.
Preliminaries: the base logic
We formulate our approach on top of a simple logic of Presburger arithmetic constraints combined with uninterpreted predicates, introduced in [25] and extended in [4, 11] to support Craig interpolation. Let x range over an infinite set X of variables, c over an infinite set C of constants, p over a set P of predicate symbols with fixed arity, and \(\alpha \) over the set \(\mathbb {Z}\) of integers. The syntax of terms and formulas is defined by the following grammar:
The symbol t denotes terms of linear arithmetic. Substitution of a term t for a variable x in \(\phi \) is denoted by \([x/t]\phi \); we assume that variable capture is avoided by renaming bound variables as necessary. For simplicity, we sometimes write \(s =t\) as a shorthand of \(s  t =0\), inequalities \(s \le t\) and \(t \ge s\) for \(st \le 0\), and \(\forall c. \phi \) as a shorthand of \(\forall x. [c/x]\phi \) if c is a constant. The abbreviation \( true \) (\( false \)) stands for equality \(0 =0\) (\(1 =0\)), and the formula \(\phi \rightarrow \psi \) abbreviates \(\lnot \phi \vee \psi \). Semantic notions such as structures, models, satisfiability, and validity are defined as is common (e.g., [26]), but we assume that evaluation always happens over the universe \(\mathbb {Z}\) of integers; bitvectors will later be defined as a subset of the integers.
A sequent calculus for the base logic
For checking whether a formula in the base logic is satisfiable or valid, we work with the calculus presented in [25], a part of which is shown in Fig. 1. If \(\varGamma \), \(\varDelta \) are finite sets of formulas, then is a sequent. A sequent is valid if the formula \(\bigwedge \varGamma \rightarrow \bigvee \varDelta \) is valid. Positions in \(\varDelta \) that are underneath an even/odd number of negations are called positive/negative; and vice versa for \(\varGamma \). Proofs are trees growing upward, in which each node is labeled with a sequent, and each nonleaf node is related to the node(s) directly above it through an application of a calculus rule. A proof is closed if it is finite and all leaves are justified by an instance of a rule without premises. Soundness of the calculus implies that the root of a closed proof is a valid sequent.
In addition to propositional and quantifier rules in Fig. 1, the calculus in [25] also includes rules for equations and inequalities in Presburger arithmetic; the details of those rules are not relevant for this paper. The calculus is complete for quantifierfree formulas in the base logic, i.e., for every valid quantifierfree sequent a closed proof can be found. It is wellknown that the base logic including quantifiers does not admit complete calculi [27], but as discussed in [25] the calculus can be made complete (by adding slightly more sophisticated quantifier handling) for interesting undecidable fragments, for instance for sequents \({}\;\vdash \;{\phi }\) in which \(\phi \) contains \(\exists \)/\(\forall \) only under an even/odd number of negations.
For quantifierfree input formulas, proof search can be implemented in depthfirst style following the core concepts of DPLL(T) [28]: rules with multiple premises correspond to decisions and explore the branches one by one; rules with a single premise represent propagation or rewriting; and logging of rule applications is used in order to implement conflictdriven learning and proof extraction. For experiments, we use the implementation of the calculus in Princess.^{Footnote 2}
Quantifier elimination in the base logic
The sequent calculus can eliminate quantifiers in Presburger arithmetic, i.e., in the base logic without uninterpreted predicates, since the arithmetic calculus rules are designed to systematically eliminate constants. To illustrate this use case, suppose \(\phi \) is a formula without uninterpreted predicates (\(P = \emptyset \)) and without constants c, but possibly containing variables x. Formula \(\phi \) furthermore only contains \(\forall \)/\(\exists \) under an even/odd number of negations, i.e., all quantifiers are effectively universal. To compute a quantifierfree formula \(\psi \) that is equivalent to \(\phi \), we can construct a proof with root sequent \({}\;\vdash \;{\phi }\), and keep applying rules until no further applications are possible in any of the remaining open goals \(\{{\varGamma _i}\;\vdash \;{\varDelta _i} \mid i = 1, \ldots , n\}\). In this process, rules \(\exists \) left and \(\forall \) right can introduce fresh constants, which are subsequently isolated and eliminated by the arithmetic rules. To find \(\psi \), it is essentially enough to extract the constantfree formulas \(\varGamma ^v_i \subseteq \varGamma _i\), \(\varDelta ^v_i \subseteq \varDelta _i\) in the open goals, and construct \(\psi = \bigwedge _{i=1}^n (\bigwedge \varGamma ^v_i \rightarrow \bigvee \varDelta ^v_i)\).
The full calculus [25] is moreover able to eliminate arbitrarily nested quantifiers, and can be used similarly to prove validity of sequents with quantifiers. A recent independent evaluation [29] showed that the resulting proof procedure is competitive with stateoftheart SMT solvers and theorem provers on a wide range of quantified integer problems.
Craig interpolation in the base logic
Given formulas A and B such that \(A\wedge B\) is unsatisfiable, Craig interpolation can determine a formula I such that the implications \(A \Rightarrow I\) and \(B \Rightarrow \lnot I\) hold, and nonlogical symbols in I occur in both A and B [30]. An interpolating version of our sequent calculus has been presented in [4, 11], and is summarised in Fig. 2. To keep track of the partitions A, B, the calculus operates on labeled formulas \(\lfloor \phi \rfloor _L\) (with L for “left”) to indicate that \(\phi \) is derived from A, and similarly formulas \(\lfloor \phi \rfloor _R\) for \(\phi \) derived from B. If \(\varGamma \), \(\varDelta \) are finite sets of L/Rlabeled formulas, and I is an unlabeled formula, then is an interpolating sequent.
Semantics of interpolating sequents is defined using the following projections: \({\varGamma }_L =_{\text {def}}\{ \phi \mid \lfloor \phi \rfloor _L \in \varGamma \}\) and \({\varGamma }_R =_{\text {def}}\{ \phi \mid \lfloor \phi \rfloor _R \in \varGamma \}\), which extract the L/Rparts of a set \(\varGamma \) of labeled formulas. A sequent is valid if 1. the sequent \({{\varGamma }_L}\;\vdash \;{I, {\varDelta }_L}\) is valid, 2. the sequent \({{\varGamma }_R,I}\;\vdash \;{{\varDelta }_R}\) is valid, and 3. constants and predicates in I occur in both \({\varGamma }_L \cup {\varDelta }_L\) and \({\varGamma }_R \cup {\varDelta }_R\). As a special case, note that the sequent \({\lfloor A\rfloor _L, \lfloor B\rfloor _R}\;\vdash _{}\;{\emptyset }\;\blacktriangleright {I}\) is valid iff I is an interpolant of \(A \wedge B\). Soundness of the calculus guarantees that the root of a closed interpolating proof is a valid interpolating sequent.
To solve an interpolation problem \(A \wedge B\), a prover typically first constructs a proof of \({A, B}\;\vdash \;{\emptyset }\) using the ordinary calculus from Sect. 2.1. Once a closed proof has been found, it can be lifted to an interpolating proof: this is done by replacing the root formulas A, B with \(\lfloor A\rfloor _L, \lfloor B\rfloor _R\), respectively, and recursively assigning labels to all other formulas as defined by the rules from Fig. 2. Then, starting from the leaves, intermediate interpolants are computed and propagated back to the root, leading to an interpolating sequent \({\lfloor A\rfloor _L, \lfloor B\rfloor _R}\;\vdash _{}\;{\emptyset }\;\blacktriangleright {I}\).
Solving nonlinear constraints
We extend the base logic in three steps: in this section, symbols and rules are added to solve nonlinear diophantine problems; a second extension is then done in Sect. 4 to handle arithmetic bitvector constraints; and, finally, additional symbols to express structural bitvector constraints are introduced in Sect. 5. All constructions preserve the ability of the calculus to eliminate quantifiers (under certain assumptions) and derive Craig interpolants.
For nonlinear constraints, we assume that the set P of predicates contains a distinguished ternary predicate \(\times \), with the intended semantics that the third argument represents the result of multiplying the first two arguments, i.e., \(\times (s, t, r) \Leftrightarrow s \cdot t =r\). The predicate \(\times \) is clearly sufficient to express arbitrary polynomial constraints by introducing a \(\times \)literal for each product in a formula, at the cost of introducing a linear number of additional constants or existentially quantified variables. We make the simplifying assumption that \(\times \) only occurs in negative positions; that means, toplevel occurrences will be on the lefthand side of sequents. Positive occurrences can be eliminated thanks to the equivalence \(\lnot \times (s, t, r) \Leftrightarrow \exists x. (\times (s, t, x) \wedge x \not = r)\).
Calculus rules for nonlinear constraints
We now introduce classes of calculus rules to reason about the \(\times \)predicate. The rules are necessarily incomplete for proving that a sequent is valid, but they are complete for finding counterexamples: if \(\phi \) is a satisfiable quantifierfree formula with \(\times \) as the only predicate symbol, then it is possible to construct a proof for \({\phi }\;\vdash \;{\emptyset }\) that has an open and unprovable goal in pure Presburger arithmetic (by systematically splitting variable domains, Sect. 3.1.4). The rule classes are:

Deriving Implied Equalities with Gröbner Bases: if implied linear equalities can be found using Buchberger’s algorithm these can be added to the proof goal.

Interval Constraint Propagation: if new bounds for constants can be derived from existing bounds these can be added to the proof goal.

CrossMultiplication of Inequalities:, if two terms are known to be nonnegative, then the nonnegativity of their product can be added to the proof goal.

Interval Splitting: as a last resort, the proof branch can be split by dividing the possible values for a constant or variable in half.

\(\times \)Elimination: if a occurrence of \(\times \) is implied by other literals, it can be eliminated from the proof goal.
Deriving implied equalities with Gröbner bases
The first rule applies standard algebra methods to infer new equalities from multiplication literals. To avoid the computation of more and more complex terms in this process, we restrict the calculus to the inference of linear equations that can be derived through computation of a Gröbner basis.^{Footnote 3} Given a set \(\{\times {(s_i,t_i,r_i)}\}_{i=1}^n\) of \(\times \)literals and a set \(\{e_j =0\}_{j=1}^m\) of linear equations, the generated ideal \(I = Ideal (\{s_i \cdot t_i  r_i\}_{i=1}^n \cup \{e_j\}_{j=1}^m)\) over rational numbers is the smallest set of rational polynomials that contains \(\{s_i \cdot t_i  r_i\}_{i=1}^n \cup \{e_j\}_{j=1}^m\), is closed under addition, and closed under multiplication with arbitrary rational polynomials [31]. Any \(f \in I\) corresponds to an equation \(f =0\) that logically follows from the literals, and can therefore be added to a proof goal:
To see how this rule can be applied practically, note that the subset of linear polynomials in I forms a rational vector space, and therefore has a finite basis. It is enough to apply \(\times \) eq for terms \(f_1, \ldots , f_k\) corresponding to any such basis, since linear arithmetic reasoning (in the base logic) will then be able to derive all other linear polynomials in I. To compute a basis \(f_1, \ldots , f_k\), we can transform \(\{s_i \cdot t_i  r_i\}_{i=1}^n \cup \{e_j\}_{j=1}^m\) to a Gröbner basis using Buchberger’s algorithm [32], and then apply Gaussian elimination to find linear basis polynomials (or directly by choosing a suitable monomial order).
Example 1
Consider the formula for the square of a sum: \((x+y)^2 = x^2 + 2xy + y^2\). We can show its validity by rewriting it to normal form and constructing a proof. Let \(\varPi = \{\times (x, x, c_1), \times (x, y, c_2), \times (y, y, c_3), \times (x+y, x+y, c_4)\}\):
Here, the \(\times \) eqstep is motivated by the fact that the Gröbner basis derived from \(\varPi \) contains the linear polynomial \(c_1 + 2c_2 + c_3  c_4\), from which the desired equation can be derived using linear reasoning (using calculus rules not presented in this paper, see Sect. 2.1).
Interval constraint propagation (ICP)
Our main technique for inequality reasoning in the presence of \(\times \)predicates is interval constraint propagation (ICP) [33]. ICP is a fixedpoint computation on the lattice \(\mathbb {I}^S\) of functions mapping constants and variables \(S = C \cup X\) to intervals \(\mathbb {I}\), and can efficiently approximate the value ranges of symbols. We define the lattice \(\mathbb {I}\) of intervals and the lattice \(\mathbb {I}^S\) of interval assignments as follows; \(S \rightarrow \mathbb {I}\) represents the set of (total) functions from \(S = C \cup X\) to \(\mathbb {I}\), and \(\bot \) is the distinguished bottom element of \(\mathbb {I}^S\):
We denote the (pointwise) join and meet on \(\mathbb {I}^S\) with \(\sqcup , \sqcap \), respectively.
To define the fixedpoint computation, we then introduce abstraction and concretisation functions that connect the lattice \(\mathbb {I}^S\) with the powerset lattice \(\mathcal{P}(S \rightarrow \mathbb {Z})\) of value assignments. The abstraction of a set \(V \in \mathcal{P}(S \rightarrow \mathbb {Z})\) of value assignments is the least element \(\alpha (V)\) of \(\mathbb {I}^S\) such that the interval \(\alpha (V)(c)\) assigned to a symbol \(c \in S\) contains all values of c in V (or \(\alpha (V) = \bot \) if V is empty). The abstraction function \(\alpha : \mathcal{P}(S \rightarrow \mathbb {Z}) \rightarrow \mathbb {I}^S\) is formally defined as follows:
The concretisation \(\gamma (I)\) of some interval assignment \(I \in \mathbb {I}^S\) is the set V of all value assignments that stay within the intervals specified by I. More formally, \(\gamma : \mathbb {I}^S \rightarrow \mathcal{P}(S \rightarrow \mathbb {Z})\) is defined by:
The result of ICP can then be defined as the greatest fixedpoint of a monotonic propagation function \( Prop : \mathbb {I}^S \rightarrow \mathbb {I}^S\) on the lattice \(\mathbb {I}^S\). Propagation can be defined separately for each formula occurring in a sequent; in particular, propagation \( Prop _{\phi } : \mathbb {I}^S \rightarrow \mathbb {I}^S\) for a multiplication literal \(\phi = \times (s, t, r)\) is defined as:
This means, propagation eliminates values from the intervals that are inconsistent with \(\times (s, t, r)\). Propagation for equalities \(t =0\) and inequalities \(t \le 0\) is defined similarly; in practice, also any monotonic overapproximation of \( Prop _{\phi }\) can be used instead of \( Prop _{\phi }\), at the cost of more overapproximate results in the end.
Given a set \(\{\phi _1, \ldots , \phi _n\}\) of formulas, the overall propagation function \( Prop = Prop _{\{\phi _1, \ldots , \phi _n\}}\) is the meet of the individual propagators:
The ICP rule assumes that a greatest fixedpoint \({\text {gfp}} Prop _{\{\phi _1, \ldots , \phi _n\}}\) for equality, inequality, and multiplication literals \(\phi _1, \ldots , \phi _n\) in a sequent has been computed, and adds resulting bounds for a constant c:
Example 2
From two inequalities \(x \ge 5\) and \(y \ge 5\), the rule \(\times \) icp can derive \((x+y)^2 \ge 100\):
The slightly different problem \(x + y \ge 10 \rightarrow (x+y)^2 \ge 100\) cannot be proven in the same way, since ICP will not be able to deduce bounds for x or y from \(x + y \ge 10\).
Crossmultiplication of inequalities
While ICP is highly effective for approximating the range of constants, and quickly detecting inconsistencies, it is less useful for inferring relationships between multiple constants that follow from multiplication literals. We cover such inferences using a crossmultiplication rule that resembles procedures used in ACL2 [34]. The rule captures the fact that if s, t are both nonnegative, then also the product \(s \cdot t\) is nonnegative.
Like in Sect. 3.1.1, we prefer to avoid the introduction of new multiplication literals during proof search. By disallowing nonlinear terms, we avoid the introduction of more and more complex terms and thus only add \(s \cdot t \ge 0\) if the term \(s \cdot t\) can be expressed linearly. For this, we again write \(I = Ideal (\{s_i \cdot t_i  r_i\}_{i=1}^n \cup \{e_j\}_{j=1}^m)\) for the ideal induced by equations and \(\times \)literals:
The term f can practically be found by computing a Gröbner basis of I, and reducing the product \(s \cdot t\) to check whether an equivalent linear term exists.
Interval splitting
If everything else fails, as last resort it can become necessary to systematically split over the possible values of a variable or constant \(c \in C \cup X\):
The \(\alpha \in \mathbb {Z}\) can in principle be chosen arbitrarily in the rule, but in practice a useful strategy is to make use of the range information derived for \(\times \) icp: when no ranges can be tightened any further using \(\times \) icp, instead \(\times \) split can be applied to split one of the intervals in half.
\(\times \)Elimination
Finally, occurrences of \(\times \) can be eliminated whenever a formula is subsumed by other literals in a goal, again writing \(I = Ideal (\{s_i \cdot t_i  r_i\}_{i=1}^n \cup \{e_j\}_{j=1}^m)\):
Note that \(\times \) elim only eliminates nonlinear \(\times \)literals, whereas \(\times \) eq only introduces linear equations, so that the application of the two rules cannot induce cycles.
Quantifier elimination for nonlinear constraints
Due to necessary incompleteness of calculi for Peano arithmetic, quantifiers can in general not be eliminated in the presence of the \(\times \) predicate, even when considering formulas that do not contain uninterpreted predicates. By combining the QE approach in Sect. 2.2 with the rules for \(\times \) that we have introduced, it is nevertheless possible to reason about quantified nonlinear constraints in many practical cases, and sometimes even get rid of quantifiers. This is possible because the rules in Sect. 3.1 are not only sound, but even equivalence transformations: in any application of the rules, the conjunction of the premises is equivalent to the conclusion.
Similarly as in [35], QE is always possible if sufficiently many constants or variables in a formula \(\phi \) range over bounded domains: if there is a set \(B \subseteq C \cup X\) of symbols with bounded domain such that in each literal \(\times (s, t, r)\) either s or t contain only symbols from B. In this case, proof construction will terminate when applying the rule \(\times \) split only to variables or constants with bounded domain. This guarantees that eventually every literal \(\times (s, t, r)\) can be turned into a linear equation using \(\times \) eq, and then be eliminated using \(\times \) elim, only leaving proof goals with pure Presburger arithmetic constraints. The boundedness condition is naturally satisfied for bitvector formulas.
Craig interpolation for nonlinear constraints
To carry over the Craig interpolation approach from Sect. 2.3 to nonlinear formulas, interpolating versions of the calculus rules for the \(\times \)predicate are needed. For this, we follow the approach used in [4] (which in turn resembles the use of theory lemmas in SMT in general): when translating a proof to an interpolating proof, we replace applications of the \(\times \)rules with instantiation of an equivalent theory axiom \( QAx \). Suppose a noninterpolating proof contains a rule application
in which \(\varGamma ', \varDelta '\) are the formulas assumed by the rule application, \(\varGamma , \varDelta \) are side formulas not required or affected by the application, and \(\varGamma _1, \varDelta _1\), ..., \(\varGamma _n, \varDelta _n\) are newly introduced formulas in the individual branches.
The (unquantified) theory axiom \( Ax \) corresponding to the rule application expresses that the conjunction of the premises has to imply the conclusion; the quantified theory axiom \( QAx =_{\text {def}}\forall S.\, Ax \) in addition contains universal quantifiers for all constants \(S \subseteq C\) occurring in \( Ax \).
\( Ax \) and \( QAx \) are specific to the application of R: the axioms for two distinct applications of R will in general be different formulas. \( QAx \) is defined in such a way that it can simulate the effect of R (as in (1)). This is done by introducing \( QAx \) in the antecedent of a sequent, applying the rule \(\forall \) left to instantiate the axiom with the constants S and obtain \( Ax \), and then applying propositional rules. The propositional rules \(\vee \) left and \(\lnot \) left are used to eliminate implications \(\rightarrow \) (which are shorthand for \(\lnot , \vee \)), and the rule \(\wedge \) right to eliminate the conjunction \(\bigwedge _{i=1}^n\):
This construction leads to a proof using only the standard rules from Sect. 2.1, which can be interpolated as discussed earlier. Since \( QAx \) is a valid formula not containing any constants, it can be introduced in a proof at any point, and labelled \(\lfloor QAx \rfloor _L\) or \(\lfloor QAx \rfloor _R\) on demand.
The obvious downside of this approach is the possibility of quantifiers occurring in interpolants. The interpolating rules \(\forall {\textsc {left}}_{L/R}\) (Fig. 2) have to introduce quantifiers \(\forall _{ Rt }\)/\(\exists _{ Lt }\) for local symbols occurring in the substituted term t; whether such quantifiers actually occur in the final interpolant depends on the applied \(\times \)rules, and on the order of rule application. For instance, with \(\times \) split it is always possible to choose the label of \( QAx \) so that no quantifiers are needed, whereas \(\times \) eq might mix symbols from left and right partitions in such a way that quantifiers become unavoidable. In our implementation we approach this issue pragmatically. We leave proof search unrestricted, and might thus sometimes get proofs that do not give rise to quantifierfree interpolants; when that happens, we afterwards apply QE to get rid of the quantifiers. QE is always possible for bitvector constraints, see Sect. 4.4.^{Footnote 4}
Solving bitvector constraints
We now define the extension of the base logic to bitvector constraints. The main idea of the extension is to represent bitvectors of width w as integers in the interval \(\{0, \ldots , 2^w1\}\), and to translate bitvector operations to the corresponding operation in Presburger arithmetic (or possible the \(\times \)predicate for nonlinear formulas), followed by an integer remainder operation to map the result back to the correct bitvector domain. Since the remainder operation tends to be a bottleneck for interpolation, we keep the operation symbolic and initially consider it as an uninterpreted predicate \( bmod_{a}^{b} \). The predicate is only gradually reduced to Presburger arithmetic by applying the calculus rules introduced later in this section.
Formally, we introduce binary predicates \(P_{ bv } = \{ bmod_{a}^{b} \mid a, b \in \mathbb {Z}, a < b \}\). The semantics of each predicate \( bmod_{a}^{b} \) is to relate any whole number \(s \in \mathbb {Z}\) to its remainder modulo \(ba\) in the interval \(\{a, \ldots , b1\}\):
We also introduce shorthand notations for the casts to the unsigned and signed bitvector domains:
Translating bitvector constraints to the core language
For the rest of the section, we use the base logic augmented with \(\times \) and \( bmod_{a}^{b} \)predicates as the core language to which bitvector constraints are translated. For presentation, the translation focuses on a subset of the arithmetic bitvector operations, \(\mathsf {BVOP}_{\mathsf {a}} = \{\mathsf {bvadd}_w\), \(\mathsf {bvmul}_w\), \(\mathsf {bvudiv}_w\), \(\mathsf {bvneg}_w\), \(\mathsf {ze}_{w+w'}\), \(\mathsf {bvule}_w\), \(\mathsf {bvsle}_w\}\). An extension to bitvector concatenation, extraction, and bitwise functions is presented in Sect. 5. All operations are subscripted with the bitwidth of the operands; the zeroextend function \(\mathsf {ze}_{w+w'}\) maps bitvectors of width w to width \(w+w'\). Semantics follows the FixedSizeBitVectors^{Footnote 5} theory of the SMTLIB [36]. Other arithmetic operations, for instance \(\mathsf {bvsdiv}_w\) or \(\mathsf {bvsmod}_w\), can be handled in the same way as shown here, though sometimes the number of cases to be considered is larger.
The translation from bitvector constraints \(\phi \) to core formulas \(\phi _{ core }\) has two parts: first, \(\mathsf {BVOP}_{\mathsf {a}}\) occurrences in a formula \(\phi \) have to be replaced with equivalent expressions in the core language; second, since the core language only knows the sort of unbounded integers, type information has to be made explicit by adding domain constraints.
\(\mathsf {BVOP}_{\mathsf {a}}\) Elimination. Like in Sect. 3, we assume that the bitvector formula \(\phi \) has already been brought into a flat form by introducing additional constants or quantified variables: the operations in \(\mathsf {BVOP}_{\mathsf {a}}\) must not occur nested, and functions only occur in equations of the form \(f(\bar{s}) =t\) in negative positions. The translation from \(\phi \) to \(\phi '\) is then defined by the rewriting rules in Fig. 3. Since the rules for the predicates \(\mathsf {bvsle}_w\) and \(\mathsf {bvule}_w\) distinguish between positive and negative occurrences, we assume that rules are only applied to formulas in negation normalform, and only in negative positions.
The rules for \(\mathsf {bvadd}_w\), \(\mathsf {bvneg}_w\), \(\mathsf {ze}_{w+w'}\), and \(\mathsf {bvule}_w\) simply translate to the corresponding Presburger term, if necessary followed by remainder \( ubmod_{w} \). Multiplication \(\mathsf {bvmul}_w\) is mapped similarly to the \(\times \)predicate defined in Sect. 3, adding an existential quantifier to store the intermediate product. Since rules are only applied in negative positions, the quantified variable can later be replaced with a Skolem constant. An optimised rule could be defined for the case that one of the factors is constant, avoiding the use of the \(\times \)predicate. Translation of \(\mathsf {bvsle}_w\) maps the operands to a signed bitvector domain \(\{2^{w1}, \ldots , 2^{w1}1\}\), in which then the arithmetic inequality predicates \(\le ,>\) can be used. The rule for unsigned division \(\mathsf {bvudiv}_w\) distinguishes the cases that the divisor t is zero or positive (as required by SMTLIB), and maps the latter case to standard integer division.
Domain constraints. Bitvector variables/constants x of width w occurring in \(\phi \) are interpreted as unbounded integer variables in \(\phi _{ core }\), which therefore has to contain explicit assumptions about the ranges of bitvector variables. We use the abbreviation \( in _{w}(x) =_{\text {def}}(0 \le x <2^w)\) and define
where \(S \subseteq C \cup X\) is the set of free variables and constants occurring in \(\phi \), \(w_x\) is the bitwidth of \(x \in S\), and \(\phi '\) is the result of applying rules from Fig. 3 to \(\phi \). Similar constraints are used to express quantification over bitvectors, for instance \(\exists x.~( in _{w}(x) \wedge \ldots )\) and \(\forall x.~( in _{w}(x) \rightarrow \ldots )\).
Example 3
Consider challenge/multiplyOverflow.smt2, a problem from SMTLIB QF_BV containing a bitvector formula that is known to be hard for most SMT solvers since it contains both multiplication and division. In experiments, neither Z3 nor CVC4 could prove the formula within 10min. In our notation, the problem amounts to showing validity of the following implication, with a, b ranging over bitvectors of width 32:
As a flat formula, with additional constants \(c_1\) of width 32 and \(c_2, c_3, c_4\) of width 64, the implication takes the form:
The final formula \(\phi _{ core }\) is obtained by application of the rules in Fig. 3, and adding domain constraints:
Preprocessing and simplification
An encoded formula \(\phi _{ core }\) tends to contain a lot of redundancy, in particular nested or unnecessary occurrences of the \( bmod_{a}^{b} \) predicates. As an important component of our calculus, and in line with the approach in other bitvector solvers, we therefore apply simplification rules both during preprocessing and during the solving phase (“inprocessing”). The most important simplification rules are shown in Fig. 4. Our implementation in addition applies rules for Boolean and Presburger connectives, for instance to inline equations \(x =t\) or to propagate inequalities, not shown here.
The notation expresses that formula \(\phi \) can be rewritten to \(\phi '\), given the set \(\varPi \) of formulas as context. The structural rules in the upper half of Fig. 4 define how formulas are traversed, and how the context \(\varPi \) is extended to \(\varPi , Lit' \) when encountering further literals. We apply the structural rules modulo associativity and commutativity of \(\wedge , \vee \), and prioritise lit\(\vee \)rw and lit\(\wedge \)rw over the other rules. Simplification is iterated until a fixedpoint is reached and no further rewriting is possible. The connection between rewriting rules and the sequent calculus is established by the following rules:
The lower half of Fig. 4 shows three of the bitvectorspecific rules. The boundrw rule defines elimination of \( bmod_{a}^{b} \)predicates that do not require any case splits; the definition of the rule assumes functions \( lbound (\varPi , s)\) and \( ubound (\varPi , s)\) that derive lower and upper bounds of a term s, respectively, given the current context \(\varPi \). The two functions can be implemented by collecting inequalities (and possibly type information available for predicates) in \(\varPi \) to obtain an overapproximation of the range of s.
Rule coeffrw reduces coefficients in \( bmod_{a}^{b} (s, r)\) by adding a multiple of the modulus \(ba\) to s. The rule assumes a wellfounded order \(\prec \) on terms to prevent cycles during simplification. One way to define such an order is to choose a total wellfounded order \(\prec \) on the union \(C \cup X\) of variables and constants, extend \(\prec \) to expressions \(\alpha \cdot x\) by sorting coefficients as \(0 \prec 1 \prec 1 \prec 2 \prec \cdots \), and finally extend \(\prec \) to arbitrary terms \(\alpha _1 t_1 + \cdots + \alpha _n t_n\) as a multiset order [25].
The same order \(\prec \) is used in bmodrw, defining how \( bmod_{a}^{b} (s, r)\) can be rewritten in the context of a second literal \( bmod_{a'}^{b'} (s', r')\). The rule is useful to optimise the translation of nested bitvector operations. Assuming \( bmod_{a'}^{b'} (s', r')\), the value of \(s'  r'\) is known to be a multiple of \(b'  a'\), and therefore \(k \cdot (s'  r')\) is a multiple of \(b  a\) provided that \(ba\) divides \(k \cdot (b'a')\). This implies that the truth value of \( bmod_{a}^{b} (s, r)\) is not affected by adding \(k \cdot (s'  r')\) to s.
Our implementation uses various further simplification rules, for instance to eliminate \(\times \) or \( bmod_{a}^{b} \) whose result is never used; we skip those for lack of space.
Example 4
Consider \(\mathsf {bvadd}_{32}(\mathsf {bvadd}_{32}(a, b), c)\), which corresponds to the expression \( ubmod_{32} (a + b, r_1) \wedge ubmod_{32} (r_1 + c, r_2)\) in the core language. Using bmodrw, the formula can be rewritten to \( ubmod_{32} (a + b, r_1) \wedge ubmod_{32} (a + b + c, r_2)\), provided that \(a + b + c \prec r_1 + c\).
Example 5
We continue Example 3 and show that \(\phi _{ core }\) is valid, focusing on the \(a \ge 1\) case of \(\mathsf {bvudiv}_{32}\). The proof (Fig. 5) consists of three core steps: 1. using \(\times \) icp, from the constraints \( in _{32}(a)\), \( in _{32}(b)\), \(\times (a, b, d)\) the inequalities \(0 \le d\) and \(d \le 2^{64}  2^{33} +1\) can be derived; 2. therefore, using rwleft and boundrw, the literal \( ubmod_{64} (d, c_2)\) can be rewritten to \(d =c_2\), capturing the fact that 64bit multiplication cannot overflow for unsigned 32bit operands; 3. using \(\times \) cross, from the inequalities \(a \ge 1\) and \(b \le c_1\) we derive \((a  1)(c_1 b) = ac_1  ab  c_1 + b \ge 0\). Using the products \(\times (a, b, d)\) and \(\times (a, c_1, e)\), we can express it linearly as \(e  d  c_1 + b \ge 0\). The proof branch can then be closed using standard arithmetic reasoning. The implementation of our procedure can easily find the outlined proof automatically.
Splitting rules for \( bmod_{a}^{b} \)
In general, formulas will of course also contain occurrences of \( bmod_{a}^{b} \) that cannot be eliminated just by simplification. We introduce two calculus rules for reasoning about such general literals \( bmod_{a}^{b} (s, r)\). The first rule makes the assumption that lower and upper bounds of s are available, and are reasonably tight, so that an explicit case analysis can be carried out; the rule generalises boundrw to the situation in which the factors l, u do not coincide:
assuming the bounds \(\big \lfloor \frac{ lbound (\varPi , s)  a}{b  a}\big \rfloor = l\) and \(\big \lfloor \frac{ ubound (\varPi , s)  a}{b  a}\big \rfloor = u\) with \(\varPi = \varGamma \cup \{\lnot \psi \mid \psi \in \varDelta \}\).
If the bounds l, u are too far apart, the number of cases created by bmodsplit would become unmanageable, and it is better to choose a direct encoding of the remainder operation in Presburger arithmetic:
where c is assumed to be a fresh constant. Rule bmodconst corresponds to the encoding chosen in [16].
In practice, it turns out to be advantageous to prioritise rule bmodsplit over bmodconst, as long as the number of cases does not become too big. This is because each of the premises of bmodsplit tends to be significantly simpler to solve (and interpolate) than the conclusion; in addition, splitting one \( bmod_{a}^{b} \) literal often allows subsequent simplifications that eliminate other \( bmod_{a}^{b} \) occurrences. We investigate experimentally in Sect. 6.1 how many applications of the rules bmodsplit and bmodconst are needed to prove formulas satisfiable or unsatisfiable, and show that the numbers are surprisingly low, in particular in the unsatisfiable case.
Quantifier elimination and Craig interpolation
Since the bitvector rules in this section are all equivalence transformations, QE for bitvectors can be done exactly as described in Sect. 3.2. As the ranges of all symbols are now bounded, it is guaranteed that any formula will eventually be reduced to Presburger arithmetic, so that we obtain complete QE for (arithmetic) bitvector constraints.
Similarly, the interpolation approach from Sect. 3.3 carries over to bitvectors, with theory axioms being generated for each of the rules defined in this section. Since the translation of bitvector formulas to the core language happens upfront, also interpolants are guaranteed to be in the core language, and can be mapped back to bitvector formulas if necessary (e.g., as in [16]). Interpolants might contain quantifiers, in which case QE can be applied (as described in the first paragraph), so that we altogether obtain a complete procedure for quantifierfree interpolation of arithmetic bitvector formulas.
In our implementation, we restrict the use of the simplification rules rwleft and rwright when computing proofs for the purpose of interpolation. Unrestricted use could quickly mix up the vocabularies of the individual partitions in an interpolation problem \(A \wedge B\), and thus increase the likelihood of quantifiers in interpolants. Instead we simplify A, B separately upfront using rules in Fig. 4, and apply rwleft, rwright only when the modified formula \(\phi \) is a literal.
Example 6
We recall the example from Sect. 1.1, and show how our calculus finds the simpler interpolant \(I'_{ LIA } = y_3 <y_2\) for the interpolation problem \(A \wedge B\). The core step is to turn the application of bmodsplit into an explicit axiom; after slight simplifications, this axiom is:
The axiom mentions all assumptions made by the rule, including the bounds \(3 \le y_2 <256\) that determine the number of resulting cases (or, alternatively, the formulas \(c_1 > y_3, y_2 =c_1, c_2 \le y_3, y_7 =3, y_7 =c_2\) from which the bounds derive). The axiom also includes domain constraints like \( in _{8}(c_2)\) for occurring symbols, which later ensures that possible quantifiers in interpolants range over bounded domains. The quantified axiom is \( QAx = \forall y_2, c_2.\, Ax \), and can be used to construct an interpolating proof:
We only show one of the cases, \(\mathcal P\), resulting from splitting the axiom \(\lfloor Ax \rfloor _R\) using the rules from Fig. 2. The final interpolant \(I_{ LAZY } = y_3 <y_2\) records the information needed from \(A_{\text {core}}\) to derive a contradiction in the presence of \(y_2 + 1 =c_2\); the branch is closed using standard arithmetic reasoning [11].
Interpolation in the presence of extract and concat
Two bitvector operations which are more tricky to translate to integer arithmetic are the extraction of bits from a larger bitvector, and the concatenation of two bitvectors. This is formalised using the function \(\textsf {bvextract}_{[u, l]}\), which cuts out a slice of \(ul+1\) consecutive bits, and the function \(\textsf {bvconcat}_{v+w}\) forming a bitvector of length \(v+w\). We call the fragment of bitvector logic containing only these operations, and positive equalities, the structural fragment of bitvector theory.
Example 7
Consider the following bitvectors:
where a bitsequence \([b_n, \dots b_0]\) is represented by the number \(\sum _{i=0}^{n} b_i2^i\). The following equations hold between those bitvectors:
While it is possible to translate extractions and concatenations to integer arithmetic, it is not always efficient. We show here that it can be more efficient to keep extractions abstract and only convert at need. This approach can also help to compute simpler interpolants.
Example 8
We consider the example from [19], a formula over the structural fragment, which we divide into two parts
where the bitvectors x, y are of width 8, and z is of width 6. The unsatisfiability of \(A \wedge B\) could be proved, as before, by translating the bitvector constraints to our core language:
Using the interpolation procedure presented in Sect. 4, we can compute the following interpolant:
The conjunction is unsatisfiable due to the conflicting assignment of a small slice in x and y, as illustrated in Fig. 6. However, when translating to integer arithmetic the overall structure is lost, and the interpolant contains a lot of redundancy. The situation gets worse with increasing bitwidths. Consider a formula where the width of x, y are doubled, while the widths of the extractions are kept constant:
The same procedure now yields an interpolant of exponentially greater size:
We will explain in the next sections how more succinct interpolants can be computed by eliminating the extraction operation only lazily.
The structural fragment
In [19], a polynomial fragment of the bitvector theory is identified, consisting of formulas that only contain extractions, concatenations, and positive equalities. The satisfiability of formulas in the structural fragment is decidable in polynomial time by a congruence closure procedure over decomposed bitvectors [18].
Definition 1
The structural fragment consists of bitvector formulas of the form \(\phi _1 \wedge \phi _2 \wedge \dots \wedge \phi _n\) where each \(\phi _i\) is an equation constructed using bitvector variables, concrete bitvectors, and the operators \(\textsf {bvextract}_{[u, l]}\) and \(\textsf {bvconcat}_{v+w}\).
Note that a formula containing \(\textsf {bvconcat}_{v+w}\) can be translated into an equisatisfiable formula that only uses \(\textsf {bvextract}_{[u, l]}\). We illustrate the translation with an example, and introduce the formal rule in Fig. 7. Consider the formula \(\phi [\textsf {bvconcat}_{v+w}(s, t)]\) containing the concatenation of two bitvectors. The concatenation can be eliminated by introducing an existentially quantified variable to represent the result of the concatenation; the relationship with the arguments is established using extraction terms:
To define a formal calculus for the structural fragment, we introduce an extended core language by adding a further family \({P_{ex} = \{extr_l^u \mid u, l \in {\mathbb {N}}, u \ge l\}}\) of predicates representing extraction from bitvectors. Semantically, \(extr_l^u(s,t)\) relates s and t if t is the result of extracting the bits u through l from s. This is formally expressed as the existence of two bitvectors x, y such that t can be made equal to s by prepending x and appending y:
Note that the argument s is not bounded, which implies that the definition contains a bound for the lower slice y, but not for x.
The rewriting rules in Fig. 7 define how extraction and concatenation are translated to the \(P_{ex}\) predicates, following the same schema as in Sect. 4. As a sideeffect of adding \(\textsf {bvextract}_{[u, l]}\) and \(\textsf {bvconcat}_{w+v}\), and moving beyond the structural fragment, the calculus can also reason about the bitwise operators \(\mathsf {BVOP}_{\mathsf {bv}}= \{\mathsf {bvnot}, \mathsf {bvand}, \mathsf {bvor}\), \(\mathsf {bvxor}\}\), by extracting the individual bits of the operands and encoding the Boolean semantics using inequalities. The rewriting rules for such an encoding are given Fig. 7 as well, and are also used in our implementation.
Bitvector decomposition
As demonstrated in Sect. 1.2, unsatisfiability of formulas can sometimes be proven by just focusing on the right slice of bitvectors; the challenge lies in how to decompose the bitvectors to find the conflicts. Intuitively, there is no need to split apart bits which are never constrained individually. We follow the procedure described in [19], and use the notion of cut points for this reason. Cut points of a bitvector variable determine the slices that need to be considered, and the points at which the bitvectors might have to be decomposed, and are determine by the boundaries of extraction operations.
More formally, given a formula \(\phi \) in the structural fragment over set \(S = C \cup X\) of constants and variables, a cut point configuration is a function \(\mathcal{C} : S \rightarrow \mathcal{P}(\mathbb {N})\) satisfying the following properties:

for each \(extr_l^u(s, t)\) literal, it is the case that:

\(\{l, u+1\} \subseteq \mathcal {C}(s)\), and

\(\{ i  l \mid i \in \mathcal {C}(s) \text {~with~} l \le i \le u+1 \} = \{ i \in \mathcal {C}(t) \mid i \le u  l +1\}\).


for each equality \(s = t\) it is the case that \(\mathcal {C}(s) = \mathcal {C}(t)\).
The set of cut points for all bitvectors can be obtained by a fixpoint computation, which begins with all cut points from extractions, and then propagates using the equalities until all conditions hold.
Example 9
Translated to our extended core language, the constraints from Example 8 are:
The extraction literals induce immediate cut points for x, y and z, respectively: \(\{6, 0\}, \{8, 2\}\), and \(\{6, 2\}\). Since x and z are related by the literal \(extr_0^5(x,z)\), the cut point 2 needs to be added to the set for x as well; similarly, due to the equation \(x = y\), also the cut points \(\{6, 0\}\) have to be added for y, and 8 for x. The alignment of the bitvectors is illustrated in Fig. 8, and the complete sets of cut points after propagation are \(\{8, 6, 2, 0\}\), \(\{8, 6, 2, 0\}\), and \(\{6, 2, 0\}\). If the bitvectors x, y, z are decomposed according to their cut points, then simple reasoning reveals the inconsistency between \(extr_2^5(x,5)\), \(extr_2^5(y, 6)\), and \(x = y\).
An interpolating calculus for extractions
A decomposition according to the cut points yields a complete and polynomial procedure for the structural fragment [19]. We formalise the splitting of bitvector extractions with an interpolating calculus rule extrsplit in Fig. 9. Intuitively, we cut the bitvector s at point i and introduce two existential variables \(x_1, x_2\) corresponding to the two slices. By constraining the corresponding slices of r according to the decomposition, we ensure the original equality between the extraction of s and r. The rule can be generalised to split into several slices at once, allowing for shorter proofs.
After extracts have been split at the cut points, we rely on congruence closure to take care of \(extr_l^u\) literals, in a similar way as the procedure in [18]. Congruence closure is in our setting expressed by an axiom schema for functional consistency of the \(extr_l^u\) predicates:
The axiom states that two extrliterals will yield the same result if the first arguments coincide, and if the same bits are extracted. Similar axioms for predicate consistency and functional consistency are used in [4]. To simplify presentation, we model the instantiation of (2) using the calculus rule extrcc in Fig. 9; the figure also gives four interpolating versions of the rule, for the four possible combinations of L/Rlabels. The LR/RL rules differ in the label used in their premises. The rules can be derived by instantiating (2) using either \(\forall \) left\(_L\) or \(\forall \) left\(_R\), in a similar way as in Sect. 3.3. In practice, and in our implementation, the calculus rules are used as in classical SMTstyle congruence closure: they are triggered when the first arguments of a pair of extrliterals have become equal.
Extraction operations can also be translated to arithmetic, which is needed to evaluate extraction from concrete numbers, and when constructing proofs for formulas that are not in the structural fragment (i.e., that combine extraction with other bitvector operations). The rule extrarith encodes an operation \(extr_l^u(s, r)\) using a modulo constraint to eliminate bits above position u, and division to strip away bits below position l. We express the division by existentially quantifying the remainder. A more direct rule to perform evaluation is introduced in Sect. 5.4.
Example 10
We continue Example 9, and show how an interpolating proof can be constructed for the conjunction \(A'_{\text {core}} \wedge B'_{\text {core}}\). The root sequent of the proof is \({\lfloor A'_{\text {core}}\rfloor _L, \lfloor B'_{\text {core}}\rfloor _R}\;\vdash \;{\emptyset }\). In the proof tree shown in Fig. 10, we first split the given formulas using Boolean rules. Then, the literal \(extr_0^5(x, z)\) can be decomposed using our extrsplit rule at the cut point 2, and congruence closure is applied to the literals \(extr_2^5(z, c_1)\) and \(extr_2^5(z, 11)\). We similarly decompose the literal \(extr_2^7(y, 6)\) at cut point 6, and then use extrarith to reduce \(extr_0^3(6, c_2)\) to \(c_2 = 6\). Finally, we need a second application of congruence closure, \({\textsc {extrcc}}_{LR}\), to relate the extractions from x and y.
The resulting interpolant is the formula \(\exists c . (extr_2^5(x,c) \wedge c = 11)\). The quantifier in the formula stems from the application of \({\textsc {extrcc}}_{LR}\), which transfers the local symbol \(c_1\) from L to R, and thus makes it shared. A quantifier is needed to eliminate the symbol again from the interpolant. However, as can be seen the quantifier naturally disappears when translating the interpolant back to functional notation, which yields the formula \(\textsf {bvextract}_{[5, 2]}(x) = 11\) in the structural fragment.
It is quite easy to see that our calculus is sound and complete for formulas in the structural fragment. The calculus does not guarantee, however, that interpolants computed for formulas in the structural fragment are again in the structural fragment, or that interpolants are quantifierfree. This leads to the question whether the structural fragment is actually closed under interpolation, i.e., whether every unsatisfiability conjunction has an interpolant that is again in the fragment. The answer to this question is positive, and it turns out that our calculus can also be used to compute such interpolants, if the right strategy is used to construct proofs.
Theorem 1
The structural fragment is closed under interpolation.
Proof
We give a simple proof that follows from the fact that our calculus can model bitblasting of bitvector formulas, and builds on work on EUF interpolation in [3, 4]. The existence of more compact interpolants, avoiding the need to blast to individual bits, can also be shown, but this is slightly more involved.
Suppose \(A \wedge B\) is an unsatisfiable conjunction in the structural fragment, and \(A_{\text {core}} \wedge B_{\text {core}}\) the translation to the (extended) core language. Further assume that \(x_1, \ldots , x_m\) are the shared bitvector constants of A, B, and that \(w_1, \ldots , w_m\) are their bitwidths, respectively. This means that we are searching for an interpolant in the structural fragment that may only contain the constants \(x_1, \ldots , x_m\). To model bitblasting, we augment \(A_{\text {core}}, B_{\text {core}}\) by adding fresh names \(\{b_i^j,c_i^j\}_{i, j}\) for the individual bits of \(x_1, \ldots , x_m\):
This means that \(b_i^j/c_i^j\) is the name of the jth bit of \(x_i\) in the L/R partition. Note that a formula \(I_{\text {core}}\) is an interpolant of \(A_{\text {core}} \wedge B_{\text {core}}\) iff it is an interpolant of \(A'_{\text {core}} \wedge B'_{\text {core}}\), because no shared symbols are added, and we can therefore work with the latter conjunction.
Without loss of generality, we further assume that even every local constant in \(A'_{\text {core}}\) and \(B'_{\text {core}}\) occurs as first argument of some \(extr_l^u\)literal, and that every bit in such constants is extracted by some of the literals. This assumption can be ensured by adding further literals to the formulas, without changing the set of possible interpolants.
We then construct a proof for the root sequent \({\lfloor A'_{\text {core}}\rfloor _L, \lfloor B'_{\text {core}}\rfloor _R}\;\vdash \;{\emptyset }\) in our interpolating calculus by systematically applying the calculus rules. Rules are applied likewise to the L and the Rformulas, so that we only mention the Lversions at this point for sake of brevity:

\(\wedge {\textsc {left}}_L\) to split conjunctions, and \(\exists {\textsc {left}}_L\) to eliminate quantifiers;

\({\textsc {extrsplit}}_L\) to split every occurring extr predicate down to the level of individual bits;

\({\textsc {extrcc}}_{LL}\) whenever two extracts \(\lfloor extr_j^j(s, r)\rfloor _L, \lfloor extr_j^j(s, r')\rfloor _L\) for the same bit occur, followed by arithmetic rules to close the left premise; this generates an equation \(\lfloor r = r'\rfloor _L\);

\({\textsc {extrcc}}_{LL}\) whenever two extracts \(\lfloor extr_j^j(s, r)\rfloor _L, \lfloor extr_j^j(t, r')\rfloor _L\) in combination with an equation \(\lfloor s = t\rfloor _L\) occur, followed by an application of \({\textsc {close}}_{LL}\) to close the left premise; again, this generates an equation \(\lfloor r = r'\rfloor _L\);

\({\textsc {extrarith}}_L\) whenever an extract \(\lfloor extr_j^j(\alpha , r)\rfloor _L\) from a concrete number \(\alpha \in \mathbb {Z}\) occurs, followed by arithmetic rules to simplify the generated formula to an equation \(\lfloor r = 0\rfloor _L\) or \(\lfloor r = 1\rfloor _L\);

\({\textsc {extrarith}}_L\) whenever an extract \(\lfloor extr_0^0(s, r)\rfloor _L\) in combination with the domain constraint \( in _{1}(s)\) occurs, i.e., when the single bit of a bitvector of width 1 is extracted, followed by arithmetic rules to simplify the generated formula to an equation \(\lfloor r = s\rfloor _L\).
After those rule applications, we can focus on the obtained bitlevel equations in the proof goal: on equations \(\lfloor s = t\rfloor _{D}\) or \(\lfloor s = \alpha \rfloor _{D}\) in which s, t have width 1 (i.e., \( in _{1}(s)\) and \( in _{1}(t)\)) and \(\alpha \in \{0, 1\}\), with \(D \in \{L, R\}\). By construction, the set of Llabelled bitlevel equations is equisatisfiable to the original formula \(A'_{\text {core}}\), and the Rlabelled equations are equisatisfiable to \(B'_{\text {core}}\), so that we can continue constructing a bitlevel proof using the equations.
Since the conjunction \(A'_{\text {core}} \wedge B'_{\text {core}}\) is by assumption unsatisfiable, there are three possible cases:
(i) the equations labelled with L are by themselves unsatisfiable, the interpolant is \( false \), and the proof can be closed by applying arithmetic rules;
(ii) symmetrically, the equations labelled with R are unsatisfiable, and the interpolant is \( true \); or
(iii) the equations are unsatisfiable only in combination.
In case (iii), there has to be a chain of equations, alternating between L and Requations, that witnesses unsatisfiability. There are several symmetric cases, of which we only consider one:
In the other cases, the chain can start in R and end in L, or start and end in the same partition. The dotted equations \(b_{i}^{j} \doteq c_{i}^{j}\) are implied by the literal \(\lfloor extr_{j}^{j}(x_{i}, b_{i}^{j})\rfloor _L\), \(\lfloor extr_{j}^{j}(x_{i}, c_{i}^{j})\rfloor _R\), but do not exist explicitly in the proof goal.
From (3), it is easy to read off an interpolant for \(A \wedge B\) in the structural fragment by summarising the Lchains:
Clearly, I follows from A, and \(I \wedge B\) is unsatisfiable due to (3).
To construct an interpolant mechanically in our calculus, there are several strategies. The simplest one is to apply the interpolating cutrule \({\textsc {cut}}_{RL}\) to each the formulas \(extr_{j_1}^{j_1}(x_{i_1}, 0)\) and \(\{\, \exists z.\, (extr_{j_l}^{j_l}(x_{i_l}, z) \wedge extr_{j_{l+1}}^{j_{l+1}}(x_{i_{l+1}}, z)) \,\}_{l=2}^{k1}\), which yields an interpolant \(I_{\text {core}}\) in the core language that corresponds to the structural interpolant I shown above. \(\square \)
A rewriting rule for constant extraction
Given an extraction \(extr_l^u(s, r)\) and bounds on s, it is in some cases possible to determine value of extracted bits. For example, the longest prefix on which the lower and upper bound agree is guaranteed to be present in any consistent value of s. Therefore, extractions that overlap with that prefix yield some bit values of the extraction without knowing the exact value of s. We allow rewriting if the extraction operator falls entirely within the common prefix:
where \( rem \) and \( div \) are the integer remainder and division, respectively. The rule extrconst allows in particular evaluation of extractions from constant bitvectors.
Splitting of disequalities
As shown above, proofs can be closed by finding contradicting assignments to (a slice of) a bitvector. In general, formulas can also contain bitvector disequalities, i.e., negative equalities between bitvectors. As an optimisation, disequalities can be split using the notion of cut points as well. Given a formula with a disequality \(s \ne t\), we extend the notion of cut point configurations (Sect. 5.2) by also propagating between s and t. For a cut point \(i \in \mathcal {C}(s) = \mathcal {C}(t)\), we can then replace the disequality with a disjunction of two disequalities, as expressed by the following rule:
The constants c, d must be fresh and not occur in the conclusion in this rule.
Experiments
To evaluate the effectiveness of the approach, the procedures described in this article have been implemented in the Princess theorem prover^{Footnote 6} [25]. The implementation of the full SMTLIB theory of bitvectors in Princess is still an ongoing effort, and at this point includes fairly refined versions of the calculi for nonlinear arithmetic (Sect. 3) and for arithmetic bitvector operators (Sect. 4). The implementation of the calculus for the structural fragment (Sect. 5) has been added more recently, and still lacks many optimisations that could be applied. Support for bitwise operations (like bvand) is also quite naïve at the moment, and simply bitblasts each bitwise operation separately by introducing \(\textsf {bvextract}_{[i, i]}\) terms for the individual bits, as shown in Fig. 7. A more refined encoding would choose, for each subexpression, whether the arithmetic encoding or bitblasting should be applied, but this refinement is left for future work. The implementation also supports the SMTLIB shift operators, which are handled by splitting over the possible values of the second argument. The SMTLIB rotation operators are not supported yet; those operators are overapproximated as uninterpreted functions, which means that it might be possible to prove problems involving the operators unsatisfiable, but not satisfiable.
All experiments were done on an AMD Opteron 2220 SE machine, running 64bit Linux and Java 1.8. Runtime was limited to 10min wall clock time, and heap space to 2GB. We used Princess version 20191002 for all experiments. Where runtimes are reported, we use wall clock time.
We evaluate the performance of our approach in three different ways:

Sect. 6.1: performance of satisfiability queries on quantifierfree bitvector formulas (SMTLIB QF_BV), in comparison to the stateoftheart solvers Z3 4.8.0 [37] and CVC4 1.6 [38].

Section 6.2: performance of satisfiability queries on bitvector formulas with quantifiers (SMTLIB BV), again with comparison to Z3 and CVC4.

Section 6.3: applicability of the interpolation procedure for software model checking, using the integration in the Horn solver Eldarica. We compare to the software model checker CPAchecker 1.7 [39], which internally uses MathSAT 5 [20] and the interpolation method from [16].
Satisfiability queries on quantifierfree formulas
While our procedure is not specifically designed for just checking satisfiability of formulas, it is nevertheless interesting to evaluate how the approach performs on problems from the QF_BV category of the SMTLIB. Results for this category are given in Table 1, and show that our implementation can overall solve a decent number of benchmarks, but is not competitive with Z3 and CVC4 on most of the benchmark families. As a general trend, and unsurprisingly, it can be observed that our lazy arithmetic encoding works relatively well for problems that use arithmetic bitvector operators, but does not pay off for problems that are mostly Boolean, or problems involving bitwise operators.
Our implementation can solve the “challenge/multiplyOverflow.smt2” problem discussed in Example 3, and it performs particularly well on the “brummayerbiere4” and “pspace” families, which contain benchmarks with large bitwidths, with variables with up to \(30\,000\) bits. This is to be expected, since our arithmetic encoding is essentially agnostic about the bounds of bitvector variables, so that the complexity of a problem hardly changes when adding more bits.
The family “bruttomesso/core” consists of SMTLIB problems in the structural fragment from Sect. 5 (with additional Boolean structure). Compared to the implementation described in the FMCAD 2018 paper [17], the performance on those problems has improved significantly as a result of adding the procedure described in Sect. 5. In 2018, only 8 benchmarks from the “core” family could be solved, compared to 142 in the new version. This is still lower than the results for Z3 and CVC4, which is likely due to more efficient Boolean reasoning.
We also investigated how often the rules \(\times \) split, bmodsplit, and bmodconst for splitting and eliminating predicates were applied on the benchmarks. We first determined how many of the problems required the application of the rules at all:
Total solved  bmodsplit  bmodconst  \(\times \) split  

SAT  7331  2699  268  334 
UNSAT  15,148  647  130  44 
The statistics show that a large number of the benchmarks can indeed be solved without those rules. This is in particular the case for unsatisfiable problems, for which it is apparently largely sufficient to work with the simplification rules from Fig. 4, in combination with the rules for Presburger arithmetic, (nonsplitting) multiplication, and extraction. In Fig. 11 we compare the required number of applications of bmodsplit and bmodconst for the individual benchmarks; the scatter plot shows that often a small number of rule applications is sufficient.
The runtimes reported in Table 1 for Princess are somewhat higher than those of Z3 and CVC4, which can partly be explained by the fact that Princess is entirely implemented in Scala, and runs on a JVM. This results in repeated overhead for starting up the JVM and for justintime compilation. In actual applications, for instance software model checking as discussed in Sect. 6.3, normally many queries are handled without restarts in between, and the amortised overhead is smaller.
Satisfiability queries on formulas with quantifiers
We evaluate the effectiveness of our quantifier elimination approach on problems from the BV category of SMTLIB. In order to check whether a quantified bitvector formula is satisfiable, QE often does not have to be run to completion, instead the elimination approach from Sect. 2.2 can be stopped as soon as a statement about satisfiability of the resulting formula can be made. This incremental approach to solving quantified formulas has been implemented in Princess for Presburger arithmetic, and in combination with our lazy encoding for bitvectors also directly applies to quantified bitvector formulas.
Results on the SMTLIB BV benchmarks are given in Table 2. Our procedure can solve a similar number of problems as Z3 and CVC4 on many of the BV families, although the total number of problems solved is still lower than for Z3 and CVC4. Like for QF_BV, the results confirm that the encoding of bitvectors into arithmetic is more effective for problems that are arithmetic in nature (e.g., the families “Automizer,” “model,” and “Heizmann”), than for more combinatorial problems (e.g., “psyco”). In general, quantified bitvector problems tend to be smaller and harder than quantifierfree problems, which leads to a situation where it is essential to have the right heuristics and optimisations in place; in this respect our implementation is clearly still lagging behind Z3 and CVC4.
In the experiments, we used a simple portfolio mode enabled by the option portfolio=bv. This mode is inspired by the observation that a closed bitvector formula \(\phi \) (i.e., a formula without free variables or uninterpreted predicates) can be shown to be satisfiable also be proving that the negation \(\lnot \phi \) is unsatisfiable, and vice versa. Experiments showed that often one of \(\phi \) or \(\lnot \phi \) is significantly simpler to solve than the other, but that it is difficult to predict the easier one; in the portfolio mode the prover therefore simultaneously tries to solve \(\phi \) and \(\lnot \phi \).
Interpolation and verification of C programs
The main purpose of our procedure is the computation of Craig interpolants for bitvector formulas. Unfortunately, comparing and evaluating interpolation procedures is relatively tricky, since the properties that can be measured easily (e.g., the size, shape, or strength of interpolants, or the time required to extract interpolants) are ultimately only of limited importance in applications. The decisive property that makes interpolants useful is the ability to generalise, which is hard to measure syntactically. Adding to this, there is no standard set of interpolation benchmarks that could be used, and the interpolation queries that occur in model checking can differ from run to run. In model checking, moreover interpolation queries are interdependent: the results of earlier queries in a run will affect the later interpolation queries being generated.
We therefore decided to evaluate in an applicationoriented way, by integrating our interpolation procedure into a model checker and measuring its ability to verify safety properties of C programs with machine integer semantics. As model checker we use Eldarica version 2.0.2^{Footnote 7} [40], a Horn clausebased model checker that uses Cartesian predicate abstraction and the CEGAR algorithm. Eldarica was already previously tightly integrated with Princess, and was in the scope of this work extended to also handle Horn clauses over bitvectors. Since Eldarica internally uses the Princess datastructures to store Horn clauses, we could implement the translation from bitvectors to our core language (Sect. 4.1) as a preprocessing step that is applied to all Horn clauses upfront. This means that the actual model checking engine operates purely on expressions in the core language, and all interpolation queries and implication checks stay within the core language; the need to translate back and forth between bitvector formulas and core language is eliminated. As an obvious downside of this approach, however, it is no longer easily possible to replace the interpolation procedure with other solvers.
Benchmarks. For the experiments, we used the builtin C parser of Eldarica, and work with the benchmark set of 551 C programs already used in [41] for evaluating different predicate generation strategies. The programs stem from a variety of sources, including the SVCOMP 2016 categories “Integers and Control Flow” and “Loops,” and were selecting by taking all programs that do not include arrays or heap data structures (i.e., only arithmetic operations). The verification task consisted in showing that safety assertions included in the programs can never fail. For the experiment, we interpret the programs as operating either on the unbounded mathematical integers (math, Eldarica option arithMode:math), or on signed 32bit bitvectors (ilp32, Eldarica option arithMode:ilp32) with wraparound semantics. Eldarica was otherwise run with default settings, which means that it also applies the interpolation abstraction technique from [42].
Comparison math versus ilp32. The results for math and ilp32 semantics are given in Table 3 and Fig. 12. It has to be pointed out that the status of the programs depends on the chosen semantics: for instance, the 46 HOLA programs [43] are all known to be safe in mathematical semantics, but several of the programs turn out to be unsafe in bitvector semantics due to the possibility of overflow. Eldarica can consistently verify safety of more programs in math than in ilp32, but it can disprove safety in more of the ilp32 cases. The total number of solved cases is higher in math than in ilp32, but ilp32 is quite close (403 vs. 337); given the higher complexity of the bitvector semantics, this is an encouraging result. The scatter plot in Fig. 12 shows that the runtimes for the two semantics are strongly correlated, and while ilp32 is on average slower than math the difference is relatively small.
Table 3 also shows that the number of CEGAR iterations is comparable for math and ilp32, while the size of interpolants (measured as the average number of subformulas of interpolants) is bigger for ilp32 than for math, but usually by less than a factor of 2. The exception is the category “llreve/unsafe,” where drastically bigger interpolants are computed for ilp32 than for math. Inspecting this case, we found that there was a single benchmark in “llreve” that was solved after 579 seconds with interpolants of size 2133; when removing this outlier, the average interpolant size for “llreve/unsafe” is only 1.1.
Comparison with CPAchecker. As comparison, we also ran the model checker CPAchecker 1.7 [39], using options predicateAnalysis 32 and MathSAT 5 [20] as solver. MathSAT 5 uses the interpolation method from [16]. The results are given in Table 4 and Fig. 13. Our method is competitive with CPAchecker on all considered categories: Eldarica with ilp32 can consistently prove more programs safe, whereas CPAchecker can show more programs unsafe, with a lower number of CEGAR iterations. We suspect that the use of largeblock encoding [44] in CPAchecker is responsible for this phenomenon, and indeed makes CPAchecker very effective for bug finding. The runtimes of the systems are on average close, but the scatter plot in Fig. 13 shows no clear trend.
Altogether, we remark that we are comparing different verification systems here: although both Eldarica and CPAchecker apply CEGAR and interpolation, there are many factors affecting the results. What the experiments do show, however, is that the interpolation method proposed in this paper can be used to create a software model checker that is competitive with the state of the art.
Conclusions
We have presented a new calculus for Craig interpolation and quantifier elimination in bitvector arithmetic. Furthermore, we have shown how to efficiently integrate reasoning over the structural fragment. While the experimental results in model checking are already promising, we believe that there is still a lot of room for extension and improvement of the approach. This includes more powerful propagation and simplification rules, and more sophisticated strategies to apply the splitting rules \(\times \) split and bmodsplit. Future work also includes more efficient use of bounds, and a strategy to employ bitblasting directly to whole subexpressions when deemed more efficient.
Notes
The set of all linear equations implied by a set of \(\times \)literals over integers is clearly not computable, by reduction of Hilbert’s 10th problem.
Nonlinear integer arithmetic in general does not admit quantifierfree interpolants. For instance, \((x >1 \wedge x = y^2) \wedge x = z^2 + 1\) is unsatisfiable, but no quantifierfree interpolants exist, regardless of whether divisibility predicates \(\alpha \mid t\) are allowed or not.
References
McMillan KL (2005) An interpolating theorem prover. Theor Comput Sci 345(1):101–121
D’Silva V, Purandare M, Weissenbacher G, Kroening D (2010) Interpolant strength. In: VMCAI, LNCS. Springer
Fuchs A, Goel A, Grundy J, Krstić S, Tinelli C (2009) Ground interpolation for the theory of equality. In: TACAS, LNCS. Springer
Brillout A, Kroening D, Rümmer P, Wahl T (2011) Beyond quantifierfree interpolation in extensions of Presburger arithmetic. In: VMCAI, LNCS. Springer, pp 88–102
McMillan KL (2008) Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan CR, Rehof J (eds) Tools and algorithms for the construction and analysis of systems, TACAS 2008, vol 4963 of Lecture Notes in Computer Science. Springer, pp 413–427
Kovács L, Voronkov A (2009) Interpolation and symbol elimination. In: CADE, pp 199–213
Bonacina MP, Johansson M (2015) On interpolation in automated theorem proving. J. Autom. Reason. 54(1):69–97. https://doi.org/10.1007/s1081701493140
Kapur D, Majumdar R, Zarba CG (2006) Interpolation for data structures. In: SIGSOFT’06/FSE14, ACM, New York, NY, USA, pp 105–116. https://doi.org/10.1145/1181775.1181789
Hojjat H, Rümmer P (2017) Deciding and interpolating algebraic data types by reduction. In: Jebelean T, Negru V, Petcu D, Zaharie D, Ida T, Watt SM (eds) 19th international symposium on symbolic and numeric algorithms for scientific computing, SYNASC 2017, Timisoara, Romania, September 21–24, IEEE Computer Society, 2017, pp 145–152. https://doi.org/10.1109/SYNASC.2017.00033
Dai L, Xia B, Zhan N (2013) Generating nonlinear interpolants by semidefinite programming. In: Sharygina N, Veith H (eds) Computer aided verification—25th international conference, CAV 2013, Saint Petersburg, Russia, July 13–19, 2013. Proceedings, vol 8044 of Lecture Notes in Computer Science. Springer, pp 364–380. https://doi.org/10.1007/9783642397998_25
Brillout A, Kroening D, Rümmer P, Wahl T (2011) An interpolating sequent calculus for quantifierfree Presburger arithmetic. J Autom Reason 47:341–367
Griggio A, Le TTH, Sebastiani R (2010) Efficient interpolant generation in satisfiability modulo linear integer arithmetic. Log Methods Comput Sci. https://doi.org/10.2168/LMCS8(3:3)2012
Bruttomesso R, Ghilardi S, Ranise S (2012) Quantifierfree interpolation of a theory of arrays. Log Methods Comput Sci. https://doi.org/10.2168/LMCS8(2:4)2012
Totla N, Wies T (2016) Complete instantiationbased interpolation. J. Autom Reason 57(1):37–65. https://doi.org/10.1007/s1081701693717
Hoenicke J, Schindler T (2018) Efficient interpolation for the theory of arrays. CoRR abs/1804.07173. arXiv:1804.07173
Griggio A (2011) Effective wordlevel interpolation for software verification. In: Bjesse P, Slobodová A (eds) International conference on formal methods in computeraided design. FMCAD ’11, Austin, TX, USA, October 30–November 02, 2011, FMCAD Inc., pp 28–36
Backeman P, Rümmer P, Zeljic A Bitvector interpolation and quantifier elimination by lazy reduction. In: Bjørner and Gurfinkel, vol 45, pp. 1–10. https://doi.org/10.23919/FMCAD.2018.8603023
Cyrluk D, Möller O, Rueß H (1997) An efficient decision procedure for the theory of fixedsized bitvectors. In: Grumberg O (ed) Computer aided verification. Springer, Berlin, pp 60–71
Bruttomesso R, Sharygina N (2009) A scalable decision procedure for fixedwidth bitvectors. In: Proceedings of the 2009 international conference on computeraided design, ICCAD ’09, ACM, New York, pp 13–20. https://doi.org/10.1145/1687399.1687403
Cimatti A, Griggio A, Schaafsma BJ, Sebastiani R (2013) The MathSAT5 SMT solver. In: TACAS, vol 7795 of LNCS
Asadi S, Blicha M, Fedyukovich G, Hyvärinen AEJ, EvenMendoza K, Sharygina N, Chockler H (2018) Function summarization modulo theories. In: Barthe G, Sutcliffe G, Veanes M (eds) LPAR22. 22nd international conference on logic for programming, artificial intelligence and reasoning, Awassa, Ethiopia, 1621 November 2018, vol 57 of EPiC Series in Computing, EasyChair, pp 56–75
Kroening D, Weissenbacher G (2007) Lifting propositional interpolants to the wordlevel. In: FMCAD, IEEE Computer Society, pp 85–89
Kroening D, Weissenbacher G (2009) An interpolating decision procedure for transitive relations with uninterpreted functions. In: Haifa verification conference, vol 6405 of Lecture Notes in Computer Science. Springer, pp 150–168
Ho Y, Chauhan P, Roy P, Mishchenko A, Brayton RK (2016) Efficient uninterpreted function abstraction and refinement for wordlevel model checking. In: Piskac R, Talupur M (eds), 2016 formal methods in computeraided design, FMCAD 2016, Mountain View, CA, USA, October 3–6, IEEE, 2016, pp 65–72. https://doi.org/10.1109/FMCAD.2016.7886662
Rümmer P (2008) A constraint sequent calculus for firstorder logic with linear integer arithmetic. In: LPAR, vol 5330 of LNCS. Springer, pp 274–289
Fitting MC (1996) Firstorder logic and automated theorem proving, 2nd edn. Springer, New York
Halpern JY (1991) Presburger arithmetic with unary predicates is \(\Pi _1^1\) complete. J Symbol Log 56:637–642
Nieuwenhuis R, Oliveras A, Tinelli C (2006) Solving SAT and SAT modulo theories: from an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). J ACM 53(6):937–977
Reynolds A, King T, Kuncak V (2017) Solving quantified linear arithmetic by counterexampleguided instantiation. Formal Methods Syst Des 51(3):500–532
Craig W (1957) Linear reasoning: a new form of the Herbrand–Gentzen theorem. J Symbol Log 22(3):250–268
Lang SS (1993) Algebra, 3rd edn. AddisonWesley, Reading
Buchberger B (3, 2006) An algorithm for finding the basis elements in the residue class ring modulo a zero dimensional polynomial ideal, Ph.D. thesis
Van Hentenryck P, McAllester D, Kapur D (1997) Solving polynomial systems using a branch and prune approach. SIAM J Numer Anal 34(2):797–827
Warren J, Hunt A, Krug RB, Moore JS (2003) Linear and nonlinear arithmetic in ACL2. In: Proceedings, correct hardware design and verification methods, 12th IFIP WG 10.5 advanced research working conference, vol 2860 of LNCS. Springer, pp 319–333
Borralleras C, Lucas S, Oliveras A, RodríguezCarbonell E, Rubio A (2012) SAT modulo linear arithmetic for solving polynomial constraints. J. Autom Reason 48(1):107–131
Barrett C, Fontaine P, Tinelli C (2017) The SMTLIB Standard: Version 2.6, Technical report, Department of Computer Science, The University of Iowa. www.SMTLIB.org
de Moura LM, Bjørner N (2008) Z3: an efficient SMT solver. In: TACAS, vol 4963 of LNCS. Springer, pp 337–340
Barrett C, Conway CL, Deters M, Hadarean L, Jovanovic D, King T, Reynolds A, Tinelli C (2011) CVC4. In: CAV, vol 6806 of LNCS. Springer, pp 171–177. https://doi.org/10.1007/9783642221101_14
Beyer D, Keremoglu ME (2009) CPAchecker: a tool for configurable software verification. CoRR abs/0902.0019. arXiv:0902.0019
Hojjat H, Rümmer P The ELDARICA Horn solver. In: Bjørner and Gurfinkel, vol 45, pp 1–7. https://doi.org/10.23919/FMCAD.2018.8603013
Demyanova Y, Rümmer P, Zuleger F (2017) Systematic predicate abstraction using variable roles. In: Barrett C, Davies M, Kahsai T (eds) NASA formal methods—9th international symposium, NFM 2017, Moffett Field, CA, USA, May 16–18, 2017, Proceedings, vol 10227 of Lecture Notes in Computer Science, pp 265–281. https://doi.org/10.1007/9783319572888_18
Leroux J, Rümmer P, Subotic P (2016) Guiding Craig interpolation with domainspecific abstractions. Acta Inf 53(4):387–424. https://doi.org/10.1007/s002360150236z
Dillig I, Dillig T, Li B, McMillan KL (2013) Inductive invariant generation via abductive inference. In: Hosking AL, Eugster PT, Lopes CV (eds), Proceedings of the 2013 ACM SIGPLAN international conference on object oriented programming systems languages & applications, OOPSLA. ACM, pp 443–456. https://doi.org/10.1145/2509136.2509511
Beyer D, Cimatti A, Griggio A, Keremoglu ME, Sebastiani R (2009) Software model checking via largeblock encoding. In: Proceedings of 9th international conference on formal methods in computeraided design, FMCAD 2009, 15–18 November 2009, Austin, Texas, USA. IEEE, pp 25–32. https://doi.org/10.1109/FMCAD.2009.5351147
Acknowledgements
This research has been supported by the Swedish Research Council (VR) under the Grants 20145484 and 201804727, by the Swedish Foundation for Strategic Research (SSF) under the project WebSec (Ref. RIT170011), and by a grant from Microsoft. We also wish to thank the reviewers for their extensive and helpful feedback.
Funding
Open access funding provided by Mälardalen University.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
About this article
Cite this article
Backeman, P., Rümmer, P. & Zeljić, A. Interpolating bitvector formulas using uninterpreted predicates and Presburger arithmetic. Form Methods Syst Des 57, 121–156 (2021). https://doi.org/10.1007/s10703021003726
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703021003726
Keywords
 Bitvectors
 Interpolation
 Quantifier elimination
 Presburger arithmetic