Truncating abstraction of bit-vector operations for BDD-based SMT solvers

Logo poskytovatele

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

JONÁŠ Martin STREJČEK Jan

Rok publikování 2024
Druh Článek v odborném periodiku
Časopis / Zdroj THEORETICAL COMPUTER SCIENCE
Fakulta / Pracoviště MU

Fakulta informatiky

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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info