Z3++ is a derived SMT solver based on Z3, which participated in SMT-COMP 2022 and won the gold for Biggest Lead Model Validation and Largest Contribution Model Validation.
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, Zhonghan Wang, Bohua Zhan, Xindi Zhang, Mengyu Zhao. "Z3++ at SMT-COMP 2022" https://github.com/z3-plus-plus/z3-plus-plus.github.io/blob/main/Z3++_at_SMT_COMP_2022.pdf
Shaowei Cai, Bohan Li, Xindi Zhang. "Local Search For SMT on Linear Integer Arithmetic." In CAV 2022
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.py
or instead, for a 64-bit build:
python scripts/mk_make.py -x
then:
cd build
nmake
Z3 uses C++17. The recommended version of Visual Studio is therefore VS2019.
Execute:
python scripts/mk_make.py
cd build
make
sudo make install
Note 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.py
Note 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.py
A 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 install
To uninstall Z3, use
sudo make uninstall
To 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-solver
Use 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-packages
If 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)