String Solving with Stabilization and Transducers (Technical Report)

TL;DR

This paper extends an automata-based string constraint solving approach to handle relational constraints with finite-state transducers, improving efficiency and performance significantly.

Contribution

It generalizes the stabilization-based method to support transducers, introduces heuristics for better efficiency, and demonstrates substantial performance improvements.

Findings

Outperforms existing solvers on benchmarks with relational constraints

Solves more instances and runs orders of magnitude faster

Reduces the need for expensive concatenation elimination

Abstract

We generalize an efficient automata-based approach to string constraint solving, the stabilization-based method behind the solver Z3-Noodler, to support relational constraints represented by finite-state transducers (useful, for example, for modeling replaceAll constraints). We focus on an efficient treatment of length constraints by reducing the need for expensive concatenation elimination, which is a major bottleneck in automata-based string solving. We also propose powerful heuristics that significantly improve performance in practice. Implemented on top of Z3-Noodler, our method vastly outperforms existing solvers on benchmarks with relational constraints. It solves more instances and runs orders of magnitude faster.