z3-josh

Browser-friendly packaging of the Z3 SMT solver, compiled to a single-threaded WebAssembly ES module.

The entire integration story:

import { init } from "z3-josh";

const { Context } = await init();
const { Solver, Int } = Context("main");

const x = Int.const("x");
const y = Int.const("y");
const solver = new Solver();
solver.add(x.add(y).eq(10));
solver.add(x.sub(y).eq(4));

console.log(await solver.check()); // "sat" — main thread never blocked
const model = solver.model();
console.log((await model.eval(x)).toString()); // "7"
console.log((await model.eval(y)).toString()); // "3"

Why not z3-solver?

The official npm package is built with emscripten pthreads, which requires SharedArrayBuffer, which requires cross-origin isolation (COOP/COEP headers on the document and every worker script). It also ships a self-locating classic-script loader and a CommonJS entry that expects a global initZ3. In practice that means custom dev-server middleware, raw-file serving outside the bundler, and hosts that let you set response headers.

z3-josh instead:

• No SharedArrayBuffer, no COOP/COEP, no headers. Works on GitHub Pages, vite dev, and any dumb static file server. window.crossOriginIsolated can stay false.
• Pure ESM. The wasm is resolved with new URL(..., import.meta.url), which modern bundlers understand natively. No script tags, no global shims, no config.
• check() never blocks the main thread and is cancellable — see below.
• ~16 MB wasm (down from ~33 MB), because dropping pthreads and switching to native wasm exception handling roughly halves the binary.

How it works

Two instantiations of the same wasm module (fetched and compiled once):

• A main-thread instance does everything synchronous and fast: building expressions, asserting into solvers, printing. This keeps the ergonomic synchronous API (x.add(y).eq(10)).
• A plain dedicated worker (no shared memory) holds the second instance and does all solving. solver.check() serializes the solver's full state to SMT-LIB2 (Z3_solver_to_string), sends the text over postMessage, and the worker solves it. The worker keeps the resulting model so model.eval can query it.
• Cancellation is worker.terminate() + respawn from the cached compiled WebAssembly.Module (cheap; no re-download, no re-compile). The worker holds no authoritative state, so nothing is lost: call context.interrupt(), and the in-flight check() resolves "unknown".

In Node (import { init } from "z3-josh" resolves the node condition), solving runs in-process and synchronously under the hood; the API surface is identical, but interrupt() cannot preempt a running check there.

Differences from z3-solver

The high-level API (Context, Solver, Int, Bool, BitVec, arrays, quantifiers, …) is carried over from z3-solver and works unchanged, with these exceptions:

• solver.model() returns a SolveModel, whose lookups are async (worker round trips):
  • await model.eval(expr) / await model.get(expr) — returns an expression of the main-thread context, so results compose with the API.
  • await model.evalText(expr) — the raw SMT-LIB value text.
  • await model.text() — the full (get-model) output. Iterating declarations / function interpretations is not supported in v1.
• solver.check(...assumptions) treats assumptions as plain assertions for the duration of the check: same sat/unsat answer, but unsatCore() throws (cores don't round-trip through the serialize-and-solve model).
• Model handles go stale: once a newer check() runs (any solver) or interrupt() is called, older models reject with a clear error. Query the model before starting the next check.
• Solver params set via solver.set(...) and logics passed to new Solver(logic) do not travel to the worker in v1.
• Optimize, Fixedpoint, tactics and simplify run synchronously on the main thread (they work, but block — and can't be cancelled). Prefer Solver in UI code.
• Incremental solving across checks re-sends the whole problem each time (push/pop work; state is flattened at check() time).

Using from a CDN / Observable notebooks

No bundler needed — import the dist entry directly by URL (don't use jsDelivr's /+esm transform; it rewrites import.meta.url and breaks the wasm/worker asset paths):

const { init } = await import("https://cdn.jsdelivr.net/npm/[email protected]/dist/index.js");
const z3 = await init();
const { Solver, Int } = z3.Context("main");

Cross-origin worker construction is handled internally (a same-origin blob module bootstraps the CDN-hosted worker script). In an Observable notebook, also tie the solver's lifetime to the cell so re-runs don't leak workers:

invalidation.then(() => z3.terminate());

Package contents

dist/index.js       browser entry (default condition)
dist/z3-worker.js   solve worker, spawned via new Worker(new URL(...))
dist/index-node.js  Node entry ("node" condition)
dist/z3-built.wasm  Z3, single-threaded, wasm-EH, ~16 MB
dist/**/*.d.ts      full TypeScript declarations

Building from source

Requires emscripten (emcc), python3, and Node ≥ 18.

git clone --depth 1 --branch z3-4.16.0 https://github.com/Z3Prover/z3.git z3-src
npm install
npm run build:wasm      # configure + compile libz3.a, link the ES module (~15 min)
npm run build:wrapper   # regenerate the low-level TS wrapper from the C headers
npm run build           # bundle dist/
npm test

Build notes (the parts that differ from upstream's recipe):

• mk_make.py --staticlib --single-threaded plus -DPOLLING_TIMER in CXXFLAGS. Without the latter, Z3 still spawns real threads for internal timeouts (e.g. theory_lra's hardcoded 1s conflict timers) and any unsat arithmetic query aborts in a no-pthread build. With it, deadlines are polled inside the solver loop — the same configuration Z3's own single-threaded Python wheels use.
• -fwasm-exceptions (native wasm EH) instead of emscripten's JS-based exceptions: smaller and faster; supported by all evergreen browsers and Node ≥ 18.
• -sALLOW_MEMORY_GROWTH instead of a fixed 2 GB heap; the generated wrapper reads heap views through Module.HEAP* on every access so views survive growth.