Z3-solver初学

Z3安装

pip install z3-solver

常用实例

1
2
3
4
5
6
7
8
9
10
11
from z3 import *

x,y=Reals('x y')
x = z3.Int(name = 'x') # x is an integer
y = z3.Real(name = 'y') # y is a real number
z = z3.BitVec(name = 'z', bv = 32) # z is a 32-bit vector 位向量长度需在创建时指定
p = z3.Bool(name = 'p')

#整数和实数可以互相转换
z3.ToReal(x)
z3.ToInt(y)

Z3自带常量类型运算

1
2
3
4
5
6
7
8
>>> z3.IntVal(val = 114514) # integer
114514
>>> z3.RealVal(val = 1919810) # real number
1919810
>>> z3.BitVecVal(val = 1145141919810, bv = 32) # bit vector，自动截断
2680619074
>>> z3.BitVecVal(val = 1145141919810, bv = 64) # bit vector
1145141919810

求解器

在使用 z3 进行约束求解之前我们首先需要获得一个 求解器 类实例，本质上其实就是一组约束的集合：

1
>>> s = z3.Solver()

添加约束 ¶
我们可以通过求解器的 add() 方法为指定求解器添加约束条件，约束条件可以直接通过 z3 变量组成的式子进行表示：

1
2
>>> s.add(x * 5 == 10)
>>> s.add(y * 1/2 == x)

对于布尔类型的式子而言，我们可以使用 z3 内置的 And()、Or()、Not()、Implies() 等方法进行布尔逻辑运算：

1
2
3
>>> s.add(z3.Implies(p, q))
>>> s.add(r == z3.Not(q))
>>> s.add(z3.Or(z3.Not(p), r))

约束求解

当我们向求解器中添加约束条件之后，我们可以使用 check() 方法检查约束是否是可满足的（satisfiable，即 z3 是否能够帮我们找到一组解）：
z3.sat：约束可以被满足
z3.unsat：约束无法被满足

1
2
>>> s.check()
sat

若约束可以被满足，则我们可以通过 model() 方法获取到一组解：

1
2
>>> s.model()
[q = True, p = False, x = 2, y = 4, r = False]

对于约束条件比较少的情况，我们也可以无需创建求解器，直接通过 solve() 方法进行求解：

1
2
>>> z3.solve(z3.Implies(p, q), r == z3.Not(q), z3.Or(z3.Not(p), r))
[q = True, p = False, r = False]