Installing Z3 Theorem Prover on MacOS
Z3 Theorem Prover is one of the most-used satisfiability modulo theories (SMT) solver. Provided by Microsoft, it’s source can be found in Github.
The rise4fun site provides an online interface on which we can use the z3 solver right away without any prerequisites.
For simple projects and codes, working through the site might be enough, but when working on large projects or when offline uses are needed, building and installing it on a computer might be necessary.
When trying to build/install, the README file provided might be confusing (it was for me). And for those people, here is a simplified version on how to build and install the Z3 theorem prover on MacOS.
In this article, Z3 prover is built/installed in such a way that C, C++, Python APIs are provided.
1. Build using make and GCC/Clang
git clone https://github.com/Z3Prover/z3.git
cd z3python3 scripts/mk_make.py --python
cd build
make
sudo make install
2. Install the Python wrapper
pip3 install z3-solver3. Check if installed correctly
To check whether or not everything went smoothly, execute an example python code provided in the examples/python directory
python3 examples/python/example.pyAfter checking there are no errors on executing the example.py (and there shouldn’t be any), it’s good to go and you can start using the Z3 Theorem Prover!
(Any comments or constructive criticisms are always welcome!)
