bv2epr: a tool for polynomially translating quantifier-free bit-vector formulas into EPR

DOI10.1007/978-3-642-38574-2_32zbMATH Open1382.68217OpenAlexW117910965MaRDI QIDQ4928459FDOQ4928459

Authors: Gergely Kovásznai, Andreas Fröhlich, Armin Biere 

Publication date: 14 June 2013

Published in: Automated Deduction – CADE-24 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-38574-2_32

Recommendations

• Efficiently solving quantified bit-vector formulas
• More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding
• Solving quantified bit-vector formulas using binary decision diagrams
• Complexity of fixed-size bit-vector logics
• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic

Mathematics Subject Classification ID

Cited In (4)

• More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• bv2epr
• Complexity of fixed-size bit-vector logics

Uses Software

• SMT-LIB

This page was built for publication: bv2epr: a tool for polynomially translating quantifier-free bit-vector formulas into EPR

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4928459)