Z3str3 String Constraint Solver

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.

Latest Stable Release: Z3str3 1.0.0 (May 5, 2017)

The benchmarks (for Z3str2) used in CAV'15 paper are available in the Github Repo.



Release history

2017-05-05 (1) Z3str3 1.0.0 released. 
(2) Support for SMT-LIB 2.5 strings draft standard added.
2015-02-09 (1) Z3str2 1.0.0 released.
(2) Regex support added.
(3) Overlapping variables detection.
(4) Bi-directional integration between string and integer theories.


2014-12-05 (1) Change version identifier to Z3-str 1.0.0.
(2) String/Integer theory integration.
(3) Fix Several bugs.
(4) Performance optimization tweaks.


2014-07-20 (1) Remove the upper bound of the length searched for free variable.
(2) Use the 256 ASCII character set as the default alphabet.
(3) Fix Several bugs.
(4) Performance optimization tweaks.


2014-01-20 (1) Return "UNKNOWN" for not well-formed inputs whose solution may be in the ignored loop-inducing cuts. 
(2) Allow setting the upper bound of length searched for free variables.
(3) Minor bugs fixed.
(4) The universe of the value of free variables changed from {'@'} to a set of alphabets
(5) Supports for operators "StartsWith" and "EndsWith" added


2013-10-03 (1) Solving procedure improved. On average, it runs ~3.5x faster than the initial release.
(2) Bugs fixed.


2013-06-02 Initial release