Z3-Noodler: An Automata-based String Solver (Technical Report)
Logic in Computer Science
2023-10-18 v2 Formal Languages and Automata Theory
Abstract
Z3-Noodler is a fork of Z3 that replaces its string theory solver with a custom solver implementing the recently introduced stabilization-based algorithm for solving word equations with regular constraints. An extensive experimental evaluation shows that Z3-Noodler is a fully-fledged solver that can compete with state-of-the-art solvers, surpassing them by far on many benchmarks. Moreover, it is often complementary to other solvers, making it a suitable choice as a candidate to a solver portfolio.
Cite
@article{arxiv.2310.08327,
title = {Z3-Noodler: An Automata-based String Solver (Technical Report)},
author = {Yu-Fang Chen and David Chocholatý and Vojtěch Havlena and Lukáš Holík and Ondřej Lengál and Juraj Síč},
journal= {arXiv preprint arXiv:2310.08327},
year = {2023}
}