Z3: An Efficient SMT Solver for Constraints Solving Problems

Author: **Yongfeng Gu**, Date: **May, 2020**

** Z3** is an efficient solver of the SMT problem (Satisfiability Modulo Theories). Compared with the SAT solver, Z3 can resolve not only the

In this tutorial, we implemented the Z3 solver by using a widely-used and open-source python library, namely Z3Prover/z3. Detailed documentation is at http://theory.stanford.edu/~nikolaj/programmingz3.html.

Installing the Z3 library is quite easy, just typing only one command-line (if you have already installed Anaconda environment, then skip this step).

```
$> pip install z3-solver
```

Here's a simple usage of Z3 solver for solving the **Boolean** formulas. We use the function `Bool()`

to declare the Boolean variable (or use `Bools()`

to declare a series of Boolean vairables). We then declear a solver object `s=Slover()`

and use the function `s.check()`

to solve the constraints added by the function `s.add()`

. Finally, the result is returned by the function `s.model()`

.

Note that **a solution of the given constraints is called a model** in Z3, so the function `s.model()` presents a possible solution of SMT problem.

In [139]:

```
from z3 import *
a = Bool('a') # boolean variables
b = Bool('b')
c = Bool('c')
# a,b,c = Bools('a b c') # another way to declear the boolean variables
s = Solver() # z3 solver
s.add(a,
Or(Not(b),a),
Or(Not(c),a),
Or(Not(a),b,c),
Or(Not(b),Not(c))
) # constraints
s.check()
print(s.model()) # solution
```

The `add()`

function is used to include Boolean constraints consistening with 5 common operators, i.e., **Or, And, Not, Implies, ==**. For example, the constraints $(\neg b \vee a) \wedge (\neg c \rightarrow a) \wedge (a \leftrightarrow c)$ can be rewritten in Z3 as follows,

In [130]:

```
s = Solver()
s.add(Or(Not(b),a), # !b || a
Implies(Not(c),a), # !c -> a
a == c, # a <-> c
)
```

The `check()`

function is used to check the satisfiability of given constraints, that is, if some solutions are found, then `check() == sat`

, otherwise, `check() == unsat`

. This function is the satisfiability flag of Z3 solver. Besides, `check()`

function can receive assumptions, e.g., by adding a assumption `c=True`

, we can obtain another result of `b = False, a = True, c = True`

, which is different with the first solution (`a = True, b = True, c = False`

).

In [141]:

```
s.check(c) # c==True
print(s.model())
```

The `simplify()`

function is used to simplify the constraint expressions，e.g., it automatedly transforms the `x + y + 2*x + 3`

into the `3+x*x+y`

by adding the variables `x`

and `y`

together, respectively.

In [142]:

```
x = Int('x')
y = Int('y')
print('Original :', x + y + 2*x + 3)
print('Simplified:', simplify(x + y + 2*x + 3))
```

Here's a simple usage of Z3 solver for solving the **numeric** formulas. We use the function `Int()`

to declare the Integer variable (or use `Ints()`

to declare a series of Integer vairables).

Note that `s.sexpr()`

function, this function is used to present the intermediate formulas (i.e., S-expression) of math expression in Z3 solver.

In [126]:

```
from z3 import *
x = Int('x') # declear the int variables
y = Int('y')
# x, y = Ints('x y') # another way to declear the int variables
s = Solver() # z3 solver
s.add((x % 4) + 3 * (y / 2) > x - y) # constraints
print(s.sexpr()) # intermediate formula in Z3
s.check()
print(s.model())
```

The `set_option()`

function sets the parameters of Z3 solver, such as `precision=30`

which means the results are accurated to the **30** decimal places.

In [83]:

```
p, q, r = Reals('p q r')
solve(p**2 + q**2 == 3, p**3 == 2)
set_option(precision=30) # params in Z3
solve(p**2 + q**2 == 3, p**3 == 2)
```

The `assertions()`

function is used to enumerate all the assertions (clauses) in solver `s`

. On the other hand, `statistics()`

function is used to show the performance statistics of `check()`

function, including the memory consumption, allocations, etc.

In [147]:

```
x = Real('x')
y = Real('y')
s = Solver()
s.add(x > 1, y > 1, Or(x + y > 3, x - y < 2))
print("asserted constraints...")
for c in s.assertions():
print(c)
print('parameters in check():')
print(s.statistics())
```

The `model()`

function returns one valid solution solved by Z3 solver. After geting the object `m`

(`m=model()`

), we can obtain the detailed information of each variable in the solution.

**Variable names**.`m.decls()`

collects the declarations of all variables, including their names.**Variable assignmants**.`m[x]`

gets the assignment of`x`

according to the solved solution. Similarily,`m[z]`

gets the assignment of`z`

.

In [143]:

```
x, y, z = Reals('x y z')
s = Solver()
s.add(y > 1, z - x < 10, x > 1, x + y > 3)
s.check()
print('Solution:', s.model())
print(">> Get all variable's name")
print(m.decls())
print(">> Get all variable's assignment")
m = s.model()
print([m[name] for name in m.decls()])
```

Besides solving the boolean and numeric types of formulas, Z3 also provided the solution on **Bit-vector** type of formulas. Specifically, the function `BitVec()`

can be used to creates a bit-vector variable in Z3, e.g., `BitVec('x', 16)`

means a 16-bit vector variable named **x**.

Note that each Bit-vector is resented as a hexadeciaml format string. E.g., a **16-bits** vector variable is presented as **#x0000** and a **32-bits** vector variable is presented as **#x00000000**.

In [145]:

```
x = BitVec('x', 16)
y = BitVec('y', 32)
print('x:',(x+0).sexpr())
# Internal representation
print('y:',(y+0).sexpr())
```

The `BitVecVal()`

function enables uers to initialize a Bit-vector variable with a certain value, e.g., `BitVecVal(-2, 16)`

denotes a **16-bits** vector variable whose value equals **-2**. Since the Bit-vector is expressed as the signed variable (1st bit is singed-bit), in this case, **-2** is presented as **#xFFFe**.

In [162]:

```
xs = BitVecVal(-2,16)
print('xs:',xs.sexpr())
```

Besides, the Bit-vector variable supports the bit-wise operators, including `|`

(or), `&`

(and), `~`

(not), as well as numeric operators, including `+`

, `-`

, etc.

In [182]:

```
x, y = BitVecs('x y', 16)
s = Solver()
s.add(x & y == ~y)
# s.add(x + y == 2, x > 0, y > 0)
s.check()
m = s.model()
print('x:',m[x].sexpr(), 'y:',m[y].sexpr())
```

An exciting capability of Z3 solver is that it can solve the **un-interpreted functions**. In Z3, all functions are un-interpreted before solving, which means that we do not need to know the internal structure of functions beforehand. Given some constraints about the function, Z3 is able to guess its implementation.

Here's the example of guessing the function `f`

with constraints.

In [193]:

```
x = Int('x')
y = Int('y')
f = Function('f', IntSort(), IntSort()) # function f
s = Solver()
s.add(f(f(x)) == x, f(x) == y, x != y)
s.check()
m = s.model()
print(m)
```

According to the result, the above solution of function `f`

is solved as the Step Function,

In [7]:

```
from z3 import *
x, y, z = Ints('x y z')
int_solver = Then('simplify',
'solve-eqs',
'bit-blast',
'sat').solver() # declare a cumstomized solver by `Then()`
int_solver.add(x+y+z == 5, x == -y, y >= z)
int_solver.check()
print(int_solver.model())
```

In [12]:

```
int_solver2 = Then(With('simplify', mul2concat=True),
'solve-eqs',
'bit-blast',
'sat').solver()
int_solver2.add(x+y+z == 5, x == -y, y >= z)
int_solver2.check()
print(int_solver2.model())
```

Besides, the `Tactic()`

function can also be used to parameterize the solver.

In [15]:

```
x, y, z = Ints('x y z')
int_solver3 = Tactic('smt').solver()
int_solver3.add(x+y+z == 5, x == -y, y >= z)
int_solver3.check()
print(int_solver3.model())
```

Probes (aka. formula measures) are used to calculate the measures (e.g., number of vairables) of the formulas. We use the function `Probe()`

with a given parameters to capture such measures. Here's an example of calculate the number of constants (or variables) in the formulas.

In [27]:

```
x, y, z = Reals('x y z')
a = Int('a')
g = Goal()
g.add(x + y + z > 0, a>0)
p = Probe('num-consts')
print("num-constants:", p(g))
```

In the above example, `Goal()`

defines a set of constraints (or assertions) to be solved. A **Goal** object can also use `add()`

function to add constraints. We can easily solve the constraints defined in `Goal()`

by using a **Solver** object.

In [25]:

```
s = Solver()
s.add(g) # add the constraints of the Goal object
s.check()
print(s.model())
```

Besides the `num-constants`

used in the `Probe()`

, there are a lot of measures can be captured and all their informtion can be returned by the function `describe_probes()`

.

In [30]:

```
describe_probes()
```