Exercism Z3 Track

Z3

Z3 is a theorem prover from Microsoft Research. It is licensed under the MIT license.

Pre-built binaries for stable and nightly releases are available from here..

Z3 should be built using Visual Studio with Python bindings for these exercises.

License

This repository uses the MIT License.

Installing Z3

Download Python (if not already installed)

The latest version of Python can be downloaded from here.

• When installing, please be sure to select the box that adds Python to PATH

Download Visual Studio (if not already installed)

The latest version of Visual Studio can be downloaded from here.

• When installing, please select the Python Development workload
• Select all optional Python development package check boxes on right hand side

After installation, open Visual Studio and set up you initial preferences.

Install Git commands

Git install instructions can be found here.

• You will need to add Git your system variables

Clone Z3

Navigate to the Z3 Github repository to view the project.

Open a terminal on your computer and navigate to where you want to clone the Z3 repository (Ex: C:\Z3).

From that location, run:

git clone https://github.com/z3Prover/z3.git

Building Z3 on Windows using Visual Studio Command Prompt

Open Developer Command Prompt for VS 2019 through the start menu.

Navigate to the folder that you cloned the Z3 repository into (Ex: C:\Z3).

For 32-bit builds, run:

python scripts/mk_make.py

For a 64-bit build, run:

python scripts/mk_make.py -x

then run:

cd build
pip install z3-solver

You should now be able to open Visual Studio and run Z3 with its Python binding.

To test, you can run:

from x3 import *
x = Real('x')
y = Real('y)
s = Solver()
s.add(x + y > 5, x > 1, y > 1)
print(s.check())
print(s.model())

The last two lines should produce sat and [y = 4, x = 2].