Truncating abstraction of bit-vector operations for BDD-based SMT solvers
| Authors | |
|---|---|
| Year of publication | 2024 |
| Type | Article in Periodical |
| Magazine / Source | THEORETICAL COMPUTER SCIENCE |
| MU Faculty or unit | |
| Citation | |
| web | https://doi.org/10.1016/j.tcs.2024.114664 |
| Doi | http://dx.doi.org/10.1016/J.TCS.2024.114664 |
| Keywords | Bit-vector theory; Operation abstraction; Q3B; SMT solving |
| Description | 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. |
| Related projects: |