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.

翻译：我们泛化了一种高效的基于自动机的字符串约束求解方法，即求解器Z3-Noodler背后的稳定化方法，以支持由有限状态转导器表示的关系约束（例如，适用于建模replaceAll约束）。我们专注于高效处理长度约束，通过减少对昂贵的连接消除的需求，这是基于自动机的字符串求解中的一个主要瓶颈。我们还提出了强大的启发式策略，在实践中显著提升了性能。基于Z3-Noodler实现后，我们的方法在包含关系约束的基准测试中大幅超越现有求解器，能够解决更多实例，并且运行速度快出数个数量级。