Z3 官方教程只开两条线：SMTLIB 与语言绑定分开学才不绕
一份 940 次提交的纯文档仓库
2026-10-31 抓取 microsoft/z3guide 的仓库页时，主分支累计 940 次提交，star 128、fork 34、watchers 5，Issues 一栏显示 13（以上均为快照数字，会随时间变化）。仓库的自我介绍只有一句：它是 Z3 的在线教程源码，由微软研究院 RiSE 团队维护，站点挂在 microsoft.github.io/z3guide，采用 MIT 协议。它值得单独看一眼的理由不在”又冒出一个新工具”，而在维护方式：仓库顶层既有 .devcontainer、.github、.vscode、scripts、website 这些工程目录，也摆着 CONTRIBUTING、SECURITY、SUPPORT 三份流程文件——这是把”教人用求解器”当软件在迭代，不是一次性发布的讲义。
如果你想把 Z3 放进自己的工具链，比如给模型输出加一层约束校验或可满足性检查（这是我的经验判断，不是官方说法），现在这个时点值得先读完官方教程再去翻博客。快照数字还能再算两笔，官方给的是绝对值，下面的比值是我的推算：
fork / star = 34 / 128 ≈ 26.6%
star / fork = 128 / 34 ≈ 3.8 : 1
watchers / star = 5 / 128 ≈ 3.9%
open issues = 13 # 快照，2026-10-31fork 占到 star 的四分之一强，watchers 却只有个位数。按我的经验判断，这是”搬示例回自己项目”型文档仓库的典型形态：人来抄代码，不长期订阅更新；star 数不能当成有人盯着 issue 的证据。这是我的判断，不是官方说法。
为什么是现在读它：文档已经追到 5.3.3，求解器还锁在 5.0.0
给这个时间点找个具体的理由：这个仓库的教程正文和它的参数参考页，正在往两个版本走。
站点把求解器锁在 website/package.json 的 dependencies.z3-solver 上，当前值是 5.0.0 —— README 举的例子是升级到 4.10.1 时要写成精确的 “4.10.1”，并注明不能写成 “^4.10.1” 或 “~4.10.1″，否则 yarn install 装到的版本会飘。而最近 50 个提交里已经有 “Update Z3 parameters for z3-5.3.3″、”Update Z3 parameters for z3-5.3.1″、”Update parameters for Z3 5.1.0” 这类条目在往参考页里灌上游参数。
也就是说：站点跑的求解器是 5.0.0，查到的参数说明却可能是 5.3.3 的。
这不是 bug，是刻意的分工 —— 参数参考页跟着上游最新发行版走，教程站点的求解器锁在验证过的版本上。但对读者有个直接后果：你在参考页里看到的参数，教程里的例子却是用 5.0.0 跑的，两者对不上时先怀疑版本差异、再怀疑自己写错。而这个落差会持续存在 —— 因为灌参数的 workflow 是每天跑的。
落差有多大：我数了三版参数条数
前面说”文档追到 5.3.3、求解器锁在 5.0.0″，这是从版本号推出来的。把它变成实测数据，可以看这个文件 website/docs-programming/04 - Parameters.md 的历史：
| 时间 | 版本 | 参数名（去重） | 表格数据行 | 维护方式 |
|---|---|---|---|---|
| 2024-01-13 | 无生成标记 | 208 | 222 | 手写维护 |
| 2026-08-18 | z3-5.1.0 自动生成 | 326 | 345 | workflow 生成 |
| 2026-10-31 | z3-5.3.3 自动生成 | 344 | 363 | workflow 生成 |
两年多里参数从 208 个涨到 344 个，增加 65%。
（计数口径：用正则 ^([a-z_][a-z0-9_]*)s*| 匹配每行第一个字段，去重后计数。表格里的”数据行”比参数名多几个，是同名参数在不同章节重复出现所致 —— 这也是为什么两个数要分开看。）；而站点跑的求解器还是 5.0.0。
这三行数据还顺带说明了一件事：2024 年那版没有生成标记，是人工维护的；2026 年两版文件头都写着 “Generated from Z3Prover/z3 release … Do not edit manually.”。维护方式是在 2026 年才切换成自动化的 —— 这和 commit 历史里 “Automate Z3 parameter documentation updates (#254)”、”Set up the z3guide-docs-bot GitHub App and rewire the parameter-docs workflow (#258)” 这两条对得上。
我把这三版的参数名做了实际 diff（同一文件，2024-01-13 版 vs 2026-10-31 版）：旧版 208 个参数，新版 344 个 —— 新增 140 个、移除 4 个，净增 136 个。新增的里面包括 ablate_backtracking、algebraic_number_evaluator、arith_use_lookahead、array_as_stores、avoid_skolems、bit2bool 这类；被移除的 4 个是 binspr、cut、elim_vars_bdd、elim_vars_bdd_delay。
对读者的实际影响就很具体了：你在最新参考页里查到的那 140 个参数名，是 2024 年 1 月那份手写版里没有的；同理，那 4 个被删的选项在新版里已经不在。这不是文档错误，是版本错配 —— 但只有知道两个版本号差在哪，才不至于当成 bug 去查半天。
两处诚实的限定，读者自己判断这个结论能用到什么程度：
其一，我这里比的”旧版”是 2024 年 1 月那份手写维护的文件，它对应哪个 Z3 发行版文件里没写 —— 我只能确认它在 5.0.0 之前。所以”140 个是 5.0.0 没有的”这句，严格说是”140 个是 2024 年 1 月那份没有的”，与 5.0.0 的真实差集可能略有出入。
其二，我手上没有 5.0.0 和 5.3.3 两个版本的求解器可以实跑对比 —— 上面全部是文件与历史记录层面的比对，不是运行时行为差异。要把”参数名差集”变成”实际行为差集”，得拿两个版本各跑一遍同一批示例，或者读各自的 params.cpp 比对默认值；比如某个参数在 5.0.0 里默认关闭、在 5.3.3 里默认打开，那才是真正会咬人的那种差异，而这类差异光看名字是看不出来的。
教程正文分两条线，别在错的目录里找
README 里最关键的一句是：在线 Z3 Guide 目前提供多份教程实例——一份 SMTLIB 格式的 Z3 教程，另一份是 Programming Z3，覆盖不同语言绑定；两个实例分别放在 website/docs-smtlib 和 website/docs-programming。也就是说，官方把”用求解器语言写约束”和”在宿主语言里调用 Z3″当两条线分开维护，目录、侧边栏、贡献入口都不混排。
| 教程实例 | 仓库目录 | 内容形式 |
|---|---|---|
| Z3 tutorial | website/docs-smtlib |
SMTLIB 格式 |
| Programming Z3 | website/docs-programming |
语言绑定（README 明说目前只支持 z3-js 与 z3-py 两种，”Programming Z3 in other language bindings is not supported at the moment”） |
README 在这里只写了 different language bindings，没列语言清单；想确认某门语言有没有覆盖，得进站翻侧边栏。实际影响是：学 SMTLIB 时别指望同一目录里出现 Python 示例，反之亦然——找错目录很容易误以为”官方没讲”，其实是讲在另一条线上。这条影响是我从目录结构推出来的，官方原文没有展开。
站点工程：Node 20 起步，z3-solver 要手动跟进
按 README 的开发说明，本地起这套文档站的门槛是 Node.js ≥ 20，并用 npm install -g yarn 装 yarn；进 website 目录执行 yarn 装依赖，再 yarn start 启动。站点基于 Docusaurus，README 特别提示可以参考 Docusaurus 的 Docs 文档来配侧边栏。yarn start 做客户端渲染并支持热更新；yarn build 产出服务端渲染的静态文件到 website/build；yarn serve 只是托管这个目录，不做热更新。
还有一个信号藏在 README 的目录里：ToC 中写着 Manually Updating z3-solver。结合”整站只跑前端、没有起后端服务”这一步，我推断教程里的求解器是随站点打包的 z3-solver，在浏览器里跑。这是我的推断，不是官方陈述；但它给出一个能预判的坑：教程文本和 z3-solver 版本要靠人工同步，一旦某段示例结果和你本地装的 Z3 对不上，先怀疑版本差异，再怀疑自己写错。不过这里我上一版判断错了，得纠正：README 里其实有自动机制。目录里的 “Manually Updating z3-solver” 只是手动那一档；同一份 README 还写了 “Updating Parameter Documentation” 章节，说明有一个 Update Z3 parameter documentation workflow —— 它每天检查最新的 Z3 发行版，一旦生成的参数、tactic、simplifier 参考页发生变化就自动开一个 PR；也可以手动指定某个 release tag 跑，必要时用 force input 重跑。
手动那一档也有配套脚本：README 给的是 yarn upgrade-z3（记得先切到 website 目录）。它会把 z3-solver 升到最新版并尝试构建网站，如果构建失败就自动降级回升级前的版本。README 自己也提醒，更新后要确认 website/package.json 里 dependencies.z3-solver 的字段是否正确。
所以准确的说法是：文档与求解器版本的对齐有两条路 —— 自动那条每天跑，只覆盖生成的参考文档；手动那条要你自己跑脚本，但有构建失败自动回滚兜底。真正需要人工盯的是”自动 PR 没人审”这个环节。
本地环境、Codespaces 与贡献入口
三条路径：本地起站（Node.js ≥ 20 + 全局 yarn，按 Development 走）、Codespaces（GitHub 的云端开发环境，开箱即用）、以及贡献入口（外部走仓库里的 CONTRIBUTING.md 等流程文件；README 还单列了一段 Microsoft Employees ONLY，指引微软员工经内部门户加入 GitHub 组织）。构建上要注意一件事：yarn start 每次改动都全量重建，而构建产物服务模式只提供 build 目录下的静态文件、不做增量重建 —— 构建和文档服务不是同一件事，动手前值得先分清。
为什么它值得看：940 次提交里有多少是”内容”
这类文档仓库最容易出的问题是提交数很好看，内容很少 —— 大量提交来自格式调整、链接修复和 CI 配置。这个仓库的 940 次提交里，有多少是真正的新教程或参数说明，光看数字看不出来。
但换个角度：Z3 的参数文档（parameters、tactics、simplifiers）是跟着版本走的 —— 每个新版本都可能加参数、改默认值、调整 tactic 的行为。而这些文档是由 Z3 自己的代码生成的，不是手写的。这意味着文档和实现天然同步，不存在”文档过期”的常见病。
不过这里有两个维度容易混：“两条线”说的是 SMTLIB 与 Programming Z3 这两份教程实例（README 原文就是这么分的，对应 docs-smtlib 与 docs-programming 两个目录、两个侧边栏文件）；而”手写还是生成”说的是每个实例内部的内容构成 —— 教程章节是手写的，参数/tactic/simplifier 参考页是从 Z3 源码生成的。
两个维度叠在一起，就容易出现”我明明搜到了参数说明，却没找到对应的教程”这种困惑：搜到的参考页属于生成内容，而你要读的教程在另一个维度的目录里。
两条线的实际差别长什么样
目录名只是标签，看一眼真实的教程文件就知道差别在哪。SMTLIB 那条线的开场是 website/docs-smtlib/01 - logic/02 - basiccommands.md，里面的例子长这样：
(declare-const a Int)
(declare-fun f (Int Bool) Int)
(assert (< a 10))
(assert (< (f a true) 100))
(check-sat)（这是 01 - logic/02 - basiccommands.md 里的原例，README 同一节更前面还有一个带 (echo "starting Z3...") 头的版本。）
这是求解器自己的语言：declare-const 声明常量，declare-fun 声明函数，assert 给约束，check-sat 求解。求解器是主角，代码是给它看的。
而 Programming Z3 那条线走的是 z3-js 和 z3-py 两种代码块 —— README 里明确写着 “Programming Z3 in other language bindings is not supported at the moment“，目前就这两种。另外 README 还区分了两种 Python 片段的用途：标 z3-py 的支持输出渲染和代码编辑，而 z3-python 用于只读的、依赖上下文片段或浏览器不支持的特性。
所以”分开学”落到实处是三件事：SMTLIB 那条线读的是语言本身（怎么把问题写成约束），Programming 那条线读的是怎么在宿主语言里驱动求解器，而参数参考页是查的、不是读的。
那 940 次提交里有多少是内容？ 我抽样统计了最近 50 个 commit（GitHub 官方 API，2026-11-01 拉取；归类规则与逐条归类见参考来源，便于复核）：
| 类型 | 条数 | 占比 |
|---|---|---|
| 依赖升级 | 35 | 70% |
| 教程/文档内容 | 6 | 12% |
| 参数文档自动更新 | 5 | 10% |
| CI/工作流基建 | 3 | 6% |
| 其它 | 1 | 2% |
七成是依赖升级。这个仓库不是”有人在持续写教程”，而是自动化在持续维护 —— 手写内容大约只占两成，其余是机器干的活。
这个比例反过来解释了几件事：为什么它有 940 次提交却不会显得嘈杂（绝大多数提交碰的是 website/package.json 这类文件，不影响正文）；为什么 “Update Z3 parameters for z3-5.3.3” 这类条目会稳定出现（那是 workflow 每天跑出来的）；也为什么”教程更新频率”不该从这个仓库的活跃度去推断 —— 它活跃，但活跃的是依赖机器人。
“生成”和”手写”混在一起，是这套维护模式的代价
现在能把两件事对上了：参数/tactic/simplifier 参考页是生成的，教程章节是手写的。仓库里同时存在这两类内容，而 commit 统计显示它们由完全不同的机制在维护 —— 手写那部分靠人提 PR，生成那部分靠 workflow 每天自动开 PR（”Automate Z3 parameter documentation updates” 就是那个 workflow 的落地提交）。
这种混合的代价是明确的：
好处是版本不脱节。参考页由 Z3 自己的代码生成，参数一改文档就跟着改，不存在手写文档常见的”这个参数早就废弃了但说明还在”。
代价是阅读时容易混。同一个站点里，有的页面是”人写的、可能过时”，有的是”机器按最新版本生成的、可能比你手上的求解器新”。刚才说的 5.0.0 与 5.3.3 的落差就是这个代价的具体表现 —— 而且它不会消失，只会随上游发版节奏持续拉大。
使用上的对策很朴素：查参数看参考页，但以你实际使用的求解器版本为准去验证；读教程时留意它锁定的版本，别把教程里的行为当成当前版本的保证。
用它之前先想清楚的三处代价
其一是覆盖面。README 只承诺一份 SMTLIB 教程和一份 Programming Z3，而 Programming Z3 里的语言绑定目前只支持 z3-js 和 z3-py 两种，README 明确写了其它语言绑定暂不支持（这一点 README 里有原文，不需要进站确认）；除此之外的主题不在这份清单里——这是我照 README 的口径推的，不是官方声明”不做”。想学求解器理论推导或性能调优，别把它当唯一入口。
其二是版本同步。Manually Updating z3-solver 这一条说明求解器版本要手动跟进（推导见上一节）。写进自己项目时，最好记下教程对应的 z3-solver 版本，否则示例结果对不上会浪费不少时间。
其三是求助成本。快照里 Issues 显示 13、watchers 只有 5，仓库导航里另有 Discussions 入口。提问前先搜 issue 和讨论区，别拿 star 数当响应速度的保证——这是我的经验判断，不是官方说法。
参考来源
评论区
登录后可评论。