Z3 SMT 求解器引擎

Z3 是由微软研究院（Microsoft Research）开发的定理证明器与可满足性模理论（SMT, Satisfiability Modulo Theories）求解器。在 WaSHI 中，Z3 提供强大的命题逻辑推理与不可行模型的冲突诊断（Unsat Core 提取）能力。

---

安装

Z3 作为可选的 peer dependency 提供：

npm install z3-solver

---

何时选择 Z3？

1. Unsat Core 冲突诊断： 当你的 MIP 或规则模型不可行（Infeasible / Unsat），需要定位究竟是哪些命名约束相互矛盾时。
2. 布尔逻辑与规则引擎建模： 当问题包含复杂的逻辑关系（如蕴含 implies、异或 xor、取反 not 以及嵌套布尔表达式与算术约束的混合）时。
3. 精确数学保证： Z3 支持精确有理数运算，能够避免浮点舍入误差带来的精度问题。

TIP

Z3（m.check()）与 HiGHS（m.solve()）的分工建议：Z3 最擅长可满足性判定（m.check()）、安全与业务策略的形式化验证、以一般线性不等式为前提的逻辑蕴含（implies(expr`${x} <= 50`, y)）以及与量纲无关的 unsatCore 提取。而对于包含数十至上千个变量的目标函数数值优化（LP、MIP、凸 QP），内置的 HiGHS（m.solve()）凭借单纯形松弛、割平面与分支定界算法，速度比 Z3.Optimize 快几个数量级。在工程实践中，也可以将两者结合：用 Z3 m.check() 进行策略验证与冲突诊断，再用 HiGHS m.solve() 求解最优成本。

---

基本用法

import { Model, expr } from "@ohtaman/washi";
import "@ohtaman/washi/solvers/z3";

const model = new Model({ solver: "z3" });

const x = model.integer("x", { lb: 0, ub: 10 });
const y = model.integer("y", { lb: 0, ub: 10 });

model.constraint(expr`${x} + ${y} == 15`, "sum_15");
model.constraint(expr`${x} >= 8`, "x_at_least_8");

await model.solve();
console.log(`x = ${x.value}, y = ${y.value}`);

---

提取不可行冲突核心 (model.check())

配合 Z3 使用 await model.check() 可以检验模型的可满足性，并在模型不可满足（"Unsat"）时提取相互冲突的命名约束子集（conflicts / unsatCore）：

const model = new Model({ solver: "z3" });
const a = model.continuous("a");

model.constraint(expr`${a} >= 10`, "req_A");
model.constraint(expr`${a} <= 5`, "req_B");

const result = await model.check();

if (result.status === "Unsat") {
  console.log("冲突的约束:", result.conflicts); // 或 model.conflicts / model.unsatCore
  // ["req_A", "req_B"]
}

---

浏览器安全要求（跨源隔离）

在浏览器环境中，Z3 WASM 引擎依赖 pthreads 多线程与 SharedArrayBuffer，因此需要配置跨源隔离响应头（COOP / COEP）。详细配置步骤请参阅 跨源隔离配置指南。

运行时故障恢复与线程清理

如果 Z3 Worker 遇到致命的运行时错误，该实例上挂起的操作将显式 reject 并抛出错误，同时损坏的运行时实例会被作废（不会将运行时错误误判为 Sat 或 Unsat）；后续调用 solve() 或 check() 时会自动初始化全新的 Z3 运行时。

在卸载浏览器视图或销毁工作线程池时，若需显式终止 Z3 的 pthread Worker 线程，可从 @ohtaman/washi/solvers/z3 导入并调用 killZ3Threads()。