# Rei-Solver

Rei-AIOS が「自分より正確かつ厳密な道具」を呼び出すための統合層。
Z3（SMT）・SymPy（数式処理）・PySAT（SAT/MaxSAT）を単一の非同期 I/F で包む。

詳しい設計は [SPEC.md](SPEC.md)。Claude Code に追加実装を投げるときはそちらを渡す。

---

## 30 秒で動かす

```bash
pip install -r requirements.txt          # z3-solver, sympy, python-sat
python -m rei_solver.harness             # 既知解 21 ケースで健全性確認
```

`ALL GREEN: 21/21 cases passed` が出れば準備完了。

```bash
python -m unittest discover -s tests     # 統合テスト 24 件
```

---

## 使い方

### Python から

```python
from rei_solver.api import solver_run, solver_submit, solver_poll

# 恒真性の証明
job = solver_run("z3", "prove", {
    "declarations": "(declare-const x Int)(declare-const y Int)",
    "conjecture": "(= (* (+ x y) (+ x y)) (+ (* x x) (* 2 x y) (* y y)))",
})
job["result"]["proved"]       # True
job["result"]["assurance"]    # "proof"  ← 機械証明された

# 長い計算は非同期で
sub = solver_submit("pysat", "solve_cnf", {"clauses": [...]}, timeout_s=3600)
solver_poll(sub["job_id"])    # あとから何度でも
```

### TypeScript から

```ts
import { ReiSolverBridge, isProved } from "./bridge/reiSolverBridge";

const solver = new ReiSolverBridge();
const job = await solver.run("z3", "circuit_equivalence", {
  inputs: ["a", "b"],
  circuit_a: { gates: [{ op: "xor", out: "y", args: ["a", "b"] }], outputs: ["y"] },
  circuit_b: { gates: [/* NAND 4 段 */], outputs: ["y"] },
});
if (isProved(job)) { /* 等価性が証明された */ }
```

常駐プロセスは不要。ジョブ状態は SQLite に永続化されている。

### MCP サーバとして

```bash
python -m rei_solver.server               # stdio JSON-RPC
```

Rei 側の MCP 設定に追加する場合:

```json
{
  "mcpServers": {
    "rei-solver": {
      "command": "python3",
      "args": ["-m", "rei_solver.server"],
      "env": { "PYTHONPATH": "/path/to/rei-solver" }
    }
  }
}
```

---

## 公開ツール

| ツール | 用途 |
|---|---|
| `solver_capabilities` | エンジン・操作・保証レベルの一覧。まずこれを見る |
| `solver_validate` | 実行せず入力だけ検査（**投入前に必須**） |
| `solver_submit` | 非同期投入。`job_id` を即返す |
| `solver_poll` | 状態・結果の取得 |
| `solver_run` | submit+poll の糖衣。数秒で終わる問題のみ |
| `solver_cancel` | プロセスグループごと停止 |
| `solver_jobs` | ジョブ一覧 |
| `solver_verify` | 既知解ハーネス実行 |

---

## 最重要の 2 点

**1. 結果の `assurance` を必ず見ること。**

| 値 | 意味 |
|---|---|
| `proof` | 機械証明。反証が存在しないことが確定 |
| `witness` | 証拠つき。第三者が独立に検算できる |
| `numeric` | 数値近似。誤差と収束条件に依存 |
| `heuristic` | 打ち切り等。**保証なし** |

`proof` と `heuristic` を取り違えると、この層を挟む意味が消える。

**2. 投入前に `solver_validate` を通すこと。**

ソルバは入力を疑わない。設定を間違えても、もっともらしい数値を
自信満々に返す。LLM が入力を組み立てる以上、ここが唯一の防御線になる。

---

## 回路化パイプラインとの接続

ファイル解析 → 制約抽出 → SMT の順で、解析結果を機械的に反証できる。

```
ファイル解析 ──> 回路化 ──> circuit_equivalence（参照実装と比較）
                              ├── equivalent=true,  assurance=proof   → 解析結果は正しい
                              └── equivalent=false, counterexample_input → どの入力で壊れるか判明
```

推測ではなく証明になる。`z3.circuit_equivalence` はこのために用意してある。

---

## ファイル構成

```
rei-solver/
├── SPEC.md                     設計仕様書（Claude Code 用）
├── README.md
├── requirements.txt
├── rei_solver/
│   ├── api.py                  唯一のツール面
│   ├── jobs.py                 SQLite ジョブストア・プロセス管理
│   ├── worker.py               supervisor / child 2 プロセス実行
│   ├── registry.py             エンジンのルーティング
│   ├── harness.py              既知解ハーネス
│   ├── server.py               MCP stdio サーバ（依存ゼロ）
│   ├── cli.py                  単発 CLI（TS ブリッジ用）
│   └── engines/
│       ├── base.py             Engine 契約
│       ├── z3_engine.py
│       ├── sympy_engine.py
│       └── pysat_engine.py
├── bridge/
│   └── reiSolverBridge.ts      TypeScript ブリッジ
└── tests/
    └── test_rei_solver.py      統合テスト 24 件
```

## 次に足すもの

Lean 4 → OpenMM → PySCF → FEniCSx → OpenFOAM の順を推奨。
手順と障壁は [SPEC.md §6](SPEC.md) に記載。

## 制約

Linux / macOS / WSL。`os.killpg` と `fork` に依存するため Windows では動かない。