String Solving with Stabilization and Transducers (Technical Report)
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909053840523264 |
|---|---|
| author | Chocholatý, David Havlena, Vojtěch Holík, Lukáš Síč, Juraj Šedý, Michal |
| author_facet | Chocholatý, David Havlena, Vojtěch Holík, Lukáš Síč, Juraj Šedý, Michal |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_14872 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | String Solving with Stabilization and Transducers (Technical Report) Chocholatý, David Havlena, Vojtěch Holík, Lukáš Síč, Juraj Šedý, Michal Formal Languages and Automata Theory Logic in Computer Science 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. |
| title | String Solving with Stabilization and Transducers (Technical Report) |
| topic | Formal Languages and Automata Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2605.14872 |