Z3-Noodler: An Automata-based String Solver (Technical Report)

TL;DR

Z3-Noodler introduces a new automata-based string solver using stabilization algorithms, demonstrating competitive performance and complementarity with existing solvers in solving word equations with regular constraints.

Contribution

It presents a novel string solver based on automata and stabilization algorithms, integrated into Z3, with extensive evaluation showing its effectiveness and complementary strengths.

Findings

Outperforms many state-of-the-art solvers on benchmarks

Works well as part of solver portfolios due to its complementarity

Successfully solves complex word equations with regular constraints

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.