Z3: An Efficient SMT Solver for Constraints Solving Problems

Author: Yongfeng Gu, Date: May, 2020

0. Basic Introductions

Z3 is an efficient solver of the SMT problem (Satisfiability Modulo Theories). Compared with the SAT solver, Z3 can resolve not only the boolean formulas (e.g., $a \vee b = True$) but also the non-boolean formulas (e.g., $a^2-b<0$) in the constraint solving problems. What's more, Z3 also shows a more efficient and effective solving ability than SAT solvers. For example, Z3 can quickly (in seconds) solve a large SMT problem with thousands of variables and constraints.

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

1. Solving the Boolean constraints

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
[a = True, b = True, c = False]

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())
[b = False, a = True, c = True]

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))
Original  : x + y + 2*x + 3
Simplified: 3 + 3*x + y

2. Solving the Numeric constraints

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())
(declare-fun y () Int)
(declare-fun x () Int)
(assert (> (+ (mod x 4) (* 3 (div y 2))) (- x y)))

[y = 10, x = 20]

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)
[p = 1.2599210498?, q = -1.1885280594?]
[p = 1.259921049894873164767210607278?,
 q = -1.188528059421316533710369365015?]

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())
asserted constraints...
x > 1
y > 1
Or(x + y > 3, x - y < 2)
parameters in check():
(:max-memory   11.57
 :memory       5.86
 :mk-bool-var  1
 :num-allocs   431071701564.00
 :rlimit-count 103874)

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()])
Solution: [z = 0, y = 2, x = 3/2]
>> Get all variable's name
[z, y, x]
>> Get all variable's assignment
[0, 2, 3/2]

3. Solving the Bit-vector constraints

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())
x: (bvadd x #x0000)
y: (bvadd y #x00000000)

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())
xs: #xfffe

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())
x: #x0000 y: #xffff

4. Solving the Functions

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)
[x = 0, y = 1, f = [1 -> 0, else -> 1]]

According to the result, the above solution of function f is solved as the Step Function,

$$ f(x) \begin{cases}0, \ \ \mbox{if} \ x = 1 \\ 1, \ \ \mbox{if} \ x = 0 \end{cases} $$

5. Others

5.1 Tunning the Solver

In previous section, we simply call the Slover() function to instaniate a z3 solver, however, there are many key parameters can be set in this solver. In practice, we can tweak the possible values of such parameters using Then() and With() functions.

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())
[z = 5, y = 0, x = 0]
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())
[z = 5, y = 0, x = 0]

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())
[z = 5, y = 5, x = -5]

5.2 Probes

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))
num-constants: 10.0

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())
[a = 1, y = 0, z = 0, x = 1]

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()
ackr-bound-probe : A probe to give an upper bound of Ackermann congruence lemmas that a formula might generate.
is-unbounded : true if the goal contains integer/real constants that do not have lower/upper bounds.
is-pb : true if the goal is a pseudo-boolean problem.
arith-max-deg : max polynomial total degree of an arithmetic atom.
arith-avg-deg : avg polynomial total degree of an arithmetic atom.
arith-max-bw : max coefficient bit width.
arith-avg-bw : avg coefficient bit width.
is-qflia : true if the goal is in QF_LIA.
is-qfauflia : true if the goal is in QF_AUFLIA.
is-qflra : true if the goal is in QF_LRA.
is-qflira : true if the goal is in QF_LIRA.
is-ilp : true if the goal is ILP.
is-qfnia : true if the goal is in QF_NIA (quantifier-free nonlinear integer arithmetic).
is-qfnra : true if the goal is in QF_NRA (quantifier-free nonlinear real arithmetic).
is-nia : true if the goal is in NIA (nonlinear integer arithmetic, formula may have quantifiers).
is-nra : true if the goal is in NRA (nonlinear real arithmetic, formula may have quantifiers).
is-nira : true if the goal is in NIRA (nonlinear integer and real arithmetic, formula may have quantifiers).
is-lia : true if the goal is in LIA (linear integer arithmetic, formula may have quantifiers).
is-lra : true if the goal is in LRA (linear real arithmetic, formula may have quantifiers).
is-lira : true if the goal is in LIRA (linear integer and real arithmetic, formula may have quantifiers).
is-qfufnra : true if the goal is QF_UFNRA (quantifier-free nonlinear real arithmetic with other theories).
is-qfbv-eq : true if the goal is in a fragment of QF_BV which uses only =, extract, concat.
is-qffp : true if the goal is in QF_FP (floats).
is-qffpbv : true if the goal is in QF_FPBV (floats+bit-vectors).
is-qffplra : true if the goal is in QF_FPLRA.
memory : amount of used memory in megabytes.
depth : depth of the input goal.
size : number of assertions in the given goal.
num-exprs : number of expressions/terms in the given goal.
num-consts : number of non Boolean constants in the given goal.
num-bool-consts : number of Boolean constants in the given goal.
num-arith-consts : number of arithmetic constants in the given goal.
num-bv-consts : number of bit-vector constants in the given goal.
produce-proofs : true if proof generation is enabled for the given goal.
produce-model : true if model generation is enabled for the given goal.
produce-unsat-cores : true if unsat-core generation is enabled for the given goal.
has-quantifiers : true if the goal contains quantifiers.
has-patterns : true if the goal contains quantifiers with patterns.
is-propositional : true if the goal is in propositional logic.
is-qfbv : true if the goal is in QF_BV.
is-qfaufbv : true if the goal is in QF_AUFBV.
is-quasi-pb : true if the goal is quasi-pb.