Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic

Abstract

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.