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

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

JONÁŠ Martin STREJČEK Jan

Year of publication 2018
Type Article in Proceedings
Conference Theoretical Aspects of Computing – ICTAC 2018
MU Faculty or unit

Faculty of Informatics

Citation
Web 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
Keywords satisfiability modulo theories; binary decision diagrams; abstractions; bit-vectors
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.