Z3使用简介

简介

z3是巨硬开发的开源线性约束求解器

数据类型

  1. Int
  2. Real
  3. BitVec
  4. 文档

使用一般步骤

  1. 定义数据类型

    1
    2
    a = Int('a') # 定义一个数学上的整数整数
    x = [BitVec('x%d'%i,32) for i in 6] # 定义6个32位整数型位向量，就是C/C++中的int

  2. 添加约束

    1
    2
    3
    4
    s = Solver()
    s.add(x[0]+x[1]<10)
    s.add(x[0]==2)
    s.add(x[0]+x[3]==5)

  3. 求解

    1
    2
    3
    4
    5
    res = []
    if s.check()==sat: #如果约束满足
        m = s.model() # 满足的模型
        for i in m:
            res.append(i.as_long()) # 转化为长整型

  4. 上述情况只能找到一种满足情况的解，可能存在溢出

参考资料

[1] z3一把梭

[2] [vscode自动补全功能]

附件

全部代码(这个例子溢出，所以不相等)

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
from z3 import *

x = [BitVec('x%i'%i,32) for i in range(6)]
s = Solver()
s.add(x[0]==0xDF48EF7E)
s.add(x[1]==0x20CAACF4)
s.add(x[5]==0x84F30420)
s.add(x[2]-x[3]==0x84A236FF)
s.add(x[3]+x[4]==0xFA6CB703)
s.add(x[2]-x[4]==0x42D731A8)
'''
x[3]-x[4]=0x42d731a8-0x84a236ff
x[3] = (0x42d731a8-0x84a236ff+0xfa6cb703)/2;
x[2] = x[3]+0x84a236ff;
x[4] = 0xfa6cb703-x[3];
'''
res = []
while s.check()==sat:
    m = s.model()
    for i in x:
        res.append(m[i].as_long())
    print(m)