# Z3 API in Python

This tutorial demonstrates the main capabilities of Z3Py: the Z3 API in Python. There are many benefits to using, Z3Py. First, it is much more familiar to individuals who have seen programming languages before, but have never seen functional languages like Z3.

No Python background is needed to read and following along with this tutorial. However, it is useful to learn Python (a fun language!) at some point for other purposes. There are many excellent free resources for doing so Python Tutorial.

The Z3 distribution also contains the **C**, **C++**, **.Net**, **Java**, **Julia**, **JS** and **OCaml** APIs.
The source code of Z3Py is available in the Z3 distribution, feel free to modify it to meet your needs.

In the present form this tutorial is static. You can run the examples locally by copying the text into a python interpreter where you have imported z3.

### Using Z3Py Locally

The Python bindings are available from pypi. You can install them using the following command:

` pip install z3-solver`

## Getting Started

Let us start with the following simple example:

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:

x must be greater than 2 y must be less than 10 when x is added to twice the value of y, it must equal 7

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.

By default, Z3Py (for the web) displays formulas and expressions using mathematical notation.
As usual, $\wedge$ is the logical and, $\vee$ is the logical or, and so on.
The command `set_option(html_mode=False)`

makes all formulas and expressions to be
displayed in Z3Py notation. This is also the default mode for the offline version of Z3Py that
comes with the Z3 distribution.

Z3 provides functions for traversing expressions.

Z3 provides all basic mathematical operations. Z3Py uses the same operator precedence of the Python language.
Like Python, `**`

is the power operator. Z3 can solve nonlinear *polynomial* constraints.

The procedure `Real('x')`

creates the real variable `x`

.
Z3Py can represent arbitrarily large integers, rational numbers (like in the example above),
and irrational algebraic numbers. An irrational algebraic number is a root of a polynomial with integer coefficients.
Internally, Z3 represents all these numbers precisely.
Irrational numbers are displayed in decimal notation for making it easy to read the results.

The procedure `set_option`

is used to configure the Z3 environment. It is used to set global configuration options
such as how the result is displayed. The option `set_option(precision=30)`

sets the number of decimal places used when displaying results.
The `?`

mark in `1.2599210498?`

indicates the output is truncated.

The following example demonstrates a common mistake. The expression `3/2`

is a Python integer and not a Z3 rational number.
The example also shows different ways to create rational numbers in Z3Py. The procedure `Q(num, den)`

creates a
Z3 rational where `num`

is the numerator and `den`

is the denominator. The `RealVal(1)`

creates a Z3 real number
representing the number `1`

.

Rational numbers can also be displayed in decimal notation.

A system of constraints may not have a solution. In this case, we say the system is **unsatisfiable**.

Like in Python, comments begin with the hash character `#`

and are terminated by the end of line.
Z3Py does not support comments that span more than one line.

## Boolean Logic

Z3 supports Boolean operators: `And`

, `Or`

, `Not`

, `Implies`

(implication),
`If`

(if-then-else). Bi-implications are represented using equality `==`

.
The following example shows how to solve a simple set of Boolean constraints.

The Python Boolean constants `True`

and `False`

can be used to build Z3 Boolean expressions.

The following example uses a combination of polynomial and Boolean constraints.

## Solvers

Z3 provides different solvers. The command `solve`

, used in the previous examples, is implemented using the Z3 solver API.
The implementation can be found in the file `z3.py`

in the Z3 distribution.
The following example demonstrates the basic Solver API.

The command `Solver()`

creates a general purpose solver. Constraints can be added using the method `add`

.
We say the constraints have been **asserted** in the solver. The method `check()`

solves the asserted constraints.
The result is `sat`

(satisfiable) if a solution was found. The result is `unsat`

(unsatisfiable) if
no solution exists. We may also say the system of asserted constraints is **infeasible**. Finally, a solver may fail
to solve a system of constraints and `unknown`

is returned.

In some applications, we want to explore several similar problems that share several constraints.
We can use the commands `push`

and `pop`

for doing that.
Each solver maintains a stack of assertions. The command `push`

creates a new scope by
saving the current stack size.
The command `pop`

removes any assertion performed between it and the matching `push`

.
The `check`

method always operates on the content of solver assertion stack.

The following example shows an example that Z3 cannot solve. The solver returns `unknown`

in this case.
Recall that Z3 can solve nonlinear polynomial constraints, but `2**x`

is not a polynomial.

The following example shows how to traverse the constraints asserted into a solver, and how to collect performance statistics for
the `check`

method.

The command `check`

returns `sat`

when Z3 finds a solution for the set of asserted constraints.
We say Z3 **satisfied** the set of constraints. We say the solution is a **model** for the set of asserted
constraints. A model is an **interpretation** that makes each asserted constraint **true**.
The following example shows the basic methods for inspecting models.

In the example above, the function `Reals('x y z')`

creates the variables. `x`

, `y`

and `z`

.
It is shorthand for:

The expression `m[x]`

returns the interpretation of `x`

in the model `m`

.
The expression `"%s = %s" % (d.name(), m[d])`

returns a string where the first `%s`

is replaced with
the name of `d`

(i.e., `d.name()`

), and the second `%s`

with a textual representation of the
interpretation of `d`

(i.e., `m[d]`

). Z3Py automatically converts Z3 objects into a textual representation
when needed.

## Arithmetic

Z3 supports real and integer variables. They can be mixed in a single problem. Like most programming languages, Z3Py will automatically add coercions converting integer expressions to real ones when needed. The following example demonstrates different ways to declare integer and real variables.

The function `ToReal`

casts an integer expression into a real expression.

Z3Py supports all basic arithmetic operations.

The command `simplify`

applies simple transformations on Z3 expressions.

The command `help_simplify()`

prints all available options.
Z3Py allows users to write option in two styles. The Z3 internal option names start with `:`

and words are separated by `-`

.
These options can be used in Z3Py. Z3Py also supports Python-like names,
where `:`

is suppressed and `-`

is replaced with `_`

.
The following example demonstrates how to use both styles.

Z3Py supports arbitrarily large numbers. The following example demonstrates how to perform basic arithmetic using larger integer, rational and irrational numbers.
Z3Py only supports algebraic irrational numbers. Algebraic irrational numbers are sufficient for presenting the solutions of systems of polynomial constraints.
Z3Py will always display irrational numbers in decimal notation since it is more convenient to read. The internal representation can be extracted using the method `sexpr()`

.
It displays Z3 internal representation for mathematical formulas and expressions in s-expression (Lisp-like) notation.

## Machine Arithmetic

Modern CPUs and main-stream programming languages use
arithmetic over fixed-size bit-vectors.
Machine arithmetic is available in Z3Py as *Bit-Vectors*.
They implement the
precise semantics of unsigned and of
signed two-complements arithmetic.

The following example demonstrates how to create bit-vector variables and constants.
The function `BitVec('x', 16)`

creates a bit-vector variable in Z3 named `x`

with `16`

bits.
For convenience, integer constants can be used to create bit-vector expressions in Z3Py.
The function `BitVecVal(10, 32)`

creates a bit-vector of size `32`

containing the value `10`

.

In contrast to programming languages, such as C, C++, C#, Java,
there is no distinction between signed and unsigned bit-vectors
as numbers. Instead, Z3 provides special signed versions of arithmetical operations
where it makes a difference whether the bit-vector is treated as signed or unsigned.
In Z3Py, the operators
`<`

, `<=`

, `>`

, `>=`

, `/`

, `%`

and `>>;`

correspond to the signed versions.
The corresponding unsigned operators are
`ULT`

, `ULE`

, `UGT`

, `UGE`

, `UDiv`

, `URem`

and `LShR`

.

The operator `>>`

is the arithmetic shift right, and
`<<`

is the shift left. The logical shift right is the operator `LShR`

.

## Functions

Unlike programming languages, where functions have side-effects, can throw exceptions,
or never return, functions in Z3 have no side-effects and are **total**.
That is, they are defined on all input values. This includes functions, such
as division. Z3 is based on first-order logic.

Given a constraints such as `x + y > 3`

, we have been saying that `x`

and `y`

are variables. In many textbooks, `x`

and `y`

are called uninterpreted constants.
That is, they allow any interpretation that is consistent with the constraint `x + y > 3`

.

More precisely, function and constant symbols in pure first-order logic are *uninterpreted* or *free*,
which means that no a priori interpretation is attached.
This is in contrast to functions belonging to the signature of theories,
such as arithmetic where the function `+`

has a fixed standard interpretation
(it adds two numbers). Uninterpreted functions and constants are maximally flexible;
they allow any interpretation that is consistent with the constraints over the function or constant.

To illustrate uninterpreted functions and constants let us the uninterpreted integer constants (aka variables)
`x`

, `y`

. Finally let `f`

be an uninterpreted function that takes one argument of type (aka sort) integer
and results in an integer value.
The example illustrates how one can force an interpretation where `f`

applied twice to `x`

results in `x`

again, but `f`

applied once to `x`

is different from `x`

.

The solution (interpretation) for `f`

should be read as `f(0)`

is `1`

, `f(1)`

is `0`

, and `f(a)`

is `1`

for all `a`

different from `0`

and `1`

.

In Z3, we can also evaluate expressions in the model for a system of constraints. The following example shows how to
use the `evaluate`

method.

## Satisfiability and Validity

A formula/constraint `F`

is **valid** if `F`

always evaluates to true for any assignment of appropriate values to its
uninterpreted symbols.
A formula/constraint `F`

is **satisfiable** if there is some assignment of appropriate values
to its uninterpreted symbols under which `F`

evaluates to true.
Validity is about finding a proof of a statement; satisfiability is about finding a solution to a set of constraints.
Consider a formula `F`

containing `a`

and `b`

.
We can ask whether `F`

is valid, that is whether it is always true for any combination of values for
`a`

and `b`

. If `F`

is always
true, then `Not(F)`

is always false, and then `Not(F)`

will not have any satisfying assignment (i.e., solution); that is,
`Not(F)`

is unsatisfiable. That is,
`F`

is valid precisely when `Not(F)`

is not satisfiable (is unsatisfiable).
Alternately,
`F`

is satisfiable if and only if `Not(F)`

is not valid (is invalid).
The following example proves the deMorgan's law.

The following example redefines the Z3Py function `prove`

that receives a formula as a parameter.
This function creates a solver, adds/asserts the negation of the formula, and check if the negation is unsatisfiable.
The implementation of this function is a simpler version of the Z3Py command `prove`

.

## List Comprehensions

Python supports list comprehensions List comprehensions provide a concise way to create lists. They can be used to create Z3 expressions and problems in Z3Py. The following example demonstrates how to use Python list comprehensions in Z3Py.

In the example above, the expression `"x%s" % i`

returns a string where `%s`

is replaced with the value of `i`

.

The command `pp`

is similar to `print`

, but it uses Z3Py formatter for lists and tuples instead of Python's formatter.

Z3Py also provides functions for creating vectors of Boolean, Integer and Real variables. These functions are implemented using list comprehensions.

## Kinematic Equations

In high school, students learn the kinematic equations.
These equations describe the mathematical relationship between **displacement** (`d`

),
**time** (`t`

), **acceleration** (`a`

), **initial velocity** (`v_i`

) and **final velocity** (`v_f`

).
In Z3Py notation, we can write these equations as:

` d == v_i * t + (a*t**2)/2,`

v_f == v_i + a*t

### Problem 1

Ima Hurryin is approaching a stoplight moving with a velocity of `30.0`

m/s.
The light turns yellow, and Ima applies the brakes and skids to a stop.
If Ima's acceleration is `-8.00`

m/s^{2}, then determine the displacement of the
car during the skidding process.

### Problem 2

Ben Rushin is waiting at a stoplight. When it finally turns green, Ben accelerated from rest at a rate of
a `6.00`

m/s^{2} for a time of `4.10`

seconds. Determine the displacement of Ben's car during this time period.

## Bit Tricks

Some low level hacks are very popular with C programmers. We use some of these hacks in the Z3 implementation.

### Power of two

This hack is frequently used in C programs (Z3 included) to test whether a machine integer is a power of two.
We can use Z3 to prove it really works. The claim is that `x != 0 && !(x & (x - 1))`

is true if and only if `x`

is a power of two.

### Opposite signs

The following simple hack can be used to test whether two machine integers have opposite signs.

## Puzzles

### Dog, Cat and Mouse

Consider the following puzzle. Spend exactly 100 dollars and buy exactly 100 animals. Dogs cost 15 dollars, cats cost 1 dollar, and mice cost 25 cents each. You have to buy at least one of each. How many of each should you buy?

### Sudoku

Sudoku is a very popular puzzle.
The goal is to insert the numbers in the boxes to satisfy only one condition: each row, column and
`3x3`

box must contain the digits `1`

through `9`

exactly once.

The following example encodes the suduko problem in Z3. Different sukudo instances can be solved
by modifying the matrix `instance`

. This example makes heavy use of
list comprehensions
available in the Python programming language.

### Eight Queens

The eight queens puzzle is the problem of placing eight chess queens on an 8x8 chessboard so that no two queens attack each other. Thus, a solution requires that no two queens share the same row, column, or diagonal.

## Application: Install Problem

The **install problem** consists of determining whether a new set of packages can be installed in a system.
This application is based on the article
OPIUM: Optimal Package Install/Uninstall Manager.
Many packages depend on other packages to provide some functionality.
Each distribution contains a meta-data file that
explicates the requirements of each package of the distribution
The meta-data contains details like the name, version, etc. More importantly, it contains
**depends** and **conflicts**
clauses that stipulate which other packages should be on the
system. The depends clauses stipulate which other packages must be present.
The conflicts clauses stipulate which other packages must not be present.

The install problem can be easily solved using Z3. The idea is to define a Boolean variable for each
package. This variable is true if the package must be in the system. If package `a`

depends on
packages `b`

, `c`

and `z`

, we write:

`DependsOn`

is a simple Python function that creates Z3 constraints that capture the
depends clause semantics.

Thus, `DependsOn(a, [b, c, z])`

generates the constraint

`And(Implies(a, b), Implies(a, c), Implies(a, z))`

That is, if users install package `a`

, they must also install packages
`b`

, `c`

and `z`

.

If package `d`

conflicts with package `e`

, we write `Conflict(d, e)`

.
`Conflict`

is also a simple Python function.

`def Conflict(p1, p2):`

return Or(Not(p1), Not(p2))

`Conflict(d, e)`

generates the constraint `Or(Not(d), Not(e))`

.
With these two functions, we can easily encode the example in the
Opium article (Section 2) in Z3Py as:

Note that the example contains the constraint

`DependsOn(c, [Or(d, e), Or(f, g)]),`

The meaning is: to install `c`

, we must install `d`

or `e`

, and `f`

or `g`

Now, we refine the previous example. First, we modify `DependsOn`

to allow
us to write `DependsOn(b, d)`

instead of `DependsOn(b, [d])`

. We also
write a function `install_check`

that returns a list of packages that must be installed
in the system. The function `Conflict`

is also modified. It can now receive multiple
arguments.