Logo image
Back
Even Faster Conflicts and Lazier Reductions for String Solvers
Conference proceeding   Open access   Peer reviewed

Even Faster Conflicts and Lazier Reductions for String Solvers

Andres Notzli, Andrew Reynolds, Haniel Barbosa, Clark Barrett and Cesare Tinelli
COMPUTER AIDED VERIFICATION (CAV 2022), PT II, Vol.13372, pp.205-226
Lecture Notes in Computer Science
01/01/2022
DOI: 10.1007/978-3-031-13188-2_11
url
https://doi.org/10.1007/978-3-031-13188-2_11View
Published (Version of record) Open Access

Abstract

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.
 Computer Science Technology Computer Science, Hardware & Architecture Computer Science, Software Engineering Computer Science, Theory & Methods Science & Technology

Details

Metrics

19 Record Views
8 Times Cited - Web of Science
Logo image