Z3-Solver 教程

算法算法，离不开各种公式。我们坚信：只要解出这些公式，就可以得到 flag。

但计算机中的 “公式” 往往不会是简单的 x+y=2x+y=2 之类，而会是掺杂了算术、位向量、数据结构等。我们（判断能否）解出这些公式的过程，就是在判断这些公式的可满足性 (Satisfiability) 如何。

这里我们就提出了可满足性模理论 (Satisfiability Modulo Theories, SMT)：

给定一组理论 (Theory)，根据给定逻辑，求在该组理论解释下公式的可满足性
现有理论通常针对一阶理论，即公理都是一阶的

从逻辑学角度来看，a+b<ca+b<c 或者 f(b)>cf(b)>c 都是逻辑系统中不包含的符号，计算机需要知道他们的意思，这就引出了理论的概念：

理论用于对这类符号谓词 / 函数（比如 >>，f(⋅)f(⋅)，++，…）赋予含义;
理论包含一组公理和这组公理能推导出的结论;

因此，如果想解决 SMT 问题，求解器就需要内置基本的理论。

首先，Z3 内置的理论都是在一阶逻辑 (FOL, first-order logic) 下定义的，需要推的公理只使用这些一阶逻辑理论定义。
一阶逻辑的显著特点是只对对象变量（如 xx，yy 等）进行量化（全称量化 ∀ 和存在量化 ∃），没有对函数或谓词本身做量化，它们在这些理论中应当是固定的。一阶逻辑相对好求，因为对象集合离散且数量级较小，可以用 SMT 技术穷举。
二阶逻辑量化的是谓词/函数本身，这些谓词和函数在现有理论中是不固定的。二阶逻辑难求，因为它需要遍历所有可能的谓词/函数，数量级非常大，Z3 不支持这一类问题。

换句话说，一阶逻辑相当于数学考试中的 “求符合条件的 xx 的值”，二阶逻辑相当于 “求符合条件的函数 f(x)f{(x)}”

将程序算法当成一个 SMT 问题，我们便可以从正向破解它，并且相对于逆向的难度较小。Z3 就是一个高效的 SMT 求解器，具有专门用于解决一阶逻辑理论的算法。

Z3Py 入门

要使用 Python 的 Z3，请通过 pip 安装：

接下来我们解一个简单的二元一次方程：

from z3 import *

x= Int('x')
y= Int('y')
solve(x > 2, y < 10, x + 2 * y == 7)

得到输出：

1	[y = 0, x = 7]

函数 Int('x') 用于在 Z3 中创建一个名为 x 的整数变量。solve 函数求解一个约束系统 (System of Constraints)。上面的例子使用了两个变量 x 和 y，以及三个约束 (Constraints)：

x 必须大于 2
y 必须小于 10
当 x 加上 y 的两倍时，它必须等于 7

约束就相当于考试中的条件和公式。

Z3Py 和 Python 一样使用 = 进行赋值，使用运算符 <、<=、>、>=、== 和 != 进行比较。

接下来，我们将介绍 Z3 Solver 的一些特性。

表达式属性

x = Int('x')
y = Int('y')
n = x + y >= 3
print ("num args: ", n.num_args())
print ("children: ", n.children())
print ("1st child:", n.arg(0))
print ("2nd child:", n.arg(1))
print ("operator: ", n.decl())
print ("op name:  ", n.decl().name())

输出：

num args:  2
children:  [x + y, 3]
1st child: x + y
2nd child: 3
operator:  >=
op name:   >=

n 注册了一个表达式类，通过类 n 提供的方法，我们可以得到表达式的参数、子式（左右两边的式子）和比较运算符信息。

基本数学运算

Z3 提供所有基本的数学运算。Z3Py 使用与 Python 语言相同的运算符优先级。^[1]

Z3 内置的整数算术是 Presburger 算术，只完备支持加减法、乘常数和比较运算。

Z3 基本数学运算支持与完备性速查表

本表由 GPT-5 生成
本表基于 Z3Py 与 SMT - LIB2 标准，标明完备性（✅ 完备 / ⚠️ 部分完备 / ❌ 不完备）。

✅ 完备：Z3 在相应理论（如 LIA/LRA）下可保证可判定且一定返回 SAT/UNSAT。
⚠️ 部分完备：Z3 尝试求解，但可能返回 unknown。
❌ 不完备 / 不支持：Z3 无内置语义，需人工编码或近似化。

参考

通用 (LIA / LRA)

Z3Py	SMT-LIB2	含义	完备性
`+`	`+`	加法	✅
`-`	`-`	减法 / 取负	✅
`*`	`*`	乘法（线性，有一个是常量）	✅
`/`	`/`	实数除法	✅
`<`, `<=`	`<`, `<=`	小于 / 小于等于	✅
`>`, `>=`	`>`, `>=`	大于 / 大于等于	✅
`=`	`=`	等式	✅
`Distinct(a,b,c)`	`distinct`	两两不等	✅

整数专用 (LIA / LIA + mod)

Z3Py	SMT-LIB2	含义	完备性
`IntDiv(x, y)`	`div`	整数除法（向零取整）	✅
`x % y` / `Mod(x, y)`	`mod`	取模（符号与被除数相同）	✅
`Abs(x)`	`abs`	绝对值	✅
`ToReal(x)`	`to_real`	Int → Real 转换	✅
`ToInt(x)`	`to_int`	Real → Int 转换（向零取整）	✅
`is_int(x)`	`is_int`	检查实数是否是整数值	✅

常量与类型装换

Z3Py	SMT-LIB2	含义
`IntVal(n)`	numeral	整数常量
`RealVal(r)`	numeral	实数常量

不属于基本运算的运算（非线性 / 超越）

运算	例子	完备性	备注
非线性乘法	`x*y`	⚠️	两个算子都属于变量
幂运算（常数指数）	`x**2`	⚠️	属于非线性算术，可求但不完备
幂运算（变量指数）	`x**y`	❌	一般不可判定
平方根 / 开方	`sqrt(x)`	⚠️/❌	需编码为幂运算
三角函数	`sin(x)`	❌	不支持内置语义
对数 / 指数函数	`log(x)` / `exp(x)`	❌	不支持内置语义
其他超越函数	—	❌	不支持

布尔逻辑运算

Z3 支持布尔运算符：与 (And)、或 (Or)、非 (Not)、蕴含 / 充分条件 (Implies)、如果 (If)。双蕴含（即充要条件）使用等号 (==) 表示。

常 / 变量表示

一阶逻辑公式由项（变量或常量）与扩展布尔结构组成。变量在 Z3 中可表示为：

x = Int(name = 'x') 

y = Real(name = 'y') 

z = BitVec(name = 'z', bv = 32) 

p = Bool(name = 'p')

这里可以忽略掉 name 和 bv，直接写参数，如 BitVec('z', 32)

在 Z3 中，Int 类型使用的是数学上的 “整数” 概念，这和我们在计算机中有范围的 int 类型不一样。如果需要指定类型可以表示的数字大小，请使用 BitVec，如 BitVec('x', 32) 表示一个 32 位位向量，就相当于我们在计算机中使用的 int。

我们建议，如果想要声明 “整数” 变量，请使用 Int 而不是 BitVec 以避免截断导致的精度问题。

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

1
2
3

ToReal(x)

ToInt(y)

Z3 也支持序列的表示：

flag = [BitVec('x%d' % i, 8) for i in range(32)] 

flag = [Int('%d' % i) for i in range(32)] 

flag = [BitVec('x%d' % i, 32) for i in range(32)]

BitVec('x%d' % i, 8) 应该这样理解：%d 对应循环计数器 i，本句实际上在创建从 x0 到 x31 的数个 8 位符号位向量。
这种方式声明的序列，在添加约束时应该调用 flag[i]，默认输出 x<i> = ...

对于常量，除了 Python 原有的数据类型外，也可以用 Z3 自己的数据类型表示：

>>> IntVal(val = 114514) 
114514

>>> RealVal(val = 1919810) 
1919810

>>> BitVecVal(val = 1145141919810, bv = 32) 
2680619074

>>> BitVecVal(val = 1145141919810, bv = 64) 
1145141919810

Z3 中的布尔常量用 True 和 False 表示。

求解器

如果只有公式（约束）较少，那我们调用 solve 方法就好，但有时我们会有大量约束，单行命令易读性就很差了。此时需要创建一个求解器类 Solver，一行一行地将约束添加进去。所以，求解器是一群约束的集合。

1	s = Solver()

现在我们创建了一个求解器实例 s，需要用 add 方法向这个求解器添加约束：

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

添加约束之后，我们可以调用 check 方法检查约束是否可满足 (satisfiable)。如果返回 sat 即为 “可以满足”，unsat 即为 “不可满足”。

如果约束可以满足，则我们可以调用 model 方法得到一组解。

如果需要输出结果（包括满足性情况），注意使用 print 函数。

之前示例中使用的 solve 方法是通过 Z3 求解器 API 实现的。当你调用 solve 时，Z3 会帮你创建一个临时的求解器，将约束传入，检查是否满足并输出结果。可以将 solve 方法简单理解为 check、model 和 print 的一次性封装。

一个求解器示例：

from z3 import *

flag = [Int('s[%d]' % i) for i in range(6)]

s = Solver()








s.add(flag[2] - flag[3] == 0x84A236FF)
s.add(flag[3] + flag[4] == 0xFA6CB703)
s.add(flag[2] - flag[4] == 0x42D731A8)
s.add(flag[0] == 0xDF48EF7E)
s.add(flag[5] == 0x84F30420)
s.add(flag[1] == 0x20CAACF4)

if s.check() == sat:
    m = s.model()
    print(m)
else:
    print("No solution")

运行后输出：

[s[4] = 2652626477,
 s[2] = 3774025685,
 s[0] = 3746099070,
 s[1] = 550153460,
 s[5] = 2230518816,
 s[3] = 1548802262]

Python 运算符 ↩︎

推荐订阅源

Watermelonabc的Blog