BV2EPR: A Tool for Polynomially Translating Quantifier-free Bit-Vector Formulas into EPR
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
24th Intl. Conf. on Automated Deduction (CADE'13)
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
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 (QF_BV) is
NEXPTIME-complete. In this paper, we present a tool based on a new
polynomial translation from QF_BV to Effectively Propositional Logic
(EPR). This allows us to solve QF_BV-problems using EPR-solvers and
avoids the exponential growth that comes with bit-blasting.
Additionally, our tool allows us to easily generate new challenging
benchmarks for EPR solvers
Forschungs-