bv2epr: a tool for polynomially translating quantifier-free bit-vector formulas into EPR 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 , 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 into 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.
Keywords for this software
References in zbMATH (referenced in 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- Biere, Armin; Kröning, Daniel: SAT-based model checking (2018)
- Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: Complexity of fixed-size bit-vector logics (2016)
- Sebastiani, Roberto: Colors make theories hard (2016)
- Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp: Deciding bit-vector formulas with mcsat (2016)
- Cook, Byron; Kroening, Daniel; Rümmer, Philipp; Wintersteiger, Christoph M.: Ranking function synthesis for bit-vector relations (2013)
- Fröhlich, Andreas; Kovásznai, Gergely; Biere, Armin: More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding (2013)
- Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin: bv2epr: a tool for polynomially translating quantifier-free bit-vector formulas into EPR (2013)
Further publications can be found at: http://fmv.jku.at/papers/index.html