An SMT Solver for Regular Expressions and Linear Arithmetic over String Length

TL;DR

This paper introduces a new length-aware algorithm for solving regex membership and linear string length constraints, implemented in Z3, which significantly outperforms existing solvers on industrial and diverse benchmarks.

Contribution

The paper presents a novel length-aware solving algorithm and heuristics for regex and linear arithmetic constraints, improving efficiency and performance in SMT solving.

Findings

Outperforms five state-of-the-art string solvers.

Achieves up to 13x speedup over OSTRICH.

Effective use of length bounds simplifies automata operations.

Abstract

We present a novel length-aware solving algorithm for the quantifier-free first-order theory over regex membership predicate and linear arithmetic over string length. We implement and evaluate this algorithm and related heuristics in the Z3 theorem prover. A crucial insight that underpins our algorithm is that real-world instances contain a wealth of information about upper and lower bounds on lengths of strings under constraints, and such information can be used very effectively to simplify operations on automata representing regular expressions. Additionally, we present a number of novel general heuristics, such as the prefix/suffix method, that can be used in conjunction with a variety of regex solving algorithms, making them more efficient. We showcase the power of our algorithm and heuristics via an extensive empirical evaluation over a large and diverse benchmark of 57256 regex-heavy instances, almost 75% of which are derived from industrial applications or contributed by other solver developers. Our solver outperforms five other state-of-the-art string solvers, namely, CVC4, OSTRICH, Z3seq, Z3str3, and Z3-Trau, over this benchmark, in particular achieving a 2.4x speedup over CVC4, 4.4x speedup over Z3seq, 6.4x speedup over Z3-Trau, 9.1x speedup over Z3str3, and 13x speedup over OSTRICH.