An SMT solver for regular expressions and linear arithmetic over string length

DOI10.1007/978-3-030-81688-9_14zbMATH Open1493.68182arXiv2010.07253OpenAlexW3186328512MaRDI QIDQ832270FDOQ832270

Authors: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel D. Day, Dirk Nowotka, Vijay Ganesh 

Publication date: 25 March 2022

Abstract: We present a novel length-aware solving algorithm for the quantifier-free first-order theory over regex membership predicate and linear arithmetic over string length. We implement and evaluate this algorithm and related heuristics in the Z3 theorem prover. A crucial insight that underpins our algorithm is that real-world instances contain a wealth of information about upper and lower bounds on lengths of strings under constraints, and such information can be used very effectively to simplify operations on automata representing regular expressions. Additionally, we present a number of novel general heuristics, such as the prefix/suffix method, that can be used in conjunction with a variety of regex solving algorithms, making them more efficient. We showcase the power of our algorithm and heuristics via an extensive empirical evaluation over a large and diverse benchmark of 57256 regex-heavy instances, almost 75% of which are derived from industrial applications or contributed by other solver developers. Our solver outperforms five other state-of-the-art string solvers, namely, CVC4, OSTRICH, Z3seq, Z3str3, and Z3-Trau, over this benchmark, in particular achieving a 2.4x speedup over CVC4, 4.4x speedup over Z3seq, 6.4x speedup over Z3-Trau, 9.1x speedup over Z3str3, and 13x speedup over OSTRICH.

Full work available at URL: https://arxiv.org/abs/2010.07253

Recommendations

• An efficient SMT solver for string constraints
• A decision procedure for string logic with quadratic equations, regular expressions and length constraints
• Symbolic solving of extended regular expression inequalities
• Extended regular expressions: succinctness and decidability
• Extended Regular Expressions: Succinctness and Decidability
• A Compact Proof of Decidability for Regular Expression Equivalence
• Towards more efficient methods for solving regular-expression heavy string constraints

zbMATH Keywords

SMT solversregular expressionsstring solvers

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Formalization of mathematics in connection with theorem provers (68V20) Algorithms on strings (68W32)

Cites Work

• Derivatives of Regular Expressions
• An efficient algorithm for solving word equations
• Satisfiability of word equations with constants is in PSPACE
• Title not available (Why is that?)
• Makanin's algorithm for word equations-two improvements and a generalization
• Path Feasibility Analysis for String-Manipulating Programs
• A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings
• Automata-based model counting for string constraints
• The satisfiability of word equations: decidable and undecidable theories
• String theories involving regular membership predicates: from practice to theory and back
• String solving with word equations and transducers: towards a logic for analysing mutation XSS
• Progressive Reasoning over Recursively-Defined Strings
• Quadratic word equations with length constraints, counter systems, and Presburger arithmetic with divisibility

Cited In (8)

• Solving String Theories Involving Regular Membership Predicates Using SAT
• A closer look at the expressive power of logics based on word equations
• String theories involving regular membership predicates: from practice to theory and back
• Word equations in synergy with regular constraints
• Towards more efficient methods for solving regular-expression heavy string constraints
• Verified verifying: SMT-LIB for strings in Isabelle
• Incremental dead state detection in logarithmic time
• Solving string constraints using SAT

Uses Software

• SMT-LIB
• z3
• Stranger
• CVC4
• HAMPI
• Jalangi
• Z3str3
• Z3str2
• GitHub
• StringFuzz

This page was built for publication: An SMT solver for regular expressions and linear arithmetic over string length

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832270)