Z3¶

Variable Type¶

• Int(name: str) : integer
• Real(name: str) : real number
• Bool(name: str) : True or False
• BitVec(name: str, length: int) : length bits integer

Solver¶

s = Solver()

• s.add(<condition>) : add condition to Solver
• s.check() : if there’s a solve for Solver return sat, else return unsat
• s.model() : return a solve of this Solver. we can use s.model()[x] to get x's value in this solve

Function¶

• And([condition1, condition2, ...]) or And(condition1, condition2, ...) : combine these conditions with and
• Or([condition1, condition2, ...]) or Or(condition1, condition2, ...) : combine these conditions with or

Example¶

from z3 import *

x = Int('x')
y = Int('y')
z = Int('z')

s = Solver()

s.add(And(x > 0, y > 0, z > 0))
s.add(x + y + z > 10)
s.add(x + y < 5)
s.add(y + z < 12)

while s.check() == sat:
    ans = s.model()
    print(ans)
    s.add(Or(x != ans[x], y != ans[y], z != ans[z]))