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

arXiv: https://arxiv.org/abs/2010.07253 · HTML: https://mlsanity.com/paper/2010.07253/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Oct 2020.

## Built on by (most cited first, 2 of 2)

- [Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis](https://mlsanity.com/paper/2401.17159/) (2024)
- [String Theories involving Regular Membership Predicates: From Practice to Theory and Back](https://mlsanity.com/paper/2105.07220/) (2021)

## Abstract (arXiv)

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.