What is Z3?
As per Microsoft Research in this tutorial:
Z3 is a state-of-the art theorem prover from Microsoft Research. It can be used to check the satisfiability of logical formulas over one or more theories. Z3 offers a compelling match for software analysis and verification tools, since several common software constructs map directly into supported theories.
Installing Z3 for python on Windows 10
My steps differ somewhat from those given in [RM] for python:
I build the python bindings in the local repo of the cloned, latest release to have a single Z3 version on my system. I can then copy the necessary files into any python environment I choose.
Note: This installation requires Visual Studio.
Many other software installations also rely on it, so go ahead: download it and install it: you won’t regret it!
Step 1: Create a local repo for Z3 by cloning the latest stable release into some local
As of my installation, the release number was
z3-4.8.10. This information is not stated in [RM], but an installation using the cloned main Z3 repo (without any branch option for the
git clone command), will fail.
cd <project> git clone --depth 1 -b z3-4.8.10 https://github.com/Z3Prover/z3.git
Step 2: Create the makefile into the local Z3 repo [RM]:
cd z3 python scripts/mk_make.py -x --python
This step creates a build folder containing a Makefile and ends with clear instructions:
[...] Makefile was successfully generated. compilation mode: Release platform: x64 To build Z3, open a [Visual Studio x64 Command Prompt], then type 'cd C:\<path\to\project>\z3\build && nmake' Remark: to open a Visual Studio Command Prompt, go to: "Start > All Programs > Visual Studio > Visual Studio Tools"
Step 3: Open a Visual Studio Command Prompt:
On my system (Windows 10x64, VS 2019):
- Select Start [Windows logo key on the keyboard] and scroll to the letter V.
- Expand the Visual Studio 2019 folder
- Select & launch: ‘x64 Native Tools Command prompt for VS 2019’
Step 4: Build Z3 with the created Makefile from the VS command prompt:
cd C:\<path\to\project>\z3\build && nmake & REM use the command given at end of Step 2.
The output lists all the C++ modules generated (in around 10 minutes on my system). A successful build ends with these lines:
Z3 was successfully built. "Z3Py scripts can already be executed in the 'build\python' directory." "Z3Py scripts stored in arbitrary directories can be executed if the 'build\python' directory is added to the PYTHONPATH environment variable and the 'build' directory is added to the PATH environment variable."
After a successful build, the
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. Decoded, “from where python is used” means a Python environment.
Step 5: Add the path to
libz3.dll to the
Z3_LIBRARY_PATH environment variable.
Step 6: Add Z3 to an enviroment, e.g.
- 6.0: Activate the environment (I’m using conda):
conda activate env1
- 6.1: Install the Python wrapper for Z3:
pip install z3-solver
- 6.2 Locate the environment site-packages folder:
In a default Anaconda installation, the path to the environment site-packages folder is:
python -c "import site; print(site.getsitepackages())"
- 6.3: Copy the Z3 folder from the
<project>/z3/build/python/directory into the
environment site-packages/z3 directory.
Step 7: Test
(env1)> python >>> import z3 >>> z3.Int('x') x >>> exit()
If you pass the test, you’re all set with Z3!