Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Autoři

JONÁŠ Martin STREJČEK Jan

Druh Článek ve sborníku
Konference Theoretical Aspects of Computing – ICTAC 2018
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www https://link.springer.com/chapter/10.1007/978-3-030-02508-3_15
Doi http://dx.doi.org/10.1007/978-3-030-02508-3_15
Klíčová slova satisfiability modulo theories; binary decision diagrams; abstractions; bit-vectors
Popis BDD-based SMT solvers have recently shown to be competitive for solving satisfiability of quantified bit-vector formulas. However, these solvers reach their limits when the input formula contains complicated arithmetic. Hitherto, this problem has been alleviated by approximations reducing efficient bit-widths of bit-vector variables. In this paper, we propose an orthogonal abstraction technique working on the level of the individual instances of bit-vector operations. In particular, we compute only several bits of the operation result, which may be sufficient to decide the satisfiability of the formula. Experimental results show that our BDD-based SMT solver Q3B extended with these abstractions can solve more quantified bit-vector formulas from the smt-lib repository than state-of-the-art SMT solvers Boolector, CVC4, and Z3.
Související projekty: