# Z3 SMT Solver Engine

**Z3** is a theorem prover and Satisfiability Modulo Theories (SMT) solver developed by Microsoft Research. In WaSHI, Z3 provides advanced propositional logic reasoning and conflict diagnosis.

---

## Installation

Z3 is provided as an optional peer dependency:

```bash
npm install z3-solver
```

---

## When to Use Z3?

1. **Unsat Core Conflict Diagnosis**:
   When your MIP model is infeasible and you need to isolate which constraints are contradictory.
2. **Boolean / Logical Formulations**:
   When solving problems containing complex logical relations (implications, XOR, nested Boolean expressions).
3. **Exact Mathematical Guarantees**:
   Z3 can perform exact rational arithmetic without floating-point inaccuracies.

> [!TIP]
> **Z3 (`m.check()`) vs. HiGHS (`m.solve()`)**: Z3 excels at satisfiability checking (`m.check()`), formal policy verification, general inequality implications (`` implies(expr`${x} <= 50`, y) ``), and scale-invariant `unsatCore` extraction. For numerical LP, MIP, or Convex QP optimization with objective functions over tens or hundreds of variables, use the built-in **HiGHS** solver (`m.solve()`), whose simplex relaxations and branch-and-bound cutting planes are orders of magnitude faster than `Z3.Optimize`. Or combine both in a hybrid pipeline: verify/diagnose rules with Z3 `m.check()`, then optimize costs with HiGHS `m.solve()`.

---

## Basic Usage

```typescript
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}`);
```

---

## Unsat Core Extraction (`model.check()`)

Use `await model.check()` with Z3 to verify satisfiability and extract the conflicting subset of named constraints (`conflicts` / `unsatCore`) when a model is unsatisfiable:

```typescript
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("Conflicting constraints:", result.conflicts); // or model.conflicts / model.unsatCore
  // ["req_A", "req_B"]
}
```

---

## Browser Security Note

In browser environments, the Z3 WASM engine relies on pthreads and `SharedArrayBuffer`, which require cross-origin isolation headers (`COOP` / `COEP`). See the [Cross-Origin Isolation Guide](../getting-started/cross-origin.md) for detailed setup.

## Runtime Failures and Thread Cleanup

If a Z3 worker encounters a fatal runtime error, pending operations on that instance reject with an error and the broken runtime is invalidated; subsequent `solve()` or `check()` calls automatically initialize a fresh Z3 runtime rather than misclassifying failures as `Sat` or `Unsat`.

To explicitly terminate Z3 pthread workers when tearing down a browser view or worker pool, call `killZ3Threads()` from `@ohtaman/washi/solvers/z3`.