Need help with z3?
Click the “chat” button below for chat support from the developer who created it, or find similar developers for support.

About the developer

Z3Prover
5.9K Stars 978 Forks Other 14.7K Commits 181 Opened issues

Description

The Z3 Theorem Prover

Services available

!
?

Need anything else?

Contributors list

No Data

Z3

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.

Build status

| Azure Pipelines | TravisCI | | --------------- | -------- | Build Status | Build Status

Building Z3 on Windows using Visual Studio Command Prompt

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

Building Z3 using make and GCC/Clang

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

bash
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 if 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.

Building Z3 using CMake

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.

Dependencies

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 bindings

Z3 has bindings for various programming languages.

.NET

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.

C

These are always enabled.

See

examples/c
for examples.

C++

These are always enabled.

See

examples/c++
for examples.

Java

Use the

--java
command line flag with
mk_make.py
to enable building these.

See

examples/java
for examples.

OCaml

Use the

--ml
command line flag with
mk_make.py
to enable building these.

See

examples/ml
for examples.

Python

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 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.

Julia

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.

Web Assembly

WebAssembly bindings are provided by Clément Pit-Claudel.

System Overview

System Diagram

Interfaces

We use cookies. If you continue to browse the site, you agree to the use of cookies. For more information on our use of cookies please see our Privacy Policy.