Reductions for Strings and Regular Expressions Revisited

“Reductions for Strings and Regular Expressions Revisited” by Andrew Reynolds, Andres Nötzli, Clark Barrett, and Cesare Tinelli. In Proceedings of the 20^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '20), (Alexander Ivrii and Ofer Strichman, eds.), Sep. 2020, pp. 225-235.

Abstract

The theory of strings supported by solvers in formal methods contains a large number of operators. Instead of implementing a semi-decision procedure that reasons about all the operators directly, string solvers often reduce operators to a core fragment and implement a semi-decision procedure over that fragment. These reductions considerably increase the number of constraints and thus have to be done carefully to achieve good performance. We propose novel reductions from regular expressions to string constraints and a framework for minimizing the introduction of new variables in current reductions of string constraints. The reductions of regular expression constraints enable string solvers to handle a significant fragment of such constraints without using dedicated reasoning over regular expressions. Minimizing the number of variables in the reduced constraints makes those constraints significantly cheaper to solve by the core solver. An experimental evaluation of our implementation of both techniques in CVC4, a state-of-the-art SMT solver with extensive support for the theory of strings, shows that they significantly improve the solver's performance.

BibTeX entry:

@inproceedings{RNB+20-FMCAD,
   author = {Andrew Reynolds and Andres N{\"o}tzli and Clark Barrett and
	Cesare Tinelli},
   editor = {Alexander Ivrii and Ofer Strichman},
   title = {Reductions for Strings and Regular Expressions Revisited},
   booktitle = {Proceedings of the {\it 20^{th}} International Conference
	on Formal Methods In Computer-Aided Design (FMCAD '20)},
   pages = {225--235},
   publisher = {TU Wien Academic Press},
   month = sep,
   year = {2020},
   doi = {10.34727/2020/isbn.978-3-85448-042-6_30},
   url = {http://theory.stanford.edu/~barrett/pubs/RNB+20-FMCAD.pdf}
}

(This webpage was created with bibtex2web.)