Logo image
Back
Reductions for Strings and Regular Expressions Revisited
Conference proceeding   Open access

Reductions for Strings and Regular Expressions Revisited

Andrew Reynolds, Andres Notzlit, Clark Barrett and Cesare Tinelli
2020 Formal Methods in Computer Aided Design (FMCAD), pp.225-235
09/21/2020
DOI: 10.34727/2020/isbn.978-3-85448-042-6_30
url
http://hdl.handle.net/20.500.12708/15526View
Open Access

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.
 Benchmark testing Cognition Data preprocessing Design automation Input variables Optimization Performance gain

Details

Metrics

20 Record Views
Logo image