來自微軟研究院的Z3定理證明：Z3 Theorem Prover
Z3來自微軟研究院的定理證明
Z3可以使用 Visual Studio Command Prompt和make/g++構建
它依賴于Python2配置構建腳本。
1) Building Z3 on Windows using Visual Studio Command Prompt
python scripts/mk_make.py
cd build
nmake
2) 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 is the installation prefix used for installing Python in your system.
It is usually /usr for most Linux distros, and /usr/local for FreeBSD.
Use the following commands to install in a different prefix (e.g., /home/leo)
python scripts/mk_make.py --prefix=/home/leo
cd build
make
make install
In this example, the Z3 Python bindings will be stored at /home/leo/lib/pythonX.Y/dist-packages,
where X.Y corresponds to the python version in your system.
To uninstall Z3, use
sudo make uninstall
4) 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