Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic
We present the key ideas in the design and implementation of Beaver,
an SMT solver for quantifier-free finite-precision bit-vector logic (QF BV). Beaver
uses an eager approach, encoding the original SMT problem into a Boolean satis-
fiability (SAT) problem using a series of word-level and bit-level transformations.
In this paper, we describe the most effective transformations, such as propagating
constants and equalities at the word-level, and using and-inverter graph rewriting
techniques at the bit-level. We highlight implementation details of these transformations that distinguishes Beaver from other solvers. We present an experimental
analysis of the effectiveness of Beaver’s techniques on both hardware and soft-
ware benchmarks with a selection of back-end SAT solvers.
Beaver is an open-source tool implemented in Ocaml, usable with any back-end
SAT engine, and has a well-documented extensible code base that can be used to
experiment with new algorithms and techniques.