Getting Started

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: Official Z3 repository

Install

    1. Check out the latest version of Z3 from the Z3 Git repository.
    2. From the top-level directory, create the build scripts by running "python scripts/mk_make.py".
    3. Build Z3 by running "cd build ; make".
    4. After successfully building Z3, the build/ directory will contain a binary called "z3".
    5. Z3str3 can be invoked by calling Z3 directly from the command line, e.g. "./z3 ~/path/to/benchmark/instance.smt2", or through the Z3 API bindings (available for a number of programming languages including C++ and Python).
    6. To ensure that Z3str3 is used, it is recommended to tell Z3 explicitly which solver to use for strings. This is done by setting the "smt.string_solver" parameter to "z3str3". On the command line this is passed as an argument, e.g. "z3 smt.string_solver=z3str3 instance.smt2".

Acknowledgements

We would like to thank the following people and teams for their valuable contributions, comments or suggestions:

    • Special thanks to the S3 string solver team for their generous help on integer/string theory integration.
    • CVC4 team for the valuable dicussions
    • Benjamin Spencer for suggestions on fixing linking errors
    • Julian Thomé for suggestions on building Z3-str on Mac OS X
    • Julian Thomé for suggestions and contributions on improving the front-end string constraint encoding interface
    • Prof. Nickolai Zeldovich for a bug report and suggestions on Python API