z3库进阶

First Post:

Last Update:

Z3库使用

简单介绍z3

众所周知z3库是一个优秀的求解器，可以求解给出的给定的等式。

简单的库内函数：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
# 创建一个求解对象
s = Solver()
# 添加判断条件
s.add(等式)
# 判断是否有解
s.check
# 声明不同类型的未知数
# int型，无法使用按位运算
a = Int('a')
a,b = Ints('a b')
# real型
a = Real()
# 位向量，name表示名字，bv表示大小
x = BitVec('x',8)
x = [BitVecs(f'x[{i}]',8) for i in range(8)]

z3的一些特性

先看一段z3代码，猜测一下输出的结果。

1
2
3
4
5
6
7
8
9
10
from z3 import *
s = Solver()
x = Int('k')
k = Int('x')
a = x + 10
s.add(a == 15)
a = a - k
s.add(a == 12)
if s.check():
    print(s.model())

输出结果是：

1
[x = 3, k = 5]

从这段代码可以看出一些z3的特性，首先是z3声明未知数的命名，可以看到name其实只有在最后显示计算结果的时候才会用到，之前的算式与未知数的命名是无关的，只与存放未知数的变量名有关，当然最好保证变量名与未知数名的一致性。

第二点，z3是可以理解等式成立的先后顺序的，这里两个判断式都是判断a与一个值是否相等，但是中间插入了运算，可以看到z3是能正确求解得。

z3的求解同时也可以配合python中的循环与判断语句，来求解更复杂的式子。

≡