prolog-z3-wasm

SWI-Prolog 10.1.4 + Z3 4.16.0 in a single 19MB WebAssembly binary. Zero dependencies. One npm install.

This is a complete SWI-Prolog runtime compiled to WASM. It is not a subset, a transpilation, or a reimplementation. It is the real SWI-Prolog C codebase cross-compiled with Emscripten. Every Prolog feature that does not require OS-level resources (threads, sockets, processes) works identically to a native swipl install.

Z3 is compiled into the same binary. Prolog and Z3 share one WASM linear memory. 75 C bridge predicates call Z3's C API directly from Prolog — zero JS in the hot path. 787 Z3 functions are also callable from JS via ccall. The TypeScript wrapper exposes both Prolog and Z3 APIs on the same instance.

EXTREMELY LOUD REMINDER: The prolog module system workds identically to swipl - there is ZERO discrepancy. None. Zilch. Do not think about/compensate for module handle semantic differences.

npm install prolog-z3-wasm

What This Is

Full SWI-Prolog — Not a Subset

The module system, operator declarations, term expansion, DCG grammars, assert/retract, findall, catch/throw, copy_term, numbervars, read_term, write_term, meta-predicates, snapshot/1, transaction/1, incremental tabling — all of it. If it works in swipl on your machine, it works here.

Concrete things that work identically:

• :- module(Name, Exports). — SWI-Prolog's module system with import/export, reexport, use_module/1, use_module/2, module-qualified calls (Module:Goal), and meta_predicate declarations.
• :- use_module(library(lists)). — loads from the WASM virtual filesystem exactly as the native binary loads from disk.
• Dynamic predicates — :- dynamic foo/2. then assert, retract, retractall, abolish. Same semantics.
• Definite clause grammars — phrase/2, phrase/3, --> rules, pushback notation.
• Exception handling — catch/3, throw/1, ISO error terms.
• Constraint logic programming — CLP(FD), CLP(B), CLP(R), CLP(Q), CHR.
• Tabling — :- table pred/arity. and :- table pred/arity as incremental.
• snapshot/1 and transaction/1 — database isolation primitives.

Libraries Included in the Binary

All verified working in WASM. Load via :- use_module(library(X)).

Constraint Solving: clpfd, clpb, clpr, clpq, chr, simplex, dif

NLP: snowball (16-language stemmer), porter_stem, double_metaphone, isub

Semantic Web: semweb/rdf_db, semweb/rdfs, semweb/rdf11, semweb/turtle, semweb/rdf_ntriples

Parsing: dcg/basics, dcg/high_order, sgml, xpath

Data Structures: lists, assoc, ordsets, rbtrees, heaps, ugraphs

Strings: pcre, csv, base64, url

Crypto: md5, sha, uuid

Tabling: tabling (memoization, cycle-safe recursion, incremental re-derivation)

Not available (require OS features absent in WASM): thread, thread_pool, process, socket, http/*, crypto (OpenSSL).

Z3 Integration

Z3 4.16.0 is statically linked into the same WASM binary. Three access paths:

1. From Prolog — 75 C bridge predicates in the z3 module call Z3's C API directly. No JS roundtrip. Handles are Prolog integers.

:- use_module(library(z3)).
z3_mk_context(Ctx), z3_mk_solver(Ctx, S),
z3_mk_int_sort(Ctx, IS),
z3_mk_string_symbol(Ctx, x, SX), z3_mk_const(Ctx, SX, IS, X),
z3_mk_int(Ctx, 42, IS, N42), z3_mk_eq(Ctx, X, N42, Eq),
z3_solver_assert(Ctx, S, Eq), z3_check(Ctx, S, Result).
% Result = sat

2. From Prolog (ergonomic) — z3_solve/2 translates Prolog constraint syntax to Z3 ASTs automatically.

z3:z3_solve([x + y =:= 10, x > 3, y > 0], Model).
% Model = [x=6, y=4]

3. From TypeScript — pz.solve() DSL or raw pz.Z3.* (787 functions via ccall).

const result = pz.solve(({ Int, IntVal, assert }) => {
  const x = Int("x"),
    y = Int("y");
  assert(x.add(y).eq(IntVal(10)));
  assert(x.gt(IntVal(0)), y.gt(IntVal(0)));
});
// result.model.get("x") → 6

Z3 predicate categories: Lifecycle (z3_mk_context, z3_del_context, z3_mk_solver), Sorts (z3_mk_bool_sort, z3_mk_int_sort, z3_mk_real_sort, z3_mk_bv_sort), Symbols & Constants (z3_mk_const, z3_mk_int, z3_mk_real, z3_mk_string), Boolean (z3_mk_not, z3_mk_and, z3_mk_or, z3_mk_implies, z3_mk_eq, z3_mk_distinct), Arithmetic (z3_mk_add, z3_mk_sub, z3_mk_mul, z3_mk_div, z3_mk_le, z3_mk_lt), Bitvector (z3_mk_bvadd, z3_mk_bvsub), Solver (z3_solver_assert, z3_check, z3_solver_push, z3_solver_pop), Model (z3_solver_get_model, z3_model_eval, z3_get_numeral_string), Optimize (z3_mk_optimize, z3_optimize_assert, z3_optimize_maximize), SMT-LIB2 (z3_eval_smtlib2_string).

Quick Start

import { initPrologZ3 } from "prolog-z3-wasm";

const pz = await initPrologZ3();

// Prolog queries
const r = pz.query("member(X, [a, b, c])").all();
console.log(r.map((b) => b.X)); // ['a', 'b', 'c']

// Foreign predicate — JS function callable from Prolog
pz.registerForeign("is_admin", 1, (user) => user === "alice");
pz.query("is_admin(alice)").first(); // succeeds
pz.query("is_admin(bob)").first(); // null (failed)

// Load rules from a string
pz.consult(`
  allowed(User, Action) :- is_admin(User), Action = anything.
  allowed(User, read) :- \\+ is_admin(User).
`);

// CLP(FD) constraint solving
pz.consult(`
  :- use_module(library(clpfd)).
  schedule(X, Y) :- [X, Y] ins 1..5, X + Y #= 7, X #< Y, label([X, Y]).
`);
pz.query("schedule(X, Y)").all();
// [{ X: 2, Y: 5 }, { X: 3, Y: 4 }]

// Z3 from TypeScript
const result = pz.solve(({ Int, IntVal, assert }) => {
  const x = Int("x");
  const y = Int("y");
  assert(x.add(y).eq(IntVal(10)));
  assert(x.gt(IntVal(0)), y.gt(IntVal(0)));
});
console.log(result.model.get("x"), result.model.get("y"));

// Z3 from Prolog (ergonomic)
pz.query("z3:z3_solve([x + y =:= 10, x > 3, y > 0], Model)").first();
// Model = [x=6, y=4]

// Z3 user propagator — Z3 calls YOUR JS during solving
const sat = pz.solve(({ Bool, assert, propagate }) => {
  const a = Bool("a");
  const b = Bool("b");
  assert(a.or(b));
  propagate({
    variables: [a, b],
    onFixed(cb, term, value) {
      console.log("Z3 fixed:", term, value);
    },
    onFinal(cb) {
      return true;
    },
  });
});

pz.dispose();

Architecture

┌──────────────────────────────────────────────────┐
│           TypeScript / Node.js                    │
│                                                   │
│  pz.query("...")        pz.solve(builder)        │
│  pz.consult(src)        pz.Z3.mk_solver(ctx)    │
│  pz.registerForeign()   pz.userPropagator.attach │
└──────────┬──────────────────────┬────────────────┘
           │ ccall PL_*           │ ccall Z3_*
           │                      │
┌──────────▼──────────────────────▼────────────────┐
│           Single WASM Binary (19MB)               │
│                                                   │
│  ┌─────────────┐    ┌──────────┐    ┌──────────┐ │
│  │ SWI-Prolog  │◄──►│ swiplz3  │◄──►│   Z3     │ │
│  │  10.1.4     │ C  │   .c     │ C  │  4.16.0  │ │
│  │             │ FFI│ 75 preds │ API│          │ │
│  └─────────────┘    └──────────┘    └──────────┘ │
│                                                   │
│  One linear memory. Direct C function calls.      │
│  1019 exported functions (225 PL + 792 Z3).       │
└───────────────────────────────────────────────────┘

Prolog API Reference

initPrologZ3(opts?): Promise<PrologZ3Full>

Loads the WASM binary and returns the combined API:

const pz = await initPrologZ3();
const pz = await initPrologZ3({ artifactDir: "./deployed" });

pz.query(goal)           // ergonomic query with .first(), .all(), .forEach()
pz.consult(source)       // load Prolog rules from a string
pz.assertClause(clause)  // assert a single clause
pz.registerForeign(...)  // register a JS function as a Prolog predicate
pz.solve(builder)        // Z3 solve DSL (Bool, Int, Real, Enum)
pz.solveSync(ctx, solver)// synchronous Z3 check-sat
pz.Z3                    // Z3 C API (787 functions via ccall)
pz.UnsafeZ3              // Z3 callback-heavy functions
pz.userPropagator        // Z3 user propagator API
pz.inspect               // Z3 model inspection (exact strings, FPA, RCF)
pz.errors                // Z3 error handling
pz.em                    // raw Emscripten module
pz.pl                    // raw PL_* C API (60+ functions)
pz.stock                 // stock swipl-wasm prolog object
pz.dispose()             // clean up

pz.query(goal)

pz.query("member(X, [1, 2, 3])").first(); // { X: 1 } or null
pz.query("member(X, [1, 2, 3])").all(); // [{ X: 1 }, { X: 2 }, { X: 3 }]
pz.query("member(X, [1, 2, 3])").forEach((r) => console.log(r.X));

pz.registerForeign(name, arity, fn): Disposer

Register a JS function as a Prolog predicate. Prolog calls it during inference.

const dispose = pz.registerForeign("check", 2, (user, action) => {
  return myDb.canDo(user as string, action as string);
});
pz.query("check(alice, read)").first(); // succeeds if myDb says so
dispose(); // releases the WASM function table slot

Arguments are automatically marshaled: atoms -> strings, integers -> numbers, floats -> numbers, lists -> arrays. Return true for success, false for failure.

pz.consult(source)

pz.consult(`
  :- use_module(library(clpfd)).
  solve(X, Y) :- X in 1..10, Y in 1..10, X + Y #= 15, label([X, Y]).
`);

pz.assertClause(clause)

pz.assertClause("parent(tom, bob)");
pz.assertClause("ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y)");

Z3 API Reference

pz.solve(builder): SolveResult

One function to build constraints, solve, and extract the model:

const result = pz.solve(({ Bool, Int, Real, IntVal, RealVal, BoolVal, assert, distinct, propagate }) => {
  const x = Int("x");
  const y = Int("y");
  assert(x.add(y).eq(IntVal(10)));
  assert(x.gt(IntVal(0)), y.gt(IntVal(0)));
  assert(distinct(x, y));
});

result.sat; // true
result.model.get("x"); // 9 (or any valid assignment)
result.model.get("y"); // 1

Chainable expression methods:

| Bool | Arith (Int/Real) | Any Expr | | ------------- | --------------------------- | ------------- | | .and(...) | .add(...) | .eq(other) | | .or(...) | .sub(...) | .neq(other) | | .not() | .mul(...) | | | .implies(b) | .div(other) | | | .iff(b) | .neg() | | | .xor(b) | .le(other) / .lt(other) | | | | .ge(other) / .gt(other) | |

pz.userPropagator.attach(ctx, solver, state, callbacks): Disposer

Register typed callbacks for the Z3 user propagator protocol. Z3 calls your JS functions during solving:

const dispose = pz.userPropagator.attach(
  ctx,
  solver,
  { count: 0 },
  {
    onFixed: (state, cb, term, value) => {
      state.count++;
    },
    onFinal: (state, cb) => true, // true = accept model
    onEq: (state, cb, lhs, rhs) => {
      /* equality detected */
    },
    onDiseq: (state, cb, lhs, rhs) => {
      /* disequality detected */
    },
    onDecide: (state, cb, term, idx, phase) => {
      /* decision point */
    },
    onCreated: (state, cb, term) => {
      /* term internalized */
    },
    onPush: (state, cb) => {
      /* scope pushed */
    },
    onPop: (state, cb, n) => {
      /* n scopes popped */
    },
  },
);
dispose(); // releases all WASM callback slots

Error handling

pz.errors.setMode(ctx, "throw"); // Z3 throws on errors
pz.errors.setMode(ctx, "noop"); // poll for errors
const err = pz.errors.check(ctx);
if (err) console.log(err.code, err.message);

Model inspection

const { str, length } = pz.inspect.getExactString(ctx, stringAst);

withContext — managed Z3 lifecycle from TypeScript

const solutions = pz.withContext(({ ctx, solver, Z3 }) => {
  const x = Z3.mk_const(ctx, Z3.mk_string_symbol(ctx, "x"), Z3.mk_int_sort(ctx));
  Z3.solver_assert(ctx, solver, Z3.mk_gt(ctx, x, Z3.mk_int(ctx, 0, Z3.mk_int_sort(ctx))));
  pz.solveSync(ctx, solver); // SAT
  return Z3.get_numeral_string(ctx, Z3.model_eval(ctx, Z3.solver_get_model(ctx, solver), x, true));
});
// Context is gone. No inc_ref, dec_ref, del_context.

z3.pl ergonomic layer

z3:z3_solve([x + y =:= 10, x > 3, y > 0], Model).
% Model = [x=6, y=4]

% Supported operators: +, -, *, /, mod, =:=, =\=, >, <, >=, =<
% Boolean: /\, \/, \+
% CLP(FD) aliases: #=, #\=, #>, #<, #>=, #=<

SMT-LIB2 string interface

z3:z3_mk_context(Ctx),
z3:z3_eval_smtlib2_string(Ctx, '(declare-const x Int)', _),
z3:z3_eval_smtlib2_string(Ctx, '(assert (> x 5))', _),
z3:z3_eval_smtlib2_string(Ctx, '(check-sat)', Response).
% Response = 'sat'

Diagnostics

import { printDiagnostics } from "prolog-z3-wasm";
printDiagnostics(pz.em);
// === prolog-z3-wasm diagnostics ===
// Binary:   JS loaded=✓ Prolog init=✓
// Exports:  PL=225 Z3=792 shims=✓ heaps=✓
// Memory:   256MB growable=✓
// Prolog:   z3 preds=76 z3.pl=✓ clpfd=✓ clpb=✓
// Z3 (JS):  context=✓ solver=✓ solve=✓
// Z3 (PL):  selftest=sat
// =================================

Z3 Prolog Bridge — Full Predicate List

All 75 predicates live in the z3 module. Call with z3: prefix or use_module(library(z3)).

Lifecycle: z3_mk_context/1, z3_del_context/1, z3_mk_solver/2, z3_mk_simple_solver/2, z3_solver_inc_ref/2, z3_solver_dec_ref/2

Sorts: z3_mk_bool_sort/2, z3_mk_int_sort/2, z3_mk_real_sort/2, z3_mk_bv_sort/3

Symbols & Constants: z3_mk_string_symbol/3, z3_mk_int_symbol/3, z3_mk_const/4, z3_mk_true/2, z3_mk_false/2, z3_mk_int/4, z3_mk_real/4, z3_mk_numeral/4, z3_mk_string/3

Boolean: z3_mk_not/3, z3_mk_and/3, z3_mk_or/3, z3_mk_implies/4, z3_mk_iff/4, z3_mk_xor/4, z3_mk_eq/4, z3_mk_distinct/3, z3_mk_ite/5

Arithmetic: z3_mk_add/3, z3_mk_sub/3, z3_mk_mul/3, z3_mk_div/4, z3_mk_mod/4, z3_mk_rem/4, z3_mk_power/4, z3_mk_unary_minus/3, z3_mk_le/4, z3_mk_lt/4, z3_mk_ge/4, z3_mk_gt/4

Bitvector: z3_mk_bvadd/4, z3_mk_bvsub/4, z3_mk_bvand/4, z3_mk_bvor/4

Solver: z3_solver_assert/3, z3_solver_assert_and_track/4, z3_check/3, z3_solver_push/2, z3_solver_pop/3, z3_solver_reset/2, z3_solver_get_num_scopes/3, z3_solver_set_initial_value/4, z3_solver_to_string/3, z3_solver_get_assertions/3, z3_solver_get_unsat_core/3

Model: z3_solver_get_model/3, z3_model_eval/4, z3_model_to_string/3, z3_model_inc_ref/2, z3_model_dec_ref/2, z3_get_numeral_string/3, z3_get_bool_value/3

Introspection: z3_ast_to_string/3, z3_get_sort/3, z3_get_sort_kind/3, z3_sort_to_string/3, z3_is_eq_ast/3, z3_ast_vector_size/3, z3_ast_vector_get/4

Optimize: z3_mk_optimize/2, z3_optimize_assert/3, z3_optimize_maximize/4, z3_optimize_minimize/4, z3_optimize_check/3, z3_optimize_get_model/3, z3_optimize_push/2, z3_optimize_pop/2

Parameters: z3_mk_params/2, z3_params_set_uint/4, z3_params_set_bool/4, z3_solver_set_params/3, z3_params_dec_ref/2

Refcount: z3_inc_ref/2, z3_dec_ref/2

SMT-LIB2: z3_eval_smtlib2_string/3

Isolated Scopes

snapshot/1 — throwaway sandbox

pz.query(
  `snapshot((
  assert(temperature(42)),
  temperature(T)
))`,
).first(); // { T: 42 }
pz.query("temperature(_)").first(); // null — snapshot discarded everything

transaction/1 — commit on success, rollback on failure

pz.query("transaction(assert(config(ready)))").first();
pz.query("config(ready)").first(); // exists

pz.query("catch(transaction((assert(config(bad)), fail)), _, true)").first();
pz.query("config(bad)").first(); // null — rolled back

Examples

Every example is copy-paste-runnable:

npx tsx examples/01-hello.ts

Z3 Examples

| # | Example | Feature | | --- | ---------------------------- | -------------------------------------------------- | | 01 | 01-hello.ts | Basic SAT/UNSAT, model extraction | | 02 | 02-observe.ts | User propagator: onFixed, onEq, onFinal timeline | | 03 | 03-repair.ts | set_initial_value, onDecide — warm-start repair | | 04 | 04-alternatives.ts | Solution enumeration with blocking clauses | | 05 | 05-diagnostics.ts | Error modes: throw, noop, checkError | | 06 | 06-exact-values.ts | getExactString — lossless string extraction | | 07 | 07-unsafe-raw.ts | Raw addFunction/ccall escape hatch | | 08 | 08-error-boundary.ts | Callback exception -> solveSync re-throw | | 09 | 09-solve-api.ts | solve() DSL: Bool, Int, chainable ops | | 10 | 10-propagator-lifecycle.ts | onPush, onPop, onCreated — scope lifecycle | | 11 | 11-clause-stream.ts | on_clause — watch CDCL emit clauses live | | 12 | 12-interrupt.ts | Z3_interrupt — cancel solve from callback | | 13 | 13-consequence.ts | solver_propagate_consequence — inject clauses | | 14 | 14-real-arithmetic.ts | solve() DSL: Real variables, rational arithmetic | | 15 | 15-graph-coloring.ts | solve() DSL: distinct(), graph coloring | | 16 | 16-worker-pool.ts | Multi-user worker pool with deterministic routing | | 17 | 17-dsl-consequence.ts | Propagator consequence via solve DSL |

Build

Two build modes: base (full recompile) and bake (layer files onto existing binary).

Base build — full recompile (~15 min)

npm run build:wasm    # or: cd build && ./build.sh

Produces vendor/swipl-z3.{wasm,js,data} — the base binary with SWI-Prolog + Z3, no application files. Used for development and testing.

The Dockerfile:

1. Builds zlib 1.3.2 + PCRE2 10.47 (SWI-Prolog deps)
2. Builds Z3 4.16.0 as libz3.a with -fwasm-exceptions -fvisibility=default
3. Builds SWI-Prolog with swiplz3.c compiled into the core
4. Merges 792 Z3 function names into SWI-Prolog's exports.json via merge_exports.sh
5. Links everything with -fwasm-exceptions -sSUPPORT_LONGJMP=wasm
6. Bakes z3.pl into the WASM data filesystem
7. Outputs swipl-z3.wasm (19MB), swipl-z3.js (302K), swipl-z3.data (3.7MB)

Bake — layer files onto the binary (~35 sec)

npm run bake -- --add ./my-prolog-app:/app

Adds files to the WASM virtual filesystem without recompiling the .wasm binary. Produces deployed/swipl-z3.{wasm,js,data} — a self-contained binary with your application code baked in. No file mirroring needed at runtime.

npm run bake -- --add ./src/logic/my-app:/app
npm run bake -- --add ./le-runtime:/library/le
npm run bake -- --add ./app:/app --add ./le:/library/le
npm run bake -- --add ./app:/app --out ./production

The .wasm binary is identical between vendor/ and deployed/. Only the .data (filesystem image) and .js (file manifest) change.

| | vendor/ (base) | deployed/ (baked) | | ------------ | --------------------------- | ----------------------- | | .wasm | 19MB | 19MB (same) | | .data | 3.7MB (stdlib only) | 16MB+ (stdlib + app) | | .js | 302KB | 544KB+ | | Use case | Dev/testing | Production | | File loading | Mirror from host at runtime | Pre-baked, no mirroring |

const pz = await initPrologZ3(); // dev
const pz = await initPrologZ3({ artifactDir: "./deployed" }); // prod

Key compiler flags:

• -fwasm-exceptions: native WASM exception handling for Z3's C++ try/catch
• -sSUPPORT_LONGJMP=wasm: WASM-native longjmp for SWI-Prolog's setjmp/longjmp
• -fvisibility=default: ensures Z3 API symbols are exported
• -s ALLOW_MEMORY_GROWTH=1 -s INITIAL_MEMORY=256MB -s MAXIMUM_MEMORY=4GB: growable memory
• -s TOTAL_STACK=32MB: generous stack for Z3 CDCL recursion + Prolog WAM

Known Limitations

• Nonlinear integer arithmetic (NIA): Z3's NIA solver may crash in WASM for constraints involving division by variables (15 / x) or polynomial expressions (x^2 = 9). Linear arithmetic (LIA/LRA), boolean logic, bitvectors, optimization, and quantifiers work correctly.
• Browser support: The WASM binary works in browsers but the initPrologZ3() loader uses Node.js APIs. A browser-compatible loader is planned.
• Deterministic foreign predicates only: registerForeign supports deterministic predicates (succeed or fail, no backtracking).

FAQ

How do I use this in a multi-user server?

Use snapshot/1 for per-request isolation. Each request asserts temporary facts, reasons over them, and the snapshot discards everything. For RDF data, use named graphs per request.

For full process isolation, use worker_threads. Each worker holds a hot WASM instance.

Can Z3 call out to TypeScript?

Yes. User propagators — Z3 calls your JS/TS functions during solving via 10 callback types (onFixed, onFinal, onEq, onDecide, etc.). Your callbacks can inject constraints back into Z3 via cb.propagate() and cb.conflict().

Does Z3 work from Prolog?

Yes. 75 C bridge predicates call Z3's C API directly within WASM linear memory. The z3:z3_solve/2 ergonomic predicate provides constraint syntax translation (Prolog terms -> Z3 ASTs) and model extraction.

Can two users share a worker?

Yes. Use snapshot/1 to isolate each request's temporary facts. The base database is shared and read-only during snapshots. Each pz.solve() call creates and destroys its own Z3 context — complete isolation.

Tests

npm test          # 255 tests, ~17s

25 test files:

• 7 Prolog suites (basic, advanced, CLP(FD), foreign predicates, marshaling, libraries, WASM modules)
• 3 Z3 JS API suites (solve DSL, integration, enum)
• 11 Prolog->Z3 bridge suites (lifecycle, sorts, boolean, arithmetic, incremental, model, optimize, unsat core, introspection, params, bitvectors)
• 1 z3.pl ergonomic layer suite
• 1 combined suite (Prolog + Z3 + CLP(FD) together)
• 2 utility suites (handle table, callback registry)

Standalone packages

This combined package supersedes the standalone prolog-wasm-full and z3-solver-full packages. If you need either runtime without the other:

• Prolog only (2.2MB, no Z3): packages/prolog-wasm-full — commit cd227abe
• Z3 only (25MB, no Prolog): packages/z3-solver-full — commit cd227abe

git checkout cd227abe -- packages/prolog-wasm-full

License

MIT