Z3 API in Python
Z3 is a high performance theorem prover developed at Microsoft Research. Z3 is used in many applications such as: software/hardware verification and testing, constraint solving, analysis of hybrid systems, security, biology (in silico analysis), and geometrical problems.
This tutorial demonstrates the main capabilities of Z3Py: the Z3 API in Python. No Python background is needed to read this tutorial. However, it is useful to learn Python (a fun language!) at some point, and there are many excellent free resources for doing so (Python Tutorial).
The Z3 distribution also contains the C, .Net and OCaml APIs. The source code of Z3Py is available in the Z3 distribution, feel free to modify it to meet your needs. The source code also demonstrates how to use new features in Z3 4.0. Other cool front-ends for Z3 include Scala^Z3 and SBV.
Please send feedback, comments and/or corrections to [email protected]. Your comments are very valuable.
Getting Started
Let us start with the following simple example:
x = Int ( 'x' ) y = Int ( 'y' ) solve ( x > 2 , y < 10 , x + 2 * y == 7 )
The function Int('x') creates an integer variable in Z3 named x . The solve function solves a system of constraints. The example above uses two variables x and y , and three constraints. Z3Py like Python uses = for assignment. The operators < , <= , > , >= , == and != for comparison. In the example above, the expression x + 2*y == 7 is a Z3 constraint. Z3 can solve and crunch formulas.
The next examples show how to use the Z3 formula/expression simplifier.
... continue reading