mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity
No description
4400 commits 24 branches 48 tags 158 MiB
Find a file
Dan Liew f09fa3c87b Recent changes to the build system mean that setting a custom 
``--prefix=`` is likely to disable installing the Python bindings so
the old instructions aren't helpful. Reword them and mention using
``DESTDIR``.
2015-12-12 10:22:56 +00:00
doc C API cleanup. Mainly removal of ML-specific macros that are not used anymore and inline documentation fixes. 2015-12-03 17:33:25 +00:00
examples add python visitor example in response to Stackoverflow question 2015-12-06 20:09:13 -08:00
scripts Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-09 07:37:51 -08:00
src ensure that formula is skolemized in the smt solver when using MBQI 2015-12-11 18:18:09 +00:00
.gitattributes set text default to auto to try to avoid crlf disasters 2014-04-01 17:20:37 -07:00
.gitignore pull unstable 2015-04-01 14:57:11 -07:00
configure Add configure script that is just a wrapper for python 'src/mk_make.py'. It makes the build more user friendly for users familiar with ./configure + make idiom 2013-01-13 11:34:05 -08:00
LICENSE.txt Move to MIT License 2015-03-26 11:44:49 -07:00
README.md Recent changes to the build system mean that setting a custom 2015-12-12 10:22:56 +00:00
RELEASE_NOTES add to release notes 2015-10-05 09:31:14 -07:00

README.md

Z3

Z3 is a theorem prover from Microsoft Research. Z3 is licensed under the MIT license. Z3 can be built using Visual Studio Command Prompt and make/g++.

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/g++ and Python

Execute:

   python scripts/mk_make.py
   cd build
   make
   sudo make install

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

Note the above will typically disable the installation of the Python bindings because the Python site-packages directory (e.g. /usr/lib/python3.5/site-packages/) is not rooted in the install prefix and installing outside of the install prefix is dangerous and misleading.

To avoid this issue you can use the DESTDIR makefile variable and leave the install prefix as the default. The DESTDIR variable is prepended to the install locations during make install and make uninstall and is intended to allow "staged installs". Therefore it must always contain a trailing slash.

For example:

  python scripts/mk_make.py
  cd build
  make
  make install DESTDIR=/home/leo/

In this example, the Z3 Python bindings will be stored at /home/leo/lib/pythonX.Y/site-packages (/home/leo/lib/pythonX.Y/dist-packages on Debian based Linux distributions) where X.Y corresponds to the python version in your system.

To uninstall Z3, use

  sudo make uninstall

Building Z3 using clang and clang++ on Linux/OSX

Remark: clang does not support OpenMP yet.

   CXX=clang++ CC=clang python scripts/mk_make.py
   cd build
   make

To clean Z3 you can delete the build directory and run the mk_make.py script again.