Effective String Solving via Regular Constraint Propagation

The past decade has witnessed substantial developments in string solving. Motivated by the complexity of existing string solving strategies, we propose as a simple but effective and generic method for solving string constraints: regular constraint propagation. This method repeatedly computes pre- or post-images of regular languages under the string functions present in a string formula, inferring more and more knowledge about the possible values of string variables, until either a conflict is found or satisfiability of the string formula can be concluded. Such a propagation strategy is applicable to string constraints with multiple operations like concatenation, replace, and almost all flavors of string transductions. We demonstrate the generality and effectiveness of the method theoretically and experimentally. On the theoretical side, we show that the method is sound and complete for a large fragment of string constraints, subsuming both straight-line and chain-free constraints, which are the hitherto largest decidable fragments of string constraints supported by string solvers. One common reason for the unsatisiability of a string constraint is due to the interaction between string operations and the regular constraints. Consider, for example, the string constraint $\varphi: = x = yy \wedge x \in a^+b^+ \wedge y \in (a^+|b^+)$, which is unsatisfiable because the right hand side of the equation admits only strings of the form $a^+$ or of the form $b^+$, which are not admitted by the left hand side. One simple yet effective method in proving such an unsatisfiability is regular constraint propagation. Essentially, this means propagating regular constraints between the left-hand side and right-hand side of string equations, which could contain various string functions including concatenation, replaceAll, etc. This idea has been formalized in a proof system that is implemented in the OSTRICH string solver, the 2023 winner of the SMT-COMP QF\_S category of pure string constraints. In addition to concatenation and regular constraints, OSTRICH has a good support of various complex string functions, including replaceAll, transducers, reverse, and string functions from JavaScript library related to real-world regular expressions that are not immediately available in most other string solvers. In this presentation, we demonstrate that even simple strategies can solve a wide range of benchmarks in string solving. We build upon a sound proof system established in previous work, highlighting that the main challenge in such a system is the search for a proof. Joint work with Matthew Hague, Artur Jeż, Anthony W. Lin and Philipp Rümmer

Authors

• Oliver Markgraf

Keywords

No keywords are indexed for this paper.