Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors

Advances in solving formula satisfiability modulo theories (smt) achieved during the last few decades enabled significant progress and practical applications in the area of automated analysis, testing, and verification of various systems. In the case of software and hardware systems, the most relevant theory is the theory of fixed-sized bit-vectors, as these systems work with inputs expressed as bit-vectors (i.e., sequences of bits) and perform bitwise and arithmetic operations on bit-vectors. The quantifier-free fragment of this theory is supported by many general-purpose smt solvers, such as CVC4 [1], MathSAT [7], Yices [10], or Z3 [9] and also by several dedicated solvers, such as Boolector [21] or STP [12]. However, there are some use-cases where quantifier-free formulas are not natural or expressive enough. For example, formulas containing quantifiers arise naturally when expressing loop invariants, ranking functions, loop summaries, or when checking equivalence of two symbolically described sets of states [8, 13, 17, 18, 24]. In the following, we focus on smt solvers for quantified bit-vector formulas. In particular, this paper describes the state-of-the-art smt solver Q3B including its implementation and the inner workings.

Solving of quantified bit-vector formulas was first supported by Z3 in 2013 [25] and for a limited set of exists/forall formulas with only a single quantifier alternation by Yices in 2015 [11]. Both of these solvers decide quantified formulas by quantifier instantiation, in which universally quantified variables in the Skolemized formula are repeatedly instantiated by ground terms until the resulting quantifier-free formula is unsatisfiable or a model of the original formula is found. In 2016, we proposed a different approach for solving quantified bit-vector formulas: by using binary decision diagrams (bdds) and approximations [14]. For evaluation of this approach, we implemented an experimental smt solver called Q3B, which outperformed both Z3 and Yices. Next solver that was able to solve quantified bit-vector formulas was Boolector in 2017, using also an approach based on quantifier instantiation [22]. Unlike Z3, in which the universally quantified variables are instantiated only by constants or subterms of the original formula, Boolector uses a counterexample-guided synthesis approach, in which a suitable ground term for instantiation is synthesized based on the defined grammar. Thanks to this, Boolector was able to outperform Q3B and Z3 on certain classes of formulas. More recently, in 2018, support of quantified bit-vector formulas has also been implemented into CVC4 [20]. The approach of CVC4 is also based on quantifier instantiation, but instead of synthesizing terms given by the grammar as Boolector, CVC4 uses predetermined rules based on invertibility conditions, which directly give terms that can prune many spurious models without using potentially expensive counterexample-guided synthesis. The authors of CVC4 have shown that this approach outperforms Z3, CVC4, and the original Q3B. However, Q3B has been substantially improved since the original experimental version. In 2017, we extended it with simplifications of quantified bit-vector formulas using unconstrained variables [15]. Further, in 2018, we added the experimental implementation of abstractions of bit-vector operations [16]. With these techniques, Q3B is able to decide more formulas than Z3, Boolector, and CVC4. Besides the theoretical improvements, Q3B was also improved in terms of stability, ease of use, technical parts of the implementation, and compliance with the smt-lib standard. This tool paper presents the result of these improvements: Q3B 1.0, the first stable version of Q3B.

We briefly summarize the smt solving approach of Q3B. As in most of modern smt solvers, the input formula is first simplified using satisfiability-preserving transformations that may reduce the size and complexity of the formula. The simplified formula is then converted to a binary decision diagram (bdd) that represents all assignments satisfying the formula, i.e., the models of the formula. If the bdd represents at least one model, we say that the bdd is satisfiable and it implies satisfiability of the formula. If the bdd represents the empty set of models, we say that it is unsatisfiable and so is the formula. Unfortunately, there are formulas for which the corresponding bdd (or some of the intermediate bdds that appear during its computation) is necessarily exponential in the number of bits in the formula. For example, this is the case for formulas that contain multiplication of two bit-vector variables [5]. To be able to deal with such formulas, Q3B computes in parallel also bdds underapproximating and overapproximating the original set of models, i.e., bdds representing subsets and supersets of the original set of models, respectively. The approximating bdds may be much smaller in size than the precise bdd, especially if the approximation is very rough. Still, they can be used to decide satisfiability of the original formula. If an overapproximating bdd is unsatisfiable, the original formula is also unsatisfiable. If the overapproximating bdd is satisfiable, we take one of its models, i.e., an assignment to the top-level existential variables of the formula, and check whether it is a model of the original formula. If the answer is positive, the original formula is satisfiable. In the other case, we build a more precise overapproximating bdd. Underapproximating bdds are utilized analogously. The only difference is that for unsatisfiable underapproximating bdd, we check the validity of a countermodel, i.e., an assignment to the top-level universal variables that makes the formula unsatisfiable. The approach is depicted in Fig. 1.

Q3B currently supports two ways of computing the approximating bdds from the input formula. First of these are variable bit-width approximations in which the effective bit-width of some variables is reduced. In other words, some of the variables are represented by fewer bits and the rest of the bits is set to zero bits, one bits, or the sign bit of the reduced variable. This approach was originally used by the smt solvers uclid [6] and Boolector [21]. Q3B extends this approach to quantified formulas: if bit-widths of only existentially quantified variables are reduced, the resulting bdd is underapproximating; if bit-widths of only universally quantified variables are reduced, the resulting bdd is overapproximating. The second way to obtain an approximation is bit-vector operation abstraction [16], during which the individual bit-vector operations may not compute all bits of the result, but produce some do-not-know bits if the resulting bdds would exceed a given number of nodes. An underapproximating bdd then represents assignments that satisfy the formula for all possible values of these do-not-know bits. Analogously, an overapproximating bdd represents all assignments that satisfy the formula for some value of the do-not-know bits. Q3B also supports a combination of these two methods, in which both the effective bit-with of variables is reduced and the limit on the size of bdds is imposed. During an approximation refinement, either the effective bit-width or the size limit is increased, based on the detected cause of the imprecision.

This section describes the internal architecture of Q3B. The overall structure including internal and external components and the interactions between them is depicted in Fig. 2. We explain the purpose of the internal components:

Q3B is implemented in C++17, is open-source and available under MIT license on GitHub: https://​github.​com/​martinjonas/​Q3B. The project development process includes continuous integration and automatic regression tests.

Q3B relies on several external libraries and tools. For representation and manipulation with bdds, Q3B uses the open-source library cudd 3.0 [23]. Since cudd does not support bit-vector operations, we use the library by Peter Navrátil [19] that implements bit-vector operations on top of cudd. The algorithms in this library are inspired by the ones in the bdd library BuDDy¹ and they provide a decent performance. Nevertheless, we have further improved its performance by several modifications. In particular, we added a specific code for handling expensive operations like bit-vector multiplication and division when arguments contain constant bdds. This for example considerably speeds up multiplication whenever one argument contains many constant zero bits, which is a frequent case when we use the variable bit-width approximation fixing some bits to zero. Further, we have fixed few incorrectly implemented bit-vector operations in the original library. Finally, we have extended the library with the support for do-not-know bits in inputs of the bit-vector operations and we have implemented abstract versions of arithmetic operations that can produce do-not-know bits when the result exceeds a given number of bdd nodes.

For parsing the input formulas in smt-lib format, Q3B uses antlr parser generated from the grammar² for smt-lib 2.6 [2]. We have modified the grammar to correctly handle bit-vector numerals and to support push and pop commands without numerical argument. The parser allows Q3B to support all bit-vector operations and almost all smt-lib commands except get-assertions, get-assignment, get-proof, get-unsat-assumptions, get-unsat-core, and all the commands that work with algebraic data-types. This is in sharp contrast with the previous experimental versions of Q3B, which only collected all the assertions from the input file and performed the satisfiability check regardless of the rest of the commands and of the presence of the check-sat command. The reason for this was that the older versions parsed the input file using the Z3 C++ api, which can provide only the list of assertions, not the rest of the smt-lib script. Thanks to the new parser, Q3B 1.0 can also provide the user with a model of a satisfiable formula after calling get-model; this important aspect of other smt solvers was completely missing in the previous versions.

On the other hand, C++ api of the solver Z3 is still used for internal representation of parsed formulas. The Z3 C++ api is also used to perform manipulations with formulas, such as substitution of values for variables, and some of the formula simplifications. Note that these are the only uses of Z3 api in Q3B during solving the formula; no actual smt- or sat-solving capabilities of Z3 are used during the solving process.

Some classes of Q3B, in particular Solver, FormulaSimplifier, and UnconstrainedVariableSimplifier, expose a public C++ api that can be used by external tools for smt solving or just performing formula simplifications. For example, Solver exposes method Solve(formula, approximationType), which can be used to decide satisfiability by the precise solver, the underapproximating solver, or the overapproximating solver. Solver also exposes the method SolveParallel(formula), which simplifies the input formula and runs all three of these solvers in parallel and returns the first result as depicted in Fig. 1.

We have evaluated the performance of QB3 1.0 and compared it to the latest versions of smt solvers Boolector (v3.0), CVC4 (v1.6), and Z3 (v4.8.4). All tools were used with their default settings except for CVC4, where we used the same settings as in the paper that introduces quantified bit-vector solving in CVC4 [20], since they give better results than the default CVC4 settings. As the benchmark set, we have used all 5751 quantified bit-vector formulas from the smt-lib repository. The benchmarks are divided into 8 distinct families of formulas. We have executed each solver on each benchmark with cpu time limit 20 min and ram limit of 8 GiB. All the experiments were performed in a Ubuntu 16.04 virtual machine within a computer equipped with Intel(R) Core(TM) i7-8700 CPU @ 3.20 GHz cpu and 32 GiB of ram. For reliable benchmarking we employed BenchExec [4], a tool that allocates specified resources for a program execution and precisely measures their usage. All scripts used for running benchmarks and processing their results, together with detailed descriptions and some additional results not presented in the paper, are available online³.

Table 1 shows the numbers of benchmarks in each benchmark family solved by the individual solvers. Q3B is able to solve the most benchmarks in benchmark families 2017-Preiner-scholl-smt08, 2017-Preiner-tptp, 2017-Preiner-UltimateAutomizer, 2018-Preiner-cav18, and wintersteiger, and it is competitive in the remaining families. In total, Q3B also solves more formulas than each of the other solvers: 116 more than Boolector, 83 more than CVC4, and 139 more than Z3. Although the numbers of solved formulas for the solvers seem fairly similar, the cross-comparison in Table 2 shows that the differences among the individual solvers are actually larger. For each other solver, there are at least 143 benchmarks that can be solved by Q3B but not by the other solver. We think this shows the importance of developing an smt solver based on bdds and approximations besides the solvers based on quantifier instantiation.

We have described the architecture and inner workings of the first stable version of the state-of-the-art smt solver Q3B. Experimental evaluation on all quantified bit-vector formulas from smt-lib repository shows that this solver slightly outperforms other state-of-the-art solvers for such formulas.

As future work, we would like to drop the dependency on the Z3 api: namely to implement our own representation of formulas and reimplement all the simplifications currently outsourced to Z3 api directly in Q3B. We also plan to extend some simplifications with an additional bookkeeping needed to construct a model of the original formula. With these extensions, all simplifications could be used even if the user wants to get a model of the formula. We would also like to implement production of unsatisfiable cores since they are also valuable for software verification.