SMT-solver

Z3 is a SMT(Satisfiability Modulo Theories) solver developed by Microsoft.

Simple example №1:

Task condition:

x + y = 10
x * y = 21

Solution:

from z3 import *
x = Int('x')
y = Int('y')
s = Solver()
s.add(x+y==10, x*y==21)
print(s.check()) # sat -> Satisfiable
print(s.model()) # [x = 7, y = 3]

The call to s.check() produces a verdict sat; there is a satisfying assignment for the formulas. A satisfying model, where Tie is false and Shirt is true, can be extracted using s.model(). For convenience the Python front-end to Z3 contains some shorthand functions. The function solve sets up a solver, adds assertions, checks satisfiability, and prints a model if one is available.

Simple example №2:

Task condition:

Find all the positive integer solutions of the equation
x² + y² + z² = x * y * z, where
x, y, z -> integer
1 ≤ x ≤ y ≤ z ≤ 100 

Solution:

from z3 import *
x = Int('x')
y = Int('y')
z = Int('z')
s = Solver()
solutions = []
s.add((x**2+y**2+z**2) == (x*y*z))
s.add(1<=x, x<=y, y<=z, z<=100)

while s.check() == sat:
    m = s.model()
    solution = (m[x].as_long(), m[y].as_long(), m[z].as_long()) # Return a Z3 integer numeral as a Python long (bignum) numeral.
    solutions.append(solution)

    s.add(Not(And(x==m[x], y==m[y], z==m[z]))) # Restrictions are accumulating

print(*solutions) # (3, 3, 6) (3, 3, 3) (6, 15, 87) (3, 6, 15) (3, 15, 39)

Simple example №3:

Task condition:

You have intercepted 6 numbers generated by LCG(Linear Congruential Generator):

X0 = 0 
X1 = 3
X2 = 66
X3 = 89
X4 = 72
X5 = 15
x6 = ?

All numbers are 16-bit.

Solution:

LCG: X_n+1 = (aX_n + c) mod m

from z3 import *
X = [0, 3, 66, 89, 72, 15]

a = Int('a')
c = Int('c')
m = Int('m')

s = Solver()

s.add(m>0, m<65536)
s.add(0<a, a<m)
s.add(0<c, c<m)

for i in range(len(X)-1):
    s.add(((a*X[i]+c)%m)==X[i+1])

print(s.check())
print(s.model())

# sat
# [m = 100,
# c = 3,
# a = 21,
# div0 = [(1389, 100) -> 13,
#         (1872, 100) -> 18,
#         (1515, 100) -> 15,
#         else -> 0],
# mod0 = [else -> 0]]

sol = s.model()
next_x = (sol[a].as_long()*X[5]+sol[c].as_long()) % sol[m].as_long()
print(next_x)
# 18

To read:

• namespace
• strategies