# WaSHI (@ohtaman/washi)

> WaSHI: WebAssembly-backed Algebraic Modeler for Mathematical Optimization & Constraint Programming (LP, MIP, QP, SMT)

**WaSHI** (WebAssembly-backed, Solver-independent, High-level modeling Interface) brings the algebraic modeling style of Python's **PuLP** to the TypeScript and JavaScript ecosystem.

- Full single-file documentation reference: [llms-full.txt](llms-full.txt)
- Canonical AI agent modeling quick-reference: [getting-started/ai-agents.md](getting-started/ai-agents.md)

---

## 1. Package Imports & Deployment

### Node.js / Bundlers (Vite, Webpack, Next.js, Bun)

```ts
import {
  Model,
  expr,
  sum,
  dot,
  maximize,
  minimize,
  and,
  or,
  not,
  implies,
  xor,
  setHighsWasmUrl,
} from "@ohtaman/washi";

// Optional solver plugins (require installing peer dependencies first):
// npm install z3-solver
import "@ohtaman/washi/solvers/z3";
// npm install glpk.js
import "@ohtaman/washi/solvers/glpk";
```

### Browser ESM & Classic Script Tags

- **Browser ESM**:
  - Core (HiGHS built-in): `import { Model, expr, maximize } from "./washi/washi.js";`
  - GLPK plugin: `import "./washi/solvers/glpk.js";`
  - Z3 plugin: `import "./washi/solvers/z3.js";`
- **Classic `<script>` / CodePen (IIFE)**:
  - Core: `<script src="./washi/washi.min.js"></script>` (exposes global `Washi`)
  - GLPK plugin: `<script src="./washi/solvers/glpk.min.js"></script>` (registers `"glpk"`, exposes `WashiGLPK`)
  - Z3 plugin: `<script src="./washi/solvers/z3.min.js"></script>` (registers `"z3"`, exposes `WashiZ3`)

### WebAssembly Asset & Runtime Rules

1. **Bundled WASM by default (no implicit CDN fallback)**:
   - In Node.js and modern bundlers, WebAssembly assets resolve relative to the module automatically.
   - In browser deployments, deploy the full `dist/browser/` directory (JS, Worker, and `.wasm` files) together. If a local WASM URL is missing or returns an HTML SPA fallback, initialization fails immediately and reports the attempted URL—it **never** silently switches to a public CDN.
   - In browser runtimes, to load `highs.wasm` from a custom location, call `setHighsWasmUrl("https://.../highs.wasm")` or pass `await m.solve({ wasmUrl: "https://.../highs.wasm" })` (ignored in Node.js, which always loads the local Node `highs` package runtime).
2. **Z3 requires a Secure Context, Cross-Origin Isolation, and CORS in browsers**:
   - Z3 WebAssembly uses `SharedArrayBuffer` multithreading. Browser pages running Z3 must run in a secure context (`window.isSecureContext === true`, i.e., HTTPS or `localhost`) and be cross-origin isolated (`window.crossOriginIsolated === true`) by serving:
     - `Cross-Origin-Opener-Policy: same-origin` (on the document)
     - `Cross-Origin-Embedder-Policy: require-corp` (on the document)
     - `Cross-Origin-Resource-Policy: cross-origin` and `Access-Control-Allow-Origin` (on cross-origin script/WASM asset responses)
   - Importing `@ohtaman/washi` never auto-injects a Service Worker. When a secure context or cross-origin isolation is absent in a browser, Z3 rejects immediately with a descriptive error.
3. **Web Workers & Cancellation (`AbortSignal`)**:
   - Pre-solve cancellation (`signal.aborted` before execution starts) is supported across all solvers.
   - In browsers where `Worker` is available, HiGHS runs in a dedicated Web Worker by default (`useWorker: true`). Passing `{ signal }` to `m.solve({ signal })` preemptively terminates an in-flight Worker solve (or cancels queued Worker requests).
   - On main-thread HiGHS (`useWorker: false` or in Node.js), cooperative mid-solve cancellation is supported when `abort()` is triggered synchronously inside an `onProgress` callback at a solver interrupt checkpoint; arbitrary asynchronous aborts from outside cannot preempt a blocked synchronous WASM thread until a callback checkpoint or completion. Single-threaded WASM solvers without interrupt hooks (GLPK, Z3) check `signal` before execution starts.

---

## 2. Canonical Modeling Workflow & Key Rules

Formulating and solving a model consists of four distinct steps:

### Step 1: Create Model & Decision Variables

```ts
const m = new Model("ExampleModel");

// Scalar variables
const x = m.continuous("x", { lb: 0, ub: 100 });
const n = m.integer("n", { lb: 0, ub: 10 });
const b = m.binary("b");
const flag = m.bool("flag"); // Propositional boolean (for Z3 / logical constraints)

// Indexed variable containers:
// - Numeric dimension -> Array
// - Key-array dimension -> Record
const vec = m.continuous(4, { lb: 0, prefix: "v" }); // Var[] (length 4)
const grid = m.binary(2, 3, { prefix: "g" }); // Var[][] (2x3)
const byItem = m.integer(["desk", "chair"] as const, { lb: 0 }); // Record<"desk" | "chair", Var>
const mixed = m.binary(["A", "B"] as const, 3); // Record<"A" | "B", Var[]>
```

- **Optional Primal Initial Values (`initialValue?: number`)**:
  - Numeric variable constructors (`m.continuous`, `m.integer`, `m.binary`, and `new Var`) and the mutable `v.initialValue` property accept an optional finite primal hint (validated with tolerance `1e-6` against bounds `[lb, ub]` and integer/binary domains), kept distinct from the solved `v.value`.
  - A start may be complete or partial (e.g., transferred by stable variable names when rebuilding a MIP model). Supplying `initialValue` is a hint only—it does **not** fix the variable, add a hard constraint, or guarantee solver acceptance or a runtime speedup.
  - Supported by **HiGHS** (`supportsWarmStart: true`); solvers without warm-start support (**GLPK**, **Z3**) throw an error if any variable has `initialValue !== undefined`.

### Step 2: Build Expressions (`expr`, `sum`, `dot`)

- **Unified `expr` template tag**:
  - Linear expression (`LinExpr`): `` expr`30 * ${x} + 50 * ${n} - 10` ``, `` expr`dot(${profit}, ${byItem}) - 20 * ${b}` ``, `` expr`sum((${price} - ${cost}) * ${byItem})` ``
  - Quadratic expression (`QuadExpr`): `` expr`${x}^2 + 2 * ${x} * ${n} + ${n}^2` ``, `` expr`sum((${vec} - ${target})^2)` `` (variable-by-variable products and squares are supported for convex QP objectives).
  - Linear constraint (`Constraint`): `` expr`${x} + 2 * ${n} <= 40` ``, `` expr`sum(${byItem}) <= 100` `` (supports `<=`, `>=`, `==`, and `=`).
- **Aggregations & Element-Wise Container Arithmetic**:
  - `sum(containerOrItems, mapper?)` (usable inside `` expr`sum(...)` `` or standalone `sum(...)`) sums a 1D/2D `Array`, `Iterable`, or plain `Record` of `Var` / `LinExpr` / `number` (without needing `Object.values(record)`), or maps over items/counts via `sum(items, (item, i) => ...)`. Inside `` expr`sum(...)` ``, element-wise container arithmetic (`+`, `-`, `*`, `/`, `^2`) is also supported.
  - `dot(a, b)` (usable inside `` expr`dot(${a}, ${b})` `` or standalone `dot(a, b)`) computes the inner product of matching 1D arrays, 2D arrays (`number[][]` / `Var[][]`, computing the Frobenius inner product $\sum_{i,j} A_{i,j} B_{i,j}$), plain records (`Record<string, ...>`), or mixed Array/Record containers in either operand order.
- **Fluent methods**:
  - Arithmetic (on `LinExpr` and `QuadExpr`; `Var` supports `.add()`, `.sub()`, `.mul()`, `.neg()`): `.add(other)`, `.sub(other)`, `.mul(other)`, `.div(scalar)`, `.neg()`
  - Comparisons (on `Var` and `LinExpr`): `.le(rhs, name?)`, `.ge(rhs, name?)`, `.eq(rhs, name?)`
  - Boolean logic (on `BoolVar`, `BoolExpr`, and `Constraint` for Z3): standalone `and(...)`, `or(...)`, `not(...)`, `implies(a, b)`, `xor(a, b)` and fluent `.and(...)`, `.or(...)`, `.not()`, `.implies(...)`, `.xor(...)`

### Step 3: Register Objective & Constraints on the Model

Constructing an `expr` or `.le()` object does **not** attach it to the model until you pass it to `m.constraint(...)` or `m.objective(...)`:

```ts
// Set objective using maximize() or minimize()
m.objective(maximize(expr`30 * ${x} + 50 * ${n}`));

// Register constraints on the model (returns the registered Constraint / BoolExpr or array)
const limit = m.constraint(expr`${x} + 2 * ${n} <= 40`, "resource_limit");

// Indicator constraint (MIP Big-M reformulation: b === 1 => x <= 50)
m.indicator(b, expr`${x} <= 50`, { activeValue: 1, name: "cap_when_b" });
```

### Step 4: Execute (`solve` or `check`) & Verify (`validateSolution`)

- **Optimization (`await m.solve(options?)`)**:
  - Returns `SolverStatus` (`"Optimal"`, `"Feasible"`, `"Infeasible"`, `"Unbounded"`, `"TimeLimit"`, `"IterationLimit"`, `"Error"`, `"Unknown"`, `"NotSolved"`, `"Sat"`, or `"Unsat"`). Built-in optimization solvers return the optimization statuses (`"Optimal"`, `"Feasible"`, `"Infeasible"`, `"Unbounded"`, `"TimeLimit"`, `"IterationLimit"`, `"Error"`, `"Unknown"`, `"NotSolved"`), where a time-, iteration-, or solution-limited run (or an interrupted solve) that found a valid primal incumbent returns `"Feasible"`; `"Sat"` and `"Unsat"` are included in `SolverStatus` for satisfiability/custom solver adapters (such as `MockSolver`).
  - Read values via `x.value`, `expr`...`.value`, `m.getValues(x)`, `m.getValues(container)`, `m.objectiveValue`, `constr.dual`, `constr.slack`, and `x.reducedCost`.
  - Call `m.validateSolution()` after solving to independently verify variable finiteness, variable bounds (`lb`/`ub`), integer/binary/boolean domains, linear constraint residuals, and logical constraints (`SolutionValidationReport`: `{ valid, complete, maxViolation, violations, ... }`). Note that `validateSolution()` checks primal feasibility of variables and constraints; it does not recompute or compare `m.objectiveValue`.
- **Satisfiability & Conflict Diagnosis (`await m.check(options?)`)**:
  - Returns `CheckResult` (`{ status: "Sat" | "Unsat" | "Unknown", values: Record<string, number | boolean>, conflicts?: readonly string[], unsatCore?: readonly string[], runTime?: number }`), where `conflicts` is populated when the model is proven `"Unsat"`.
  - For models containing linear arithmetic constraints or logical constraints (`BoolVar`, `and`, `or`, `implies`, `xor`), `m.check()` works with any solver (including the default HiGHS and GLPK via single-solve elastic slack relaxation, automatically linearizing logical constraints into 0-1 MIP formulation) and diagnoses conflicting constraints as `conflicts` (leaving `unsatCore: undefined` for semantic rigor).
  - Exact SMT unsatisfiable-core extraction (`result.unsatCore` and `result.conflicts`) is provided when using an SMT-capable solver (`{ solver: "z3" }`). Because Z3 asserts variable bounds (`lb`/`ub`) and binary `{0, 1}` domains directly while tracking registered constraints, `unsatCore` reports a subset of registered constraint names that conflicts *together with the model's fixed variable bounds/domains* (and is not guaranteed minimal).
- **No concurrent mutation during async solve/check**:
  - Mutating variables, constraints, or the objective while `await m.solve()` or `await m.check()` is pending invalidates the in-flight execution and rejects the stale promise.

---

## 3. Common Pitfalls & Retired Aliases

1. DO NOT pass a Constraint to m.objective() or arithmetic methods:
  - `` WRONG: m.objective(maximize(expr`${x} <= 10` as any)); -> throws Error ``
  - `` WRONG: expr`${x} + 1`.add(expr`${y} <= 5` as any); -> throws Error ``
2. DO NOT pass an arithmetic expression without (<=, >=, ==) to m.constraint():
  - `` WRONG: m.constraint(expr`${x} + ${y}` as any); -> throws Error ``
3. DO NOT use quadratic terms inside linear constraints:
  - `` WRONG: expr`${x}^2 <= 10`; -> throws Error ("Quadratic constraints are not supported") ``
4. DO NOT use retired aliases (removed in #59 / #81):
  - Use `expr` instead of retired `c` template tag
  - Use `m.constraint(...)` instead of `m.constrain(...)` or `m.add(...)`
  - Use `m.objective(maximize(...))` / `m.objective(minimize(...))` instead of `m.maximize(...)` / `m.minimize(...)` / `m.setObjective(...)`
  - Use `await m.solve()` instead of `await m.optimize()`
  - Use `.le()`, `.ge()`, `.eq()` instead of `.lessThanOrEqual()`, `.greaterThanOrEqual()`, `.equalTo()`
  - Use `.value` or `m.getValues(...)` instead of `expr.getValue()`
  - Use `m.variables` / `m.constraints` instead of `m.vars` / `m.constrs`

---

## 4. Canonical English Documentation Index

### Getting Started

- [AI Coding Agent Quick-Reference Guide](getting-started/ai-agents.md): This document is the **consumer modeling quick-reference** for AI coding agents and developers building optimization or satisfiability models with `@ohtaman/washi`.
- [Introduction & Installation](getting-started/index.md): **WaSHI** (WebAssembly-backed, Solver-independent, High-level modeling Interface) brings the algebraic modeling style of Python's **PuLP** to the TypeScript and JavaScript ecosystem.
- [Runtime Environments & Deployment](getting-started/runtimes.md): WaSHI runs across JavaScript and TypeScript runtimes—from Node.js, Bun, and Deno to modern bundlers, static hosting, and vanilla browser `<script>` tags—without native C/C++ compilation.
- [Cross-Origin Isolation (Z3 & Browsers)](getting-started/cross-origin.md): When running the **Z3** solver inside a web browser, Cross-Origin Isolation HTTP headers are required so the browser enables `SharedArrayBuffer`.

### Modeling Guide

- [Variables & Domains](guide/variables.md): Variables represent the mathematical decision variables in your optimization or logical model.
- [Expressions (`expr`, `sum`, `dot`)](guide/expressions.md): Mathematical expressions are linear or quadratic combinations of decision variables and numeric coefficients.
- [Constraints (`m.constraint` & `m.indicator`)](guide/constraints.md): Constraints restrict the feasible solution space of your mathematical or logical model.
- [Objectives & Solving (`m.solve` & `m.check`)](guide/objectives.md): The objective function defines the goal of mathematical optimization—whether to maximize profits, minimize costs, or minimize quadratic risk variance.
- [Conflict Diagnosis (`unsatCore`) & Solution Validation](guide/unsat-core.md): WaSHI provides built-in tools for both: **Unsat Core conflict diagnosis** via Z3 (`m.check()`), **independent solution validation** (`m.validateSolution()`), **LP formulation export** (`m.toLpString()`), and **fast unit testing** (`MockSolver`).
- [Decomposition Methods (`solveColumnGeneration` & `solveBenders`)](guide/decomposition.md): When monolithic Mixed-Integer Programming (MIP) models have exponentially many candidate patterns or large multi-stage subproblems, WaSHI provides two high-level decomposition orchestrators—`master.solveColumnGeneration()` and `master.solveBenders()`—along with low-level primitives for dual inspection and dynamic model updates.
- [Formulation Patterns & Optimization Tips](guide/formulation-tips.md): While the preceding Modeling Guide pages cover WaSHI's APIs (`Model`, `expr`, `m.constraint`, `m.solve`, etc.), this page collects standard mathematical optimization formulation patterns and solver tuning techniques frequently used in linear and mixed-integer programming (LP/MIP).

### Solvers

- [Solvers Overview](solvers/index.md): WaSHI is designed around a pluggable, decoupled solver architecture.
- [HiGHS Solver Engine](solvers/highs.md): **HiGHS** is high-performance mathematical optimization software developed at the University of Edinburgh (ERGO-Code/HiGHS).
- [Z3 SMT Solver Engine](solvers/z3.md): **Z3** is a theorem prover and Satisfiability Modulo Theories (SMT) solver developed by Microsoft Research.
- [GLPK Solver Engine](solvers/glpk.md): The **GNU Linear Programming Kit (GLPK)** is a long-standing, robust simplex and interior-point solver package intended for solving large-scale linear programming (LP) and mixed integer programming (MIP).
- [WaSHI Custom Solver Developer Guide](solvers/custom-solver.md): This guide describes how to build, test, and distribute custom solver plugins for **WaSHI** (`@ohtaman/washi`).

### Examples

- [Examples & API Finder](examples/index.md): Explore runnable optimization and logic formulations built with WaSHI.
- [Production Planning (LP / MIP)](examples/production.md): Production planning is a classic Linear Programming problem: determine the optimal quantity of each product to manufacture in order to maximize total profit while respecting resource constraints (raw materials, machine time, labor hours).
- [0-1 Knapsack Problem (Binary MIP)](examples/knapsack.md): The 0-1 Knapsack problem is an essential combinatorial optimization problem: given a set of items, each with a weight and a value, determine which items to include in a collection so that the total weight does not exceed a given limit and the total value is maximized.
- [Transportation & Allocation Network (LP)](examples/transportation.md): The transportation problem is one of the most fundamental network optimization models: determine how many units to ship from each supply origin (factory) to each destination (store) to minimize total shipping cost while respecting factory supply limits and meeting store demands.
- [Diet Problem & Sensitivity Analysis (LP Duals & Slacks)](examples/diet-sensitivity.md): When solving a Linear Programming model, the optimal variable values (`var.value`) are only half the story.
- [Staff Shift Scheduling & Conflict Diagnosis (MIP + Z3)](examples/shift-scheduling.md): Staff shift scheduling is a classic real-world application of Mixed-Integer Programming in SaaS and workforce management tools.
- [E-Commerce Cart & Coupon Optimizer (Indicator MIP)](examples/ecommerce-coupons.md): Modern e-commerce checkouts often feature complex promotional rules: minimum spend thresholds, category-specific discounts, stackable vs. mutually exclusive coupons, and maximum coupon limits per order.
- [Portfolio Optimization (QP)](examples/portfolio-qp.md): The Markowitz mean-variance portfolio optimization problem is the foundation of modern quantitative finance: allocate capital across risky assets to minimize overall portfolio variance (risk) subject to achieving a minimum required expected return.
- [SMT Security Policies](examples/smt-security.md): Satisfiability Modulo Theories (SMT) combines propositional logic (Boolean SAT) with first-order theories (linear integer arithmetic, real inequalities).
- [Conflict Diagnosis (Unsat Core)](examples/unsat-core.md): When business rules, budgets, and operational policies grow complex, constraints inevitably conflict.
- [Capacitated Vehicle Routing Problem (CVRP, 50 Customers via Column Generation)](examples/vehicle-routing.md): The **Capacitated Vehicle Routing Problem (CVRP)** determines the minimum number of delivery vehicles needed to visit a set of customers, subject to vehicle cargo capacity, maximum customer stops per shift, and route duration limits.
- [Traveling Salesperson Problem (TSP via Benders Decomposition)](examples/traveling-salesperson.md): The **Traveling Salesperson Problem (TSP)** seeks the shortest closed tour that visits every city in a given set once and returns to the starting city.