企业官网建设流程全解析

Z3 TypeScript 绑定新 API 实战指南：Params、ParamDescrs 与 Simplifier 详解

【免费下载链接】z3The Z3 Theorem Prover项目地址: https://gitcode.com/gh_mirrors/z3/z3

本篇指南聚焦 Z3 定理证明器 TypeScript 绑定（src/api/js）中新增的三组高阶 API——Params（参数配置对象）、ParamDescrs（参数自省与文档）、Simplifier（面向增量求解的现代预处理组件，Z3 4.12+ 引入）。这三组 API 将 TypeScript 绑定的能力对齐到 Python、Java、C#、C++ 绑定水平，让开发者能以类型安全、可复用、可验证的方式配置 tactic 与 simplifier，并把预处理流水线直接挂载到 Solver 上。读完本文，你将掌握参数对象的创建与校验、参数的自省式文档查询，以及如何用 Simplifier 编排增量求解的预处理管线，并理解每一层 API 背后对应的 C 语言实现。

背景：TypeScript 绑定为何需要这三组 API

Z3 的 TypeScript 绑定（src/api/js）通过 Emscripten 将 Z3 核心编译为 WASM，在高阶封装层（src/api/js/src/high-level/high-level.ts）中为 JS/TS 开发者提供面向对象接口。在新 API 出现之前，TypeScript 绑定存在明显的能力缺口：

• 参数配置只能通过全局的setParam(key, value)设置，无法构造可复用、可组合的参数对象；
• 没有 simplifier 支持，增量求解场景下缺乏高效的预处理手段；
• 无法在运行时自省某个 tactic 或 simplifier 接受哪些参数、参数类型是什么、文档如何。

这些缺口在社区讨论 #8145 中被系统性地指出（详见 TYPESCRIPT_API_ENHANCEMENTS.md）。为此，绑定新增了三个高层次的 API：

1. Params—— 参数配置对象，以类型化值（布尔、数字、字符串）描述配置；
2. ParamDescrs—— 参数描述集合，提供参数的自省与文档查询；
3. Simplifier—— 现代预处理组件，专为增量求解设计，可组合、可配置、可挂载到 Solver。

这三个类在源码中均有对应实现：ParamsImpl、ParamDescrsImpl、SimplifierImpl，定义于 high-level.ts，其 TypeScript 接口声明位于 types.ts。

Params API：可复用的参数配置对象

Params用于创建可复用的参数配置对象，可传递给 tactic、simplifier 与 solver。核心特性：

• 以类型化值（boolean、number、string）设置参数；
• 通过tactic.usingParams(params)应用到 tactic；
• 通过simplifier.usingParams(params)应用到 simplifier；
• 通过validate(descrs)对照参数描述进行合法性校验；
• 通过toString()输出便于调试的字符串表示。

基本用法

const { Params, Tactic } = Context('main'); // 创建参数对象 const params = new Params(); params.set('elim_and', true); // 布尔值 params.set('max_steps', 1000); // 整数（内部走 uint 通道） params.set('timeout', 5.0); // 浮点数（内部走 double 通道） params.set('logic', 'QF_LIA'); // 字符串（内部走 symbol 通道） // 与 tactic 配合使用 const tactic = new Tactic('simplify'); const configuredTactic = tactic.usingParams(params); // 校验参数是否合法 const paramDescrs = tactic.paramDescrs(); params.validate(paramDescrs); // 非法参数会抛出异常 // 调试输出 console.log(params.toString());

类型化赋值的底层细节

Params.set(name, value)在底层会根据值的运行时类型选择不同的 C API。查看 high-level.ts 中的 ParamsImpl 可以确认这一分派逻辑：

• boolean→Z3.params_set_bool；
• number且为整数（Number.isInteger）→Z3.params_set_uint；
• number且为浮点 →Z3.params_set_double；
• string→Z3.params_set_symbol（参数名与值均转为 Z3 symbol）。

同样的分派逻辑也复用于_toParams辅助函数（供Solver.set等场景使用）。这意味着你不需要关心底层参数类型的区分，绑定会自动选择合适的编码通道；同时set的类型签名也限定了只接受boolean | number | string，从类型层面杜绝了传错类型。

API 参考

class Params { /** * 以给定的名字和值设置一个参数。 * @param name - 参数名 * @param value - 参数值（boolean、number 或 string） */ set(name: string, value: boolean | number | string): void; /** * 对照参数描述集合校验当前参数集。 * @param descrs - 用于校验的参数描述 */ validate(descrs: ParamDescrs): void; /** * 将参数集转换为字符串表示。 */ toString(): string; }

validate的语义是：若参数集中存在目标（tactic/simplifier）不认识的参数名或类型不匹配的值，则会抛出异常。其底层直接调用Z3_params_validate（声明于 z3_api.h），把错误检测前置到配置阶段，避免在求解时才暴露问题。

ParamDescrs API：参数的运行时自省

ParamDescrs提供对 tactic、simplifier、solver 可用参数的运行时自省：查询参数数量、名称、类型、文档，并用于校验Params配置。核心特性：

• 查询可用参数列表；
• 获取参数类型（kind）；
• 访问参数文档；
• 校验参数配置。

基本用法

const { Simplifier } = Context('main'); // 获取参数描述 const simplifier = new Simplifier('solve-eqs'); const paramDescrs = simplifier.paramDescrs(); // 自省参数 const size = paramDescrs.size(); console.log(`Number of parameters: ${size}`); for (let i = 0; i < size; i++) { const name = paramDescrs.getName(i); const kind = paramDescrs.getKind(name); const doc = paramDescrs.getDocumentation(name); console.log(`${name}: ${doc}`); } // 一次性输出全部 console.log(paramDescrs.toString());

getKind返回的是数字，对应底层 C API 的Z3_parameter_kind枚举（如整数、布尔、双精度浮点、符号、字符串等参数类别）。如果你需要判断某参数的类型，可以结合该枚举值做分支处理；getDocumentation则返回该参数的说明文字，适合构建参数帮助面板或交互式工具。

API 参考

class ParamDescrs { /** * 返回描述集合中的参数个数。 */ size(): number; /** * 返回给定索引处参数的名称。 * @param i - 参数索引 */ getName(i: number): string; /** * 返回给定名称参数的类型（kind）。 * @param name - 参数名 */ getKind(name: string): number; /** * 返回给定名称参数的文档字符串。 * @param name - 参数名 */ getDocumentation(name: string): string; /** * 将参数描述集合转换为字符串表示。 */ toString(): string; }

在实现层面，ParamDescrsImpl 分别包装了Z3_param_descrs_size、Z3_param_descrs_get_name、Z3_param_descrs_get_kind、Z3_param_descrs_get_documentation、Z3_param_descrs_to_string等底层调用，并通过FinalizationRegistry自动管理param_descrs_inc_ref/param_descrs_dec_ref的引用计数，无需手动释放。

Simplifier API：面向增量求解的现代预处理

Simplifier是 Z3 4.12 引入的现代预处理组件，专为增量求解设计，比传统 tactic 更高效，并且可以直接挂载到 solver 上。核心特性：

• 按名称创建 simplifier；
• 用andThen()组合多个 simplifier；
• 用usingParams()配置参数；
• 挂载到 solver 进行增量预处理；
• 获取帮助文本与参数文档。

完整示例：组合 Simplifier 并挂载到 Solver

const { Simplifier, Solver, Params, Int } = Context('main'); // 创建 simplifier const simplifier = new Simplifier('solve-eqs'); // 获取帮助文档 console.log(simplifier.help()); // 用参数配置 const params = new Params(); params.set('som', true); const configured = simplifier.usingParams(params); // 组合 simplifier：先 solve-eqs，再 simplify const s1 = new Simplifier('solve-eqs'); const s2 = new Simplifier('simplify'); const composed = s1.andThen(s2); // 挂载到 solver const solver = new Solver(); solver.addSimplifier(composed); // 正常使用 solver const x = Int.const('x'); const y = Int.const('y'); solver.add(x.eq(y.add(1))); solver.add(y.eq(5)); const result = await solver.check(); // 'sat' if (result === 'sat') { const model = solver.model(); console.log('x =', model.eval(x).toString()); // 6 }

在这个例子中，solver.addSimplifier(composed)之后，solver 会在增量断言（solver.add(...)）提交时自动执行组合预处理：先解方程（solve-eqs），再做常规化简（simplify），随后才进入求解阶段。对于需要反复push/pop、多次check()的增量场景，这种模式比每次手动应用 tactic 更高效，也保持了代码的声明式表达。

API 参考

class Simplifier { /** * 按名称创建 simplifier。 * @param name - 内置 simplifier 名称（如 'solve-eqs'、'simplify'） */ constructor(name: string); /** * 返回该 simplifier 接受的参数说明字符串。 */ help(): string; /** * 返回该 simplifier 的参数描述集合。 */ paramDescrs(): ParamDescrs; /** * 返回一个使用给定配置参数的 simplifier。 * @param params - 用于配置 simplifier 的参数 */ usingParams(params: Params): Simplifier; /** * 返回先应用本 simplifier、再应用另一个 simplifier 的组合结果。 * @param other - 在本 simplifier 之后应用的 simplifier */ andThen(other: Simplifier): Simplifier; }

usingParams与andThen都遵循不可变组合语义：它们不修改原对象，而是返回新的 simplifier。这在 SimplifierImpl 中体现得很清楚——usingParams调用Z3_simplifier_using_params生成新实例，andThen调用Z3_simplifier_and_then生成组合实例，二者均返回全新的SimplifierImpl。测试用例也验证了这一点：expect(configuredSimplifier).not.toBe(simplifier)（见 high-level.test.ts 的 "Simplifier API" 测试分组）。

Solver 集成：addSimplifier

Solver类新增了一个方法用于挂载 simplifier：

class Solver { /** * 为增量预处理挂载一个 simplifier。 * solver 将使用该 simplifier 对断言进行增量预处理。 * @param simplifier - 要挂载的 simplifier */ addSimplifier(simplifier: Simplifier): void; }

实现上，SolverImpl.addSimplifier 直接包装Z3_solver_add_simplifier（声明于 z3_api.h）。注意该方法要求传入的 simplifier 与 solver 属于同一 Context，否则会抛出上下文不匹配异常（_assertContext检查）。

Tactic 增强：usingParams 与 paramDescrs

Tactic类同步得到了参数配置能力的增强：

class Tactic { /** * 返回一个使用给定配置参数的 tactic。 * @param params - 用于配置 tactic 的参数 */ usingParams(params: Params): Tactic; /** * 获取 tactic 的参数描述。 * 返回一个 ParamDescrs 对象，用于自省可用参数。 */ paramDescrs(): ParamDescrs; }

示例

const { Tactic, Params } = Context('main'); const tactic = new Tactic('simplify'); const params = new Params(); params.set('max_steps', 100); const configured = tactic.usingParams(params);

TacticImpl.paramDescrs 调用Z3_tactic_get_param_descrs，TacticImpl.usingParams 调用Z3_tactic_using_params（后者声明于 z3_api.h），两者都会返回新的TacticImpl实例。此外Tactic.help()可输出该 tactic 的参数帮助，Tactic.solver()可基于当前 tactic 构造一个 solver，便于在 tactic 与 solver 两种模式间切换。

值得说明的是，Tactic.paramDescrs()+Params.validate()的组合构成了一个非常实用的开发流程：先自省得到参数描述，再构造参数对象并校验，最后才应用到 tactic 或 simplifier。相关测试覆盖了"对合法参数 validate 不抛异常"的场景（high-level.test.ts）。

可用的内置 Simplifier

常见的内置 simplifier 包括：

使用simplifier.help()可以查看每个 simplifier 的文档及其可接受参数；使用simplifier.paramDescrs()则可以程序化地遍历这些参数。由于 Z3 内置 simplifier 集合随版本演进，建议在运行时通过help()/paramDescrs()动态发现可用项，而不是硬编码参数名。

迁移指南：从全局 setParam 到 Params + Simplifier

之前（使用全局 setParam）

// 全局参数设置 setParam('pp.decimal', true); // 无法创建可复用的参数配置 // 不支持 simplifier

全局setParam的问题在于：参数是进程/上下文级的全局状态，无法针对不同 tactic 精细配置，也无法复用、组合或校验。

之后（使用 Params 与 Simplifier）

// 可复用的参数对象 const params = new Params(); params.set('pp.decimal', true); params.set('max_steps', 1000); // 配置 tactic const tactic = new Tactic('simplify').usingParams(params); // 使用 simplifier 提升增量求解质量 const simplifier = new Simplifier('solve-eqs').usingParams(params); solver.addSimplifier(simplifier);

注意setParam仍然可用（用于全局参数，例如打印格式pp.decimal），而Params适用于需要细粒度、可复用、可校验的组件级配置。两者定位不同，可按需混用。全局参数相关能力（setParam、getParam、resetParams）在 high-level.ts 中有完整实现。

兼容性与多语言对齐

这三组 API 在功能上与 Z3 其他语言绑定完全对齐：

• ✅ Python（ParamsRef、ParamDescrsRef、Simplifier）
• ✅ Java（Params、ParamDescrs、Simplifier）
• ✅ C#（Params、ParamDescrs、Simplifier）
• ✅ C++（params、param_descrs、simplifier）

TypeScript 绑定现已覆盖 Params、ParamDescrs、Simplifier 三个 C API 模块的全部功能。换句话说，如果你熟悉任意一种 Z3 语言绑定的参数与 simplifier 用法，可以几乎无缝迁移到 TypeScript。

完整可运行示例与测试

仓库提供了完整的可运行示例 simplifier-example.ts，它演示了六组用法：

1. 创建并使用Params（含elim_and、max_steps、timeout等参数与toString()输出）；
2. 创建并使用Simplifier（含help()输出）；
3. 用andThen()组合 simplifier；
4. 用usingParams()配置 simplifier 与 tactic；
5. 将 simplifier 挂载到Solver并求解x = y + 1, y = 5得到模型；
6. 遍历ParamDescrs输出参数数量、首个参数名及其文档。

运行方式（在src/api/js目录下）：

# 安装依赖并构建 WASM 绑定 npm install npm run build # 运行示例 npx ts-node examples/high-level/simplifier-example.ts # 运行测试（含 Params / Simplifier API 测试分组） npm test

对应的单元测试位于 high-level.test.ts 的 "Params API"（约 L2144 起）与 "Simplifier API"（约 L2216 起）两个describe分组中，覆盖了参数设置、校验、自省、组合、配置以及 solver 集成等关键路径，是验证行为与阅读实现的极佳入口。TypeScript 绑定的整体使用说明可参阅 src/api/js/README.md。

小结

Params、ParamDescrs、Simplifier 三组 API 补全了 Z3 TypeScript 绑定在组件配置与增量预处理上的能力：Params提供类型安全、可复用、可校验的配置对象；ParamDescrs把参数文档与类型暴露给运行时，支撑自省式工具与动态校验；Simplifier则以可组合、可挂载的方式为增量求解提供高效预处理。三者共同将 TypeScript 绑定提升到与 Python、Java、C#、C++ 一致的能力水平，是构建复杂、增量式 Z3 应用的推荐基座。

【免费下载链接】z3The Z3 Theorem Prover项目地址: https://gitcode.com/gh_mirrors/z3/z3