BV2EPR

News

• 2013-03-27: v1.0 released.

Overview

BV2EPR is a tool for translating a QF_BV formula in SMT2 format into an EPR clause set in TPTP format.

Downloads

Evaluation

• Benchmarking scripts and generated benchmarks used for experiments described in G. Kovásznai, A. Fröhlich, A. Biere. BV2EPR: A Tool for Polynomially Translating Quantifier-free Bit-Vector Formulas into EPR. See also the README file that is part of the 1st package.
• Soundness checker scripts. See also the README file that is part of the package.
• Fuzzing script.

Related Publications

• G. Kovásznai, A. Fröhlich, A. Biere. BV2EPR: A Tool for Polynomially Translating Quantifier-free Bit-Vector Formulas into EPR. In Proc. 24th Intl.  Conference on Automated Deduction (CADE-24), Lake Placid, New York, US, 2013, accepted.
• G. Kovásznai, A. Fröhlich, A. Biere. On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width. In Proc. 10th Intl. Workshop on Satisfiability Modulo Theories (SMT'12), pages 44-55, aff. to IJCAR'12, Manchester, UK, 2012.

Related Slides

• Other Target Logics for Bit-Vector Formulas? PUMA-RiSE Workshop, Goldegg, Austria, 2012.
• On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width. SMT'12, aff. to IJCAR'12, Manchester, UK, 2012.

License