An efficient decision procedure for the theory of fixed-sized bit-vectors

Abstract

In this paper we describe a decision procedure for the core theory of fixed-sized bit-vectors with extraction and composition that can readily be integrated into Shostak's procedure for deciding combinations of theories. Inputs to the solver are unquantified bit-vector equations t = u and the algorithm returns true if t = u is valid in the bit-vector theory, false if t = u is unsatisfiable, and a system of solved equations otherwise. The time complexity of the solver is O(| t |·log n + n2), where t is the length of the bit-vector term t and n denotes the number of bits on either side of the equation. Then, the solver for the core bit-vector theory is extended to handle other bit-vector operations like bitwise logical operations, shifting, and arithmetic interpretations of bit-vectors. We develop a BDD-like data-structure called bit-vector BDDs to represent bit-vectors, various operations on bit-vectors, and a solver on bit-vector BDDs.