简介《Z3使用教程.pdf》是一份面向自动化验证与程序分析场景的SMT求解器入门教程适合需要处理一阶逻辑可满足性问题的开发人员、研究人员及学生研读。资源压缩包为1个PDF文档仅518KB目前已有86人学习篇幅精简但覆盖核心知识点。教程从可满足性模理论的基本定义出发结合数组理论、算术理论等示例解释可满足与不可满足的概念并展示Z3的系统架构及SMT-LIB2脚本、高级语言API两种交互方式。重点讲解Python API的使用与安装包含源码编译、预编译二进制部署两种途径辅以example.py写法的具体演示可帮助读者快速上手Solver创建、约束添加、模型求解等操作为后续应用Z3完成软硬件验证、形式化推理和程序分析等任务打下基础。1. Z3 是什么一个能告诉你「有没有解」的 SMT 求解器如果你写过程序验证、做过 CTF 逆向、或者被「这组约束到底有没有解」折磨过Z3 就是那个能把问题丢进黑匣子、然后返回 sat 或 unsat 的工具。它不是普通的 SAT 求解器而是可满足性模理论SMT求解器支持算术、位向量、数组、非解释函数等背景理论甚至这些理论的组合。本文这份《Z3使用教程.pdf》就是围绕 Z3 的 Python API 展开的从 SMT 基础概念讲起依次覆盖安装、三类典型求解场景命题逻辑、整数算术、数组与函数组合和常用函数。适合正在做形式化验证、自动化推理、程序分析的从业者也适合刚接触 SMT、想快速跑通第一个check()的新手。后面我会按「理论→安装→实例→避坑→进阶技巧」的顺序把教程里的内容拆成可直接照着做的步骤。2. 理解 Z3 的求解模型SMT-LIB2、Python API 与两大理论2.1 SMT 求解的是什么从命题到理论组合SMT 不是「判断一段代码对不对」而是「给定一组一阶逻辑公式在某些背景理论下判断它是否可满足」。可满足的意思是存在至少一组赋值让所有公式同时为真。比如公式x 0 且 y 1 且 x y 1一眼能看出不可能成立这就是不可满足而length 3, a [1,2,3]可以满足「数组 a 升序排列」这就是可满足并且 Z3 还能把解打出来。教程里花了不少篇幅讲背景理论划分这一步别跳过。公式∀i,j. 0 i j length a[i] a[j]属于数组理论加算术理论因为它同时涉及数组读写和比较运算公式∀a,b,c,d. a d ∧ b c a b c d属于算术理论。Z3 的高明之处在于它能把多个理论组合到一起求解而不是傻乎乎地全部转换成布尔逻辑SAT。理解这一点你就知道为什么用 Z3 解「数组升序 存在 key」这类问题比我们自己写回溯枚举要靠谱得多。理论上 SMT 问题的表达方式不止一种。Z3 支持用户通过 SMT-LIB2 脚本交互也可以直接调用高级语言 API。SMT-LIB2 是标准脚本格式适合调试和跨工具复用而 Python API 的优点是类型系统、函数定义和模型读取都在语言层面写验证逻辑时跟写普通 Python 代码几乎一样。教程里主推 Python 前端我实际工程里也几乎只用 Python API因为跑反例验证和批量枚举时脚本比文本格式好控制。2.2 Python API 的调用路径Solver、check 与 modelZ3 Python API 的核心调用链可以压缩成四步声明变量创建 Solver添加约束调用check()后读model()。下面这组代码是教程里整数算术例子的完整版我加了注释from z3 import * # 声明两个整数变量注意是 Int(x) 不是整型 int x, y Int(x), Int(y) # 创建一个 Solver 实例 solver Solver() # 用 add 添加约束Z3 内部会维护一个约束集合 solver.add(x y 42) solver.add(x - 6*y 2) solver.add(x % 2 1) # x 必须是奇数 # check() 返回 sat / unsat / unknown 三个枚举值 if solver.check() sat: m solver.model() # 把 model 存下来不要反复调用 print(m[x], m[y]) else: print(unsat)逻辑说明add()每调用一次就是在原约束集合上追加一条。Z3 求的是所有约束的合取所以多个add()与一次add()传多个参数等价。check()返回sat只说明存在解解的具体值要通过model()映射变量拿到。这里有个细节m[x]返回的是一个 Z3 算术表达式对象而不是 Python 整数直接print没问题但如果要参与 Python 计算需要用m[x].as_long()转成 int。参数说明Int(x)创建的是数学意义上的整数不是range里的整型Z3 还提供Real()、Bools()、Ints()一次声明多个变量等构造函数。solver.check()带参数时可以单独做假设检查例如check(a, b)这在排查哪条约束导致不可满足时非常有用教程里没细讲后面避坑部分我会提到。2.3 数组与理论组合Store/Select 的语义数组理论是 Z3 最容易让新人困惑的部分因为它不是命令式语言的数组赋值而是函数式更新。教程里的示例用了Store(A, x, 3)意思是「生成一个新数组下标 x 处的值为 3其他位置跟原数组 A 相同」。这是个纯函数操作不修改原数组 A。索引读取用A[i]形式等价于Select(A, i)。from z3 import * x, y, z Ints(x y z) A Array(A, IntSort(), IntSort()) # 数组 A整数下标 - 整数值 f Function(f, IntSort(), IntSort()) # 函数 f整数 - 整数 # 公式如果 x2y则 f(Store(A,x,3)[y-2]) f(y-x1) fml Implies(x 2 y, f(Store(A, x, 3)[y - 2]) f(y - x 1)) solve(fml)逻辑说明Implies(a, b)表示 a 蕴含 b。在前提x 2 y下y - 2 x所以Store(A, x, 3)[y-2]等于Store(A, x, 3)[x]也就是新数组在 x 处的值即 3右边y - x 1在前提y x2下等于 3。于是公式变成f(3) f(3)恒真。Z3 的solve()直接输出sat。注意这里的变量z声明了但没出现在公式里这是允许的Z3 不会因为你声明了没用的变量抱怨。这个例子还体现出 Z3 的一个关键设计Array和Function都是「解释很慢、但语义很严格」的对象。A[i]这个读写操作背后是 Select 操作符Store背后是写操作符。你在约束里写得越接近数学语义求解器做归一化和 term rewriting 的能力就越强。血泪经验是别试图用 Python 的 list 或 dict 去模拟数组再转成约束Z3 处理器不认识那些 Python 对象正确做法是一开始就声明 Z3 的Array。3. 安装 Z3 并跑通第一个脚本三种系统的操作顺序3.1 Ubuntu 源码编译安装依赖、mk_make 与 make教程里给的源码安装流程基于 Ubuntu 20.04 LTS amd64我自己在 22.04 上同样跑通过。先装依赖再克隆源码然后走 Z3 专用的mk_make.py脚本生成 Makefilesudo apt update sudo apt install git make python3 python3-pip git clone https://github.com/Z3Prover/z3.git cd z3 python3 scripts/mk_make.py --python cd build make sudo make install逻辑说明mk_make.py是个生成器它会把 C 核心和 Python 绑定一起编译。--python参数指定生成 Python 模块不加的话默认只编译命令行工具。make过程比较长建议提前确认磁盘空间和编译内存我遇到过一次 2GB 内存的小机器编译到一半被 OOM 杀掉的。参数说明mk_make.py还有别的参数比如--debug、--static、--java默认不用加。如果只想用 Python API--python就够了如果还想跑 SMT-LIB2 脚本编译出来的z3可执行文件会直接进系统路径。安装完后敲z3 --version能看到版本号。这里有个容易忽略的点源码安装不会自动安装z3-solver的 pip 包所以 Python 里import z3依赖的是编译生成的.so文件。如果你系统里早就pip install z3-solver过源码安装后可能会混淆。建议源码安装前先把 pip 版卸掉避免两个版本打架。3.2 二进制分发包Linux/Windows/macOS 的 PATH 与 PYTHONPATH不想编译的话教程给了预编译二进制方案。Z3 的 GitHub Release 页面提供各平台的 zip 包教程里是基于 4.8.10 版本讲解的。Linux 下的安装思路是解压后把内容复制到/usr/localsudo apt update sudo apt install python3 python3-pip wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-ubuntu-18.04.zip unzip z3-4.8.10-x64-ubuntu-18.04.zip sudo cp -R z3-4.8.10-x64-ubuntu-18.04/* /usr/local/逻辑说明包内的bin/python/目录放着 Z3 的 Python 绑定文件bin/下放着 z3 命令行可执行文件。复制到/usr/local后z3 命令可以直接运行但 Python 能找到 z3 模块是因为路径已经在默认搜索范围内。如果找不到你还需要手动把bin/python加进PYTHONPATH。Windows 上的步骤稍微绕一点因为要手动配两个环境变量。解压 zip 到C:\Program Files (x86)\z3-4.8.10-x64-win后打开系统环境变量设置在Path里追加C:\Program Files (x86)\z3-4.8.10-x64-win\bin然后新建PYTHONPATH变量值为C:\Program Files (x86)\z3-4.8.10-x64-win\bin\python。macOS 的 zip 解压后也是同样思路不过是把路径换成解压目录。一个常见习惯是安装后用命令行验证一遍。Windows 下打开 cmd先确认python -V有输出再执行下面命令python -c import z3; print(z3.get_version_string())如果能打印出版本号说明 Z3 模块已经进入 Python 的搜索路径。这一步非常值得做很多人配完 PATH 以为完事了结果import z3依然报 ModuleNotFoundError。3.3 安装后验证example.py 与 solve() 快速函数无论哪种安装方式教程都反复出现example.py脚本求解公式是∃x,y∈R. xy5, x1, y1。这个脚本帮助你验证安装是否真正通了from z3 import * x, y Real(x), Real(y) s Solver() s.add(x y 5, x 1, y 1) if s.check() sat: m s.model() print(fSolution: x {m[x]}, y {m[y]}) else: print(No solution exists.)逻辑说明这里声明的是实数变量因此输出可能是一个分数或小数。Z3 返回的模型是满足所有约束的一组赋值m[x]和m[y]就是那组解。你得出的具体解可能跟教程里写的[y4, x2]不一样因为 Z3 在多个模型之间选哪个并不保证固定这是求解器的正常行为不是翻车。在验证环境时我更习惯先用solve()这种一步到位的函数。solve(fml)等价于「创建 Solver、add 约束、check、model、打印」全流程适合快速验证一个小公式。教程里的 Tie/Shirt 命题例子就是用solve()写的from z3 import * Tie, Shirt Bools(Tie Shirt) solve(Or(Tie, Shirt), Or(Not(Tie), Shirt), Or(Not(Tie), Not(Shirt)))输出结果是sat加一组模型TieFalse, ShirtTrue。建议第一次跑通时用它等正式写验证逻辑再换回 Solver 对象——因为solve()把内部状态封装死了你没法拿到 Solver 引用去做渐近式约束追加。4. 用 Python API 求解三类问题命题、算术、数组函数4.1 命题逻辑Bools、Or、Not 与模型读取命题逻辑是 Z3 最简单也最适合练手的入口。教程里的 Tie/Shirt 例子其实是经典编译原理教材里的「穿衣约束」你必须在衬衫(Tie)和T恤(Shirt)之间做选择规则是至少穿一个、如果穿领带必须穿T恤、不能同时穿领带和T恤。用代码表达from z3 import * Tie, Shirt Bools(Tie Shirt) s Solver() s.add(Or(Tie, Shirt)) # 至少穿一件 s.add(Or(Not(Tie), Shirt)) # 穿领带 穿T恤 s.add(Or(Not(Tie), Not(Shirt))) # 不能两个都穿 print(s.check()) if s.check() sat: m s.model() print(Tie , m[Tie], Shirt , m[Shirt])逻辑说明Bools(Tie Shirt)一次声明两个布尔常量等价于Tie, Shirt Bool(Tie), Bool(Shirt)。三个Or合起来就是教程里的合取式(Tie∨Shirt) ∧ (¬Tie∨Shirt) ∧ (¬Tie∨¬Shirt)。解是 TieFalse、ShirtTrue也就是只穿T恤。这个例子的价值在于让你意识到 Z3 的布尔常量不是 Python 的 bool。m[Tie]返回的是 Z3 的 BoolRef 对象print显示为 False/True但你不能直接在 Python 代码里写if m[Tie]:需要显式转换bool(m[Tie])。这个坑在第四章里再次遇到。4.2 整数与模运算x y 42 这类约束怎么建模教程的第二个例子是求解x y 42,x - 6y 2,x % 2 1的整数解也就是找到一个奇数的 x 和对应的 y。完整脚本前面已经出现过这里讲两个建模技巧一是模运算在 Z3 里用%表示但语义是数学余数不是 Python 的%Python 的%对负数结果符号跟随除数Z3 的%结果非负。二是Int(x)声明的是整数变量如果你在约束里写了除法/Z3 会把它解释成实数除法导致模型可能返回有理数。处理这类问题时我会先问自己我要的是整数解还是实数解如果题目限定整型所有中间量尽量都用Int()声明不要混入Real()。如果必须在整数上做除法用Div(x, 2)而不是x / 2。%和Div是 Z3 的整数操作符/是实数操作符这个区分是新手最容易踩的。还有一个实用技巧check()返回sat后模型里的值可能是惰性生成的表达式。比如m[x]返回的可能是0或4等具体值但也可能是x本身当 x 是自由变量且没有约束限制它时。这时候不要慌用simplify(m[x])或m[x].as_long()把它压成 Python 整数。4.3 函数与数组理论组合Implies、Store 的常量折叠第三个例子是 Z3 真正体现「模理论」能力的地方公式里同时出现算术、数组和函数。前面的代码已经给出这里我拆开讲解每个 API 的含义。Implies(x 2 y, ...)构造蕴含式Store(A, x, 3)返回一个新数组表达式不是直接修改 Af(...)是非解释函数它不定义具体行为只要求函数一致性相同输入必须相同输出。这类问题用 SAT 求解器很难处理因为非解释函数和数组都需要专门的决策过程而 Z3 的数组部分用「读/写公理」和「常量折叠」来简化。我一般在验证真实程序时会把这种「数组更新 函数调用」的公式当作最小复现用例。比如检查一段代码在数组更新后某函数调用结果是否保持一致抽象成f(Store(A,x,3)[x]) f(3)Z3 能快速化简。教程里也提到Z3 的 Python API 还支持And()、Or()、Not()等逻辑连接词组合起来可以表达任意一阶逻辑公式。需要注意Store与Select的嵌套优先级。表达式f(Store(A, x, 3)[y - 2])先做Store再对结果做索引读取。如果你先读A[y-2]再 Store语义完全不同。写这类公式时我会先手动算一遍下标确认y-2和y-x1在前提下的值再用 Z3 验证避免被自己的公式带偏。5. Z3 使用避坑常见问题与排查5.1 现象s.check()返回unknown求解复杂公式时check()可能既不是sat也不是unsat而是unknown。原因是 Z3 的决策过程并没有完备覆盖所有理论组合比如非线性整数算术乘法和变量同时出现或带量词的公式可能超出它的可判定范围。Z3 在无法证明可满足或不可满足时就返回unknown。解决方法是先降低公式复杂度把乘法规整成线性约束或者用量词实例化参数qid、pattern辅助引导。我一般会先剔除一部分约束用二分法定位到底是哪个子公式导致计算不收敛再针对性地改写模型。如果问题本身就是非线性的考虑把变量转成实数域求解整数解再做一轮附加约束筛选。5.2 现象model()里出现表达式而不是具体值有时候你print(m[x])得到的是x而不是数字或者是一个很长的算术表达式。原因是 Z3 的模型可能是「符号模型」当变量没有受到足够强的约束时求解器可以直接给出x x的自引用赋值这在逻辑上合法但对用户不直观。解决时可以调用simplify(m[x])化简或者给变量补一个明确的边界约束比如x 0, x 100让模型更具体。如果是数组模型Z3 返回的可能是const(0)或 lambda 表达式这也是正常的数组本身就适合用函数式表示。5.3 现象整数与实数混用导致无解误判用Int(x)声明变量但在约束里写了x / 2 1Z3 会把/解释成实数除法于是 x 的解可能是2.0而不是整数甚至在某些情况下因为类型不匹配产生奇怪行为。另一个常见翻车是在一个公式里既用了Int又用了RealZ3 会尝试做类型强制提升一旦做不了判断结果就是 unexpected behavior 或 unknown。解决保持变量类型统一。整数除法用Div(x, 2)取模用x % 2 1如果确实需要实数中间结果就从Real()开始声明最后再转整数。或者在求解前用z3.is_int(m[x])检查模型值的类型。5.4 现象安装后import z3报 ModuleNotFoundError源码安装或二进制包安装后最常见的问题是 Python 找不到 z3 模块。原因通常是PYTHONPATH没指到bin/python目录或者当前 Python 解释器与编译时的 Python 版本不一致。教程里的 Windows 步骤已经让你配了 PYTHONPATH但 Linux 下很多人会忘记这一步。解决用python3 -c import sys; print(sys.path)查看搜索路径手动追加export PYTHONPATH/path/to/z3/install/bin/python到~/.bashrc。如果仍然报错检查是不是系统里有多个 Python 版本用which python3确认。说实话对只想用 Python API 的人我目前更推荐直接用pip install z3-solver它能自动处理绑定和版本问题省掉源码编译的麻烦。5.5 现象solve()输出不可控且model()被调用两次solve()自动打印的结果格式固定无法拿来做进一步处理而新手常写if s.check() sat: print(s.model())看起来没问题实际上s.model()在内部会触发生成模型如果打印后又想取某个变量的值等于生成了两次模型复杂公式下会有性能损耗。解决先m s.model()存到一个变量里再统一从m中取值。对结果格式有要求的场景不要用solve()用Solver对象手动控制。有一种常见做法是s.model()返回 None——如果你在check()返回sat之前调用model()确实会得到 None。确保顺序是check()在前model()在后。6. 把 Z3 用到真实工程验证、枚举与一个验证技巧6.1 用 sat/unsat 做程序验证的「找反例」循环把 Z3 用作程序验证器时标准套路是把程序的不变量和断言编码成 SMT 公式如果断言被违反公式就是 satZ3 给出的模型就是反例。比如你要验证「数组 a 前 n 个元素升序」可以把循环变量建模成Int然后构造一个存在性公式「存在 ij 且 a[i]a[j]」Z3 返回 sat 就意味着找到了反例。这是我最常用的验证姿势。6.2 固定一个变量打印多组解枚举技巧Z3 的model()一次只给一组解如果要枚举多组解就在每轮sat后把当前解「堵住」再重新求解from z3 import * x, y Int(x), Int(y) s Solver() s.add(x y 10, x 0, y 0) while s.check() sat: m s.model() print(x , m[x], y , m[y]) # 关键排除当前解让求解器去找下一组 s.add(Or(x ! m[x], y ! m[y]))逻辑说明s.check()每次返回 sat 后我们拿到一组具体赋值然后把这个赋值「否定」加到约束里。m[x]返回的 Z3 表达式可以直接用于构造约束不需要转成 Python int。循环会一直跑到 unsat 为止。这个枚举技巧在做测试用例生成时非常实用。参数说明如果模型里有数组类型的变量等价地排除它就稍微复杂点可以用Select比较数组元素不过简单场景不容易遇到。6.3 一个技巧用simplify()验证恒等式教程里手动推导了f(Store(A,x,3)[x]) f(3)的恒等性在工程里可以直接用simplify()自动验证from z3 import * x Int(x) A Array(A, IntSort(), IntSort()) expr Store(A, x, 3)[x] print(simplify(expr)) # 输出 3solve只能告诉你可满足性而simplify() 能告诉你表达式的规范化形式对于检查自己的公式写没写错这是一张后悔药。说句实话Z3 的模型输出在复杂约束下会给你一些意想不到的结果但那不是玄学而是它在不保证唯一解的前提下挑了一组。从那以后我每次拿 Z3 做验证都会强制走一遍「先simplify化简→再check→然后存model→最后as_long转类型」的流程发现报错先从类型和公式改写入手。希望帮到你。本文还有配套的精品资源点击获取