diff --git a/src/api/js/PUBLISHED_README.md b/src/api/js/PUBLISHED_README.md index 59db2ef584..c2135d7f12 100644 --- a/src/api/js/PUBLISHED_README.md +++ b/src/api/js/PUBLISHED_README.md @@ -50,13 +50,18 @@ import { init } from 'z3-solver/singlethread'; The API is identical to the default export. The key difference is that all Z3 operations run **synchronously in the calling thread** rather than in a background thread. To avoid blocking the UI, run your Z3 code inside a [Web Worker](https://developer.mozilla.org/en-US/docs/Web/API/Web_Workers_API/Using_web_workers): ```javascript -// my-z3-worker.js (loaded as a Web Worker) +// my-z3-worker.js (loaded as a classic Web Worker) -// 1. Load the single-threaded WASM artifact. -importScripts('z3-built-singlethread.js'); // exposes initZ3SingleThread +// 1. Load the single-threaded WASM artifact (exposes initZ3SingleThread globally). +importScripts('z3-built-singlethread.js'); -// 2. Initialise Z3 (browser entry point reads initZ3SingleThread from global scope). -const { init } = await import('z3-solver/singlethread'); +// 2. Load the single-threaded entry point as a classic script bundle. +// Most bundlers can produce a CJS/UMD build that can be loaded with importScripts. +// Alternatively, switch to a module worker (new Worker(..., { type: 'module' })) +// and use ES module import syntax instead. +importScripts('z3-solver-singlethread-bundle.js'); // exposes Z3SolverSingleThread + +const { init } = Z3SolverSingleThread; const { Context } = await init(); const { Solver, Int } = new Context('main'); @@ -67,6 +72,21 @@ solver.add(x.ge(0)); self.postMessage(await solver.check()); // 'sat' ``` +Or with a **module worker** (supported in modern browsers): + +```javascript +// my-z3-worker.mjs (loaded as new Worker('...', { type: 'module' })) +import { init } from 'z3-solver/singlethread'; + +const { Context } = await init(); +const { Solver, Int } = new Context('main'); + +const x = Int.const('x'); +const solver = new Solver(); +solver.add(x.ge(0)); +self.postMessage(await solver.check()); // 'sat' +``` + The single-threaded WASM file (`z3-built-singlethread.js` / `z3-built-singlethread.wasm`) is distributed alongside the default build in the npm package. ## High-level diff --git a/src/api/js/src/browser-singlethread.ts b/src/api/js/src/browser-singlethread.ts index ff7cc90e8f..5facb80e1c 100644 --- a/src/api/js/src/browser-singlethread.ts +++ b/src/api/js/src/browser-singlethread.ts @@ -4,6 +4,9 @@ export * from './high-level/types'; export { Z3Core, Z3LowLevel } from './low-level'; export * from './low-level/types.__GENERATED__'; +// Name of the global exposed by z3-built-singlethread.js when loaded as a script. +const INIT_GLOBAL = 'initZ3SingleThread'; + /** * Browser entry point for the single-threaded Z3 build. * @@ -17,10 +20,10 @@ export * from './low-level/types.__GENERATED__'; * worker), so that `initZ3SingleThread` is available on the global object. * @category Global */ export async function init(moduleOverrides: Z3ModuleOverrides = {}): Promise { - const initZ3 = (global as any).initZ3SingleThread; + const initZ3 = (global as any)[INIT_GLOBAL]; if (initZ3 === undefined) { throw new Error( - 'initZ3SingleThread was not found. ' + + `${INIT_GLOBAL} was not found. ` + 'Load z3-built-singlethread.js before calling init() ' + '(e.g. importScripts("z3-built-singlethread.js") in a Web Worker).', );