How to install Z3
In case you find the Z3 README page confusing, here's how I installed Z3.
One can adjust the process to one's own needs. The version of Z3 I used is
We want to download the source code and compile it by ourselves. It might be
doable to use the binary releases by setting up
python scripts/mk_make.py --prefix=$HOME/usr --python --pypkgdir=$HOME/usr/lib/python-2.7/site-packages
I want to install it in my
cd build; make
Now if one takes a look at
Because we are using a user specified prefix, the command line produces the message:
Z3Py was installed at /.../usr/lib/python-2.7/site-packages, make sure this directory is in your PYTHONPATH environment variable. @echo Z3 was successfully installed.
export PYTHONPATH=$HOME/usr/lib/python-2.7/site-packages:$PYTHONPATHIf PYTHONPATH is undefined, do:
export PYTHONPATH=$HOME/usr/lib/python-2.7/site-packages @
from z3 import * x = Real('x') y = Real('y') s = Solver() s.add(x + y > 5, x > 1, y > 1) print(s.check()) print(s.model()) quit()
One should expect some results like:
>>> print(s.check()) sat >>> print(s.model()) [y = 4, x = 2]
This example asks for a satisfying assignment to the problem:
The instructions above explain how to install Z3 in the user's home directory.
Another option is to install Z3 in a machine-wide location. The following instructions worked on at least two Mac machines:
sudo mv <dir> /usr/local/The
cd /usr/local/<dir> python scripts/mk_make.py --pythonNote that no
cd build makeThis may take a while to complete.
sudo make installThe
To make sure ACL2's build system can find Z3, Z3 should be installed in one's path. There are two ways to achieve this:
export PATH=/path to z3 executable/:$PATH
#!/bin/bash /path to z3 executable/z3 "$@"In some systems, after creating that script, one needs to run ``rehash'' in the shell.