z3约束求解

安装

python版安装

1
$ pip3 install z3-solver

基本用法

变量表示

一阶命题逻辑公式由项（变量或常量）与扩展布尔结构组成，在 z3​ 当中我们可以通过如下方式创建变量实例：

  • 整型（integer，长度不限）
1
2
>>> import z3
>>> x = z3.Int(name = 'x') # x is an integer
  • 实数类型（real number，长度不限）
1
>>> y = z3.Real(name = 'y') # y is a real number
  • 位向量（bit vector，长度需在创建时指定）
1
>>> z = z3.BitVec(name = 'z', bv = 32) # z is a 32-bit vector
  • 布尔类型（bool）
1
>>> p = z3.Bool(name = 'p')

整型与实数类型变量之间可以互相进行转换：

1
2
3
4
>>> z3.ToReal(x)
ToReal(x)
>>> z3.ToInt(y)
ToInt(y)

常量表示

除了 Python 原有的常量数据类型外，我们也可以使用 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]

例题

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
__int64 __fastcall sub_400770(_DWORD *a1)
{
  __int64 result; // rax

  if ( a1[2] - a1[3] == 2225223423LL
    && a1[3] + a1[4] == 4201428739LL
    && a1[2] - a1[4] == 1121399208LL
    && *a1 == -548868226
    && a1[5] == -2064448480
    && a1[1] == 550153460 )
  {
    puts("good!");
    result = 1LL;
  }
  else
  {
    puts("Wrong!");
    result = 0LL;
  }
  return result;
}
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
import z3

x = [0] * 6
for i in range(6):
    x[i] = z3.Int('x[' + str(i) + ']')//生成具有6个元素的列表x

s = z3.Solver()                      //生成求解器对象
s.add(x[0] == 0xDF48EF7E)            //添加约束条件
s.add(x[5] == 0x84F30420)
s.add(x[1] == 0x20CAACF4)
s.add(x[2]-x[3] == 0x84A236FF)
s.add(x[3]+x[4] == 0xFA6CB703)
s.add(x[2]-x[4] == 0x42D731A8)

if s.check() == z3.sat:              //判断有解
    print(s.model())
else:
    raise Exception("NO SOLUTION!")