“Even Faster Conflicts and Lazier Reductions for String Solvers” by Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark Barrett, and Cesare Tinelli. In Proceedings of the 34^th International Conference on Computer Aided Verification (CAV '22), (Sharon Shoham and Yakir Vizel, eds.), Aug. 2022, pp. 205-226.
In the past decade, satisfiability modulo theories (SMT) solvers have been extended to support the theory of strings and regular expressions. This theory has proven to be useful in a wide range of applications in academia and industry. To accommodate the expressive nature of string constraints used in those applications, string solvers use a multi-layered architecture where extended operators are reduced to a set of core operators. These reductions, however, are often costly to reason about. In this work, we propose new techniques for eagerly discovering conflicts based on equality reasoning and lazily avoiding reductions for certain extended functions based on lightweight reasoning. We present a strategy for integrating and scheduling these techniques in a CDCL(T)-based theory solver for strings and regular expressions. We implement the techniques and the strategy in cvc5, a state-of-the-art SMT solver, and show that they lead to a significant performance improvement.
BibTeX entry:
@inproceedings{NRB+22,
author = {Andres N{\"o}tzli and Andrew Reynolds and Haniel Barbosa and
Clark Barrett and Cesare Tinelli},
editor = {Sharon Shoham and Yakir Vizel},
title = {Even Faster Conflicts and Lazier Reductions for String Solvers},
booktitle = {Proceedings of the {\it 34^{th}} International Conference
on Computer Aided Verification (CAV '22)},
series = {Lecture Notes in Computer Science},
volume = {13372},
pages = {205--226},
publisher = {Springer},
month = aug,
year = {2022},
doi = {10.1007/978-3-031-13188-2_11},
url = {http://theory.stanford.edu/~barrett/pubs/NRB+22.pdf}
}
(This webpage was created with bibtex2web.)