: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into ^*

Gergely Kovásznai, Andreas Fröhlich, and Armin Biere

Abstract. Bit-precise reasoning is essential in many applications of Satisfiability Modulo Theories (SMT). In recent years, efficient approaches for solving fixed-size bit-vector formulas have been developed. Most of these approaches rely on bit-blasting. In [1], we argued that bit-blasting is not polynomial in general, and then showed that solving quantifier-free bit-vector formulas () is -complete. In this paper, we present a tool based on a new polynomial translation from into Effectively Propositional Logic (). This allows us to solve problems using solvers and avoids the exponential growth that comes with bit-blasting. Additionally, our tool allows us to easily generate new challenging benchmarks for solvers.

^*Supported by FWF, NFN Grant S11408-N23 (RiSE).

LNAI 7898, p. 443 ff.

Full article in PDF | BibTeX

lncs@springer.com
© Springer-Verlag Berlin Heidelberg 2013