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 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
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.
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,
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).
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.
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.
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.
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.
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.
m.decls() collects the declarations of all variables, including their names.m[x] gets the assignment of x according to the solved solution. Similarily, m[z] gets the assignment of z.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**.
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.
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.
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.
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,
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())
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.
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.
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.
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().
describe_probes()