Z3 String Constraint Solver

Latest stable release: Official Z3 Repository

Z3str3 is a constraint solver for the quantifier-free theory of string equations, the regular-expression membership predicates, and linear arithmetic over the length functions. Z3str3 is now part of the Z3 theorem prover's main codebase, and is the primary string solver in Z3.

The Z3str3 string solver is being actively developed in close cooperation with the Z3 team at Microsoft Research. Additionally, this research is being supported by IBM, Amazon, Google, and NSERC Canada through various grants, awards, and research collaborations.