3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Find a file
Nikolaj Bjorner 16fa1fa5db remove and
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-06 17:42:10 -07:00
cmake mux 2019-06-05 09:06:17 +01:00
contrib Fix bug in qprofdiff 2019-02-07 14:08:18 +00:00
doc Change from BINARY_DIR to PROJECT_BINARY_DIR 2019-05-15 11:25:40 -07:00
examples add #2298 to regression/example 2019-05-29 07:24:42 -07:00
noarch follow instructions from #1879 2018-10-15 11:44:47 -07:00
package Updated nuget package spec and directions 2018-11-13 12:19:20 -08:00
scripts Update nightly-windows.yaml for Azure Pipelines 2019-06-07 02:06:44 +02:00
src remove new_sub 2019-06-06 17:13:59 -07:00
.dockerignore [TravisCI] Implement TravisCI build and testing infrastructure for Linux 2017-07-01 11:51:30 +01:00
.gitattributes set text default to auto to try to avoid crlf disasters 2014-04-01 17:20:37 -07:00
.gitignore incrementally adding files from dotnet core pull request from @yatli 2019-01-20 10:40:11 -08:00
.travis.yml Revert "api: dotnet: switch to multi-targeting project and modern cmake-dotnet integration." 2019-01-16 10:21:56 -08:00
azure-pipelines.yml Update azure-pipelines.yml for Azure Pipelines 2019-06-07 02:03:46 +02:00
CMakeLists.txt cmake: addd SINGLE_THREADED option 2019-06-05 15:44:25 +01:00
configure Fix parameter expansion when configuring Z3 2018-03-09 14:20:31 +01:00
LICENSE.txt update license for space/quotes per #982 2017-04-24 13:34:10 -07:00
README-CMake.md Typo fixes. 2018-01-02 22:48:06 +07:00
README.md remove and 2019-06-06 17:42:10 -07:00
RELEASE_NOTES release notes 2018-12-20 10:32:36 -08:00

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 releases are available from here, and nightly builds 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

Z3Build-CI Windows x86 Windows x64 Ubuntu x64 Debian x64 macOS TravisCI
Build Status win32-badge win64-badge ubuntu-x64-badge debian-badge 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

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 an unofficial build system using CMake. Read the README-CMake.md file for details.

Z3 bindings

Z3 has bindings for various programming languages.

.NET

Use the --dotnet command line flag with mk_make.py to enable building these.

On non-windows platforms mono is required. On these platforms the location of the C# compiler and gac utility need to be known. You can set these as follows if they aren't detected automatically. For example:

CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil python scripts/mk_make.py --dotnet

Note for very old versions of Mono (e.g. 2.10) you may need to set CSC to /usr/bin/dmcs.

Note that when make install is executed on non-windows platforms the GAC utility is used to install Microsoft.Z3.dll into the GAC as the Microsoft.Z3.Sharp package. During install a pkg-config file (Microsoft.Z3.Sharp.pc) is also installed which allows the MonoDevelop IDE to find the bindings. Running make uninstall will remove the dll from the GAC and the pkg-config file.

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

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.

Web Assembly

WebAssembly bindings are provided by Cl<43>ment Pit-Claudel.