		Search-engine friendly clone of the ACL2 documentation.

Smtlink

Z3-installation

How to install Z3

How I installed 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 Z3 version 4.5.0 - 64 bit, and the version of Python I used is Python 2.7.15.

Download the current stable release from Z3 releases
We want to download the source code and compile it by ourselves. It might be doable to use the binary releases by setting up PYTHONPATH and DYLD_LIBRARY_PATH (on macos), but I haven't tried it and there's no instruction in Z3 telling us if that's the way to use it.
Assume we are in the release directory, do:
```
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 $HOME/usr directory prefix, but you can replace that part of the path with your conventional path. Note that Z3 restricts --prefix to be the prefix of --pypkgdir. Also, $HOME/usr does not need to exist in order to follow these steps; that directory and subdirectories will be created as necessary.
Now make the C/C++ libraries, do:
```
cd build; make
```
Now do the installation in places specified in --prefix:
```
make install
```
Now if one takes a look at $HOME/usr, one will see in $HOME/usr/bin, we have the z3 executable, in $HOME/usr/include we have all the z3 C++ header files, in $HOME/usr/lib we have libz3.dylib and in $HOME/usr/lib/python-2.7/site-packages we have all the z3 Python API files.

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

So the last step is to add this path to PYTHONPATH. Adding this path to existing PYTHONPATH:

export PYTHONPATH=$HOME/usr/lib/python-2.7/site-packages:$PYTHONPATH

If PYTHONPATH is undefined, do:

export PYTHONPATH=$HOME/usr/lib/python-2.7/site-packages
@

Now one should be able to import z3 into Python. Run Python, which will put you in an interactive loop.
```
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: x + y > 5, x > 1 and y > 1. It should be easy to check the result.

Additional Notes

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:

Download the latest stable release of Z3 as explained in the instructions above. Unzip it: let <dir> be the name of the resulting directory.
Move the directory to a machine-wide location, e.g.:
```
sudo mv <dir> /usr/local/
```
The sudo is needed because /usr/local is typically owned by root, and it is not good practice to change the ownership of /usr/local to a non-root user. There is no need to change the ownership of /usr/local/<dir> to root.
Prepare to build Z3 with the Python bindings:
```
cd /usr/local/<dir>
python scripts/mk_make.py --python
```
Note that no --prefix or --pypkgdir options are used here, unlike the instructions given above. This may give a warning related to Z3's restriction, mentioned in the instructions above, that --prefix must be a prefix of --pypkgdir; despite this warning, things worked on at least two Mac machines. On Mac, ensuring that this restriction is satisfied is tricky because Python packages are normally installed in places like /Library/Frameworks/Python.framework/Versions/3.6/... or /System/Library/Frameworks/Python.framework/Versions/2.7/..., but prefixes of these locations normally do not hold the bin, lib, and include directories that the Z3 installation creates (see below).
Build Z3:
```
cd build
make
```
This may take a while to complete.
Install Z3:
```
sudo make install
```
The sudo is needed because this will write into /usr/local/bin, /usr/local/lib, and /usr/local/include, which are typically owned by root (see comments above about this).
Run the Z3 example in Python described in the instructions above, to confirm that the installation was successful.

Allow the Build System to Find Z3

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:

Add the path to where Z3 is installed into one's path. For example,
```
export PATH=/path to z3 executable/:$PATH
```
Another way of achieving this purpose is to create the following bash script called ``z3'' and put it in one's path:
```
#!/bin/bash
/path to z3 executable/z3 "$@"
```
In some systems, after creating that script, one needs to run ``rehash'' in the shell.