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: |