Z3++ is a derived SMT solver based on Z3, by combining local search and preprocessing techniques into Z3. Z3++ won the gold for Biggest Lead Model Validation and Largest Contribution Model Validation in SMT-COMP 2022 and 2023.
For any solver built upon Z3++, we would appreciate that the solver includes "Z3++" in the name for credit.
The homepage of Z3++ is http://z3-plus-plus.github.io/
Reference can be found as follows:
Shaowei Cai, Bohan Li, Jinkun Lin, Bohua Zhan, Xindi Zhang, Mengyu Zhao. "Z3++ at SMT-COMP 2023"
Shaowei Cai, Bohan Li, Xindi Zhang. "Local Search For SMT on Linear Integer Arithmetic." In CAV 2022 Shaowei Cai, Bohan Li, Xindi Zhang. "Local Search For Satisfiability Modulo Integer Arithmetic Theories" In ACM Transactions on Computational Logic 2023
Z3 is a theorem prover from Microsoft Research. It is licensed under the MIT license.
If you are not familiar with Z3, you can start here.
Pre-built binaries for stable and nightly releases are available from here.
Z3 can be built using Visual Studio, a Makefile or using CMake. It provides bindings for several programming languages.
See the release notes for notes on various stable releases of Z3.
| Azure Pipelines | Code Coverage | Open Bugs | Android Build | WASM Build |
|---|---|---|---|---|
 |
 |
 |
 |
32-bit builds, start with:
python scripts/mk_make.pyor instead, for a 64-bit build:
python scripts/mk_make.py -xthen:
cd build
nmakeZ3 uses C++17. The recommended version of Visual Studio is therefore VS2019.
Execute:
python scripts/mk_make.py
cd build
make
sudo make installNote by default g++ is used as the C++ compiler if it is available. If you
would prefer to use Clang change the mk_make.py invocation to:
CXX=clang++ CC=clang python scripts/mk_make.pyNote that Clang < 3.7 does not support OpenMP.
You can also build Z3 for Windows using Cygwin and the Mingw-w64 cross-compiler. To configure that case correctly, make sure to use Cygwin's own python and not some Windows installation of Python.
For a 64 bit build (from Cygwin64), configure Z3's sources with
CXX=x86_64-w64-mingw32-g++ CC=x86_64-w64-mingw32-gcc AR=x86_64-w64-mingw32-ar python scripts/mk_make.pyA 32 bit build should work similarly (but is untested); the same is true for 32/64 bit builds from within Cygwin32.
By default, it will install z3 executable at PREFIX/bin, libraries at
PREFIX/lib, and include files at PREFIX/include, where PREFIX
installation prefix is inferred by the mk_make.py script. It is usually
/usr for most Linux distros, and /usr/local for FreeBSD and macOS. Use
the --prefix= command line option to change the install prefix. For example:
python scripts/mk_make.py --prefix=/home/leo
cd build
make
make installTo uninstall Z3, use
sudo make uninstallTo clean Z3 you can delete the build directory and run the mk_make.py script again.
Z3 has a build system using CMake. Read the README-CMake.md file for details. It is recommended for most build tasks, except for building OCaml bindings.
Z3 itself has few dependencies. It uses C++ runtime libraries, including pthreads for multi-threading. It is optionally possible to use GMP for multi-precision integers, but Z3 contains its own self-contained multi-precision functionality. Python is required to build Z3. To build Java, .Net, OCaml, Julia APIs requires installing relevant tool chains.
Z3 has bindings for various programming languages.
You can install a nuget package for the latest release Z3 from nuget.org.
Use the --dotnet command line flag with mk_make.py to enable building these.
See examples/dotnet for examples.
These are always enabled.
See examples/c for examples.
These are always enabled.
See examples/c++ for examples.
Use the --java command line flag with mk_make.py to enable building these.
See examples/java for examples.
Use the --ml command line flag with mk_make.py to enable building these.
See examples/ml for examples.
You can install the Python wrapper for Z3 for the latest release from pypi using the command
pip install z3-solverUse the --python command line flag with mk_make.py to enable building these.
Note that it is required on certain platforms that the Python package directory
(site-packages on most distributions and dist-packages on Debian based
distributions) live under the install prefix. If you use a non standard prefix
you can use the --pypkgdir option to change the Python package directory
used for installation. For example:
python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/python-2.7/site-packagesIf you do need to install to a non standard prefix a better approach is to use
a Python virtual environment
and install Z3 there. Python packages also work for Python3.
Under Windows, recall to build inside the Visual C++ native command build environment.
Note that the build/python/z3 directory should be accessible from where python is used with Z3
and it depends on libz3.dll to be in the path.
virtualenv venv
source venv/bin/activate
python scripts/mk_make.py --python
cd build
make
make install
# You will find Z3 and the Python bindings installed in the virtual environment
venv/bin/z3 -h
...
python -c 'import z3; print(z3.get_version_string())'
...See examples/python for examples.
The Julia package Z3.jl wraps the C++ API of Z3. Information about updating and building the Julia bindings can be found in src/api/julia.
A WebAssembly build with associated TypeScript typings is published on npm as z3-solver. Information about building these bindings can be found in src/api/js.
Project MachineArithmetic provides Smalltalk interface to Z3's C API. For more information, see MachineArithmetic/README.md
-
Default input format is SMTLIB2
-
Other native foreign function interfaces:
-
Python API (also available in pydoc format)
-
C
-
OCaml
-
Smalltalk (supports Pharo and Smalltalk/X)