Truncating abstraction of bit-vector operations for BDD-based SMT solvers
Autoři | |
---|---|
Rok publikování | 2024 |
Druh | Článek v odborném periodiku |
Časopis / Zdroj | THEORETICAL COMPUTER SCIENCE |
Fakulta / Pracoviště MU | |
Citace | |
www | https://doi.org/10.1016/j.tcs.2024.114664 |
Doi | http://dx.doi.org/10.1016/J.TCS.2024.114664 |
Klíčová slova | Bit-vector theory; Operation abstraction; Q3B; SMT solving |
Popis | During the last few years, BDD-based SMT solvers proved to be competitive in deciding satisfiability of quantified bit-vector formulas. However, these solvers usually do not perform well on input formulas with complicated arithmetic. Hitherto, this problem has been alleviated by approximations reducing effective bit-widths of bit-vector variables. In this paper, we propose an orthogonal abstraction technique that works 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 SMT solvers Boolector, CVC4, and Z3. |
Související projekty: |