# 公开 API 契约

本文件面向调用方：每个包对外承诺什么、什么情况下返回哪个状态、哪些字段在哪些状态下有意义。
它只写代码里已经成立的事——`.mbti` 里出现的就是契约，`.mbti` 里没出现的就是内部实现。
生成 `.mbti` 的命令是 `moon info`，任何公开面变化都会让它出现 diff，提交前看一眼这个 diff 就知道
自己的改动有没有碰到承诺面。

## 顶层包 `Freon793/moonopt`（`moonopt.mbt`）

```moonbit
pub fn solve(model : @model.Model) -> Solution
pub fn solve_with(model : @model.Model, options : SolveOptions) -> Solution

pub(all) struct SolveOptions { max_iterations, presolve, max_nodes, cut_rounds }
pub struct Solution { status, values, objective, iterations, nodes, bound, gap, message }
pub(all) enum SolveStatus { Optimal, Infeasible, Unbounded, NodeLimit, NotSolved }
```

| 规则 | 说明 |
| --- | --- |
| 整数模型走分支定界，**不做化简** | 答案不能取决于化简碰巧定住了什么；`presolve` 选项对整数模型不生效 |
| 只承认搜索证明过的结论 | `MipStatus::Optimal` / `Infeasible` → 同名公开状态；节点预算到顶 → `NodeLimit` |
| 三类情况一律 `NotSolved` 并带原话 | 松弛无界（改善射线不含整数性）、证书被拒（那是关于内核的陈述，不是关于模型的结论）、模型非法；另加"量到违反却写不出不可行证书"——Phase I 的人工和不足以解释它要证明的违反量 |
| `values` 非空时才有 `objective` | 预算到顶且没找到整数点时 `objective` 为 0，`message` 用文字说明"还没有整数点" |
| `bound` / `gap` 在所有路径同义 | 线性求解下 `bound = objective`、`gap = 0`（线性解就是它自己的界）；`NodeLimit` 下是仍在开的界 |

**状态口径与外部标准**：外部参照是 MathOptInterface 的 `TerminationStatusCode`。逐条比较过之后只有一处
是实质差异：MOI 有 `ITERATION_LIMIT`，本项目的公开面**没有**枢轴上限用尽这个状态，它与数值失败、规模
拒绝、非法模型一起归入 `NotSolved`。这是刻意的——本项目的口径是"只承认证明过的结论"，而"没解完"不是
结论；MIP 侧给 `NodeLimit` 是因为那里还有**当前整数点**与**仍在开的界**两个可用数字，线性侧没有。
其余 MOI 状态要么同义、要么对应本项目的功能不存在（不做时间预算、不做并行、没有中断通道），
要么是刻意的合并。

## `model`：模型层

`Model`（变量、约束、目标、sense）+ `Var` / `Constraint` 视图 + `validate`（返回人类可读的问题列表）。

```moonbit
pub fn Model::add_var(self, name : String, lb? : Double = 0.0, ub? : Double = infinite_bound,
                      is_int? : Bool = false) -> Int
```

- `infinite_bound` 是无穷界的哨兵（`±1e30` 量级，不是 IEEE 无穷——有界变量枢轴需要一个可比大小的界）。
- `Model::validate` 只判**结构**合法性（下标越界、NaN、`lb > ub` 等），不判数学可行性；数学结论由内核
  或分支定界给出。

## `core`：数值与稀疏基础设施

`approx_eq` / `approx_zero` / `approx_positive` / `approx_negative`（容差感知比较）、
`CompensatedSum`（Neumaier 补偿求和）、`SparseMatrix`（CSC，不存结构零、列内行号升序）、
`fabs` / `fmax` / `fmin`。

契约：所有"是否为零 / 是否为正"的判断都走容差助手，不用 `==` 比较浮点。

## `format`：MPS / LP 读写

```moonbit
pub fn parse_mps(text) -> Result[Model, ParseIssue]
pub fn read_lp(text)   -> Result[Model, ParseIssue]
pub fn write_mps(model) -> String
pub fn write_lp(model)  -> String
pub fn format_number(value : Double) -> String
```

- `Err` 带**位置**（行 / 列）与人类可读原因；**读→写→读是幂等的**（同一个模型读进来、写出去、再读回来
  得到同一个模型）。
- 数字格式用最短往返表示（`Double::to_string`），**不在上面加一层取整**——读回来的数与写出去的数逐位
  相同。CLI 的 JSON 输出用同一条政策。
- 全量真实数据的解析结果见 [`../bench/parse-report.md`](../bench/parse-report.md)（32 个实例全部成功）。

## `simplex`：稀疏修正单纯形内核

```moonbit
pub fn solve_model(model) -> Result[SimplexResult, String]
pub fn solve_model_with(model, options) -> Result[SimplexResult, String]
pub fn solve_model_with_basis(model, options, basis) -> Result[SimplexResult, String]
pub fn solve_standard(num_vars, cost, rows) -> SimplexResult
pub fn tableau_rows(model, options, basis) -> Result[Array[TableauRow], String]
```

- **`Err` 与状态的分工**：`Err` 表示模型**不在内核受理范围内**（整数变量、无法构造标准形），不是
  "没解出来"；后者由 `SimplexStatus` 表达：`Optimal` / `Infeasible` / `Unbounded` / `IterationLimit` /
  `NumericalFailure` / `TooLarge`。
- **`NumericalFailure` 的含义**：内核**有答案但证据不成立**时选择不报（行残差、变量界、非负性、行乘子
  符号约定、对偶间隙任一项过不了自检），而不是给一个看起来合理的解。恢复梯子（Bland 重启 → 去掉退化
  微扰 → 换定价规则）会先试三条走法，仍失败才返回原始失败。
- **热启动**：`solve_model_with_basis` 只在基**对偶可行**时走对偶单纯形；形状不匹配、对偶可行性丢失、
  数值失败（含"基按检验数最优但证书写不出来"的拒签）一律回退冷启动——**热启动只是提速，永远不会给出
  不同的答案**。`SimplexBasis` 由上一次运行的 `SimplexResult::basis` 提供。

## `presolve`：模型化简与还原

```moonbit
pub fn presolve(model) -> ReducedModel
pub fn max_row_violation(model, x)   -> Double
pub fn max_bound_violation(model, x) -> Double
pub fn objective_value(model, x)     -> Double
```

- 每条归约**先证明再触发**；`ReducedModel::verdict()` 为 `Reduced` / `Infeasible` / `Unbounded`，
  后两者是化简自己证出来的结论，带 `reason()`。
- **还原必须被独立复核**：`reconstruct` 把化简解映回原变量，调用方**必须**用上面三个函数在**原模型**上
  量行违反、界违反与目标值——不能拿化简自己的记账当证据（`cmd/parse` 的 `reconstructed:` 一行就是这么
  做的）。

## `verify`：独立校验器

```moonbit
pub fn verify(model, certificate, tolerance? = 1e-7) -> Verdict
pub fn derive_cut(model, certificate, tolerance? = 1e-7) -> Result[CutRow, String]
pub fn verify_cut(model, cut, certificate, tolerance? = 1e-7) -> CutVerdict
pub fn Certificate::to_json(self) -> String
pub fn Certificate::from_json(text) -> Certificate?
```

- **乘子约定**（生产者必须按它写证书）：对行定义定向形式 gᵢ（`≤` 行为 `a·x − b`，`≥` / `=` 行为
  `b − a·x`），乘子 `y ≥ 0`（`=` 行自由）；于是下界 = `Σⱼ min over [lⱼ,uⱼ](rⱼxⱼ) + D`，最优性要求该下界
  等于点上的目标值，**Farkas 不可行证书就是同一式子取 `c = 0` 并要求严格为正**。推导写在
  `verify/verify.mbt` 的包文档里。
- **`verify` 不依赖 `simplex`**：`verify/moon.pkg` 的 import 就是证据——校验器与求解器不共享任何状态，
  这是"证书"这个词的意义。
- `Verdict` 带全部测量：`accepted` / `claim` / `reason`（第一处失败的原话）/ `checks`（逐项测量与容差）。
- **割的复核**：`verify_cut` 把割**重新推导一遍**（组合重现自称的行、基变量整数、有限界移位、小数部分
  按 `combination_noise` 判、割大于产生它的算术、与交上来的行逐项相同）；拒绝即停，不"跳过继续"。
- **证书只对内核收到的模型成立**：`--verify` 因此不化简（化简模型的乘子不是原模型的乘子）。

## `mip`：分支定界

```moonbit
pub fn solve_mip(model, options) -> MipResult

pub(all) enum MipStatus { Optimal, Infeasible, NodeLimit, UnboundedRelaxation, Unverified, Invalid }
pub(all) struct MipOptions { max_nodes, max_iterations, tolerance, verify_nodes,
                             dive_steps, dive_attempts, cut_rounds, primal_rounding,
                             node_solver, cut_hook }
```

| 规则 | 说明 |
| --- | --- |
| 每个节点的松弛都过 `verify` | `verified` 是这件事的计数；开启校验时 `nodes − verified` 恰好是"无结论的松弛"数 |
| 证书被拒**停整轮**为 `Unverified` | 不拿一个没人能复核的答案去分支；消息带校验器原话 |
| 松弛无界 ≠ 模型无界 | 报 `UnboundedRelaxation`，因为改善射线不含整数性 |
| 模型非法 ≠ 不可行 | 报 `Invalid` |
| `NodeLimit` 给出当前整数点与仍在开的界 | 两者一起才是调用方需要的（"能到多好"与"已经多好"）。界取自**全部开着的活**：队列里的节点，以及松弛到达不了结论、因此不再入队的那些节点所在的子树 |
| 割必须能被独立再推导 | 每条割带"由哪一行舍入而来"的证明，`verify_cut` 复核后才进模型 |
| 取整 / 修复 / 泵 / 下潜只**提供**当前解 | 四者各走同一条求解 + 校验路径、计入 `nodes` / `verified`、受同一预算约束，永不主张最优 |
| `nodes` 永不超过 `max_nodes` | 每个"花掉一次松弛"的地方都先问预算；`mip/mip_test.mbt` 里有模型 × 预算 1..8 的遍历断言 |
| `node_solver` / `cut_hook` 只给测试用 | 用来演示"做坏的松弛 / 割会被拒" |

## CLI（`cmd/parse`）

```
moon run cmd/parse -- <file> [flags]                # 巡检（默认）
moon run cmd/parse -- <verb> <file> [flags]         # verb ∈ parse|solve|verify|fmt|bench
```

- 文本输出是 `bench/` 四个脚本解析的格式，**逐位稳定**；`--json` 是同一批运行的另一份渲染，
  没跑出来的字段不出现。
- 退出码：解析失败、证书被拒、报告的点没通过复核 → 非零；**模型超出内核受理范围（`refused`）不算失败**。
- `fmt` 不给 `-o` 时只打印不落盘；`--json` 与 `--reoptimize` 的组合被显式拒绝（退出 2）。
- 证据：`cmd/parse/main_wbtest.mbt`；[`../bench/README.md`](../bench/README.md) 的脚本与拒绝条件说明。