From b964e1a0e85f52e2fe4c46b190343686df18d8fd Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 13 Jul 2026 03:49:21 +0000 Subject: [PATCH 1/4] Initial plan From 66b0f58e2391f7ba235f68a97f06a5a2aa909ba5 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 13 Jul 2026 04:05:49 +0000 Subject: [PATCH 2/4] Add single-threaded WASM build for z3-solver without SharedArrayBuffer - Add makeCCSinglethreadWrapper() in make-cc-wrapper.ts that generates synchronous async wrappers using EM_ASM instead of threads + MAIN_THREAD_ASYNC_EM_ASM. Refactor shared error-handler code into a SHARED_ERROR_HANDLERS constant used by both variants. - Add build-wasm-singlethread.ts: new build script that compiles a separate libz3.a (in build-singlethread/) and z3-built-singlethread.js without -pthread / USE_PTHREADS=1. Uses -DSINGLE_THREAD -DPOLLING_TIMER and ALLOW_MEMORY_GROWTH instead of a fixed 2 GB SharedArrayBuffer. - Add src/node-singlethread.ts and src/browser-singlethread.ts entry points. Browser variant reads initZ3SingleThread from global scope (load z3-built-singlethread.js via importScripts in a Web Worker). - Add tests for both new entry points (node-singlethread.test.ts, browser-singlethread.test.ts). - Update package.json: add build:wasm:singlethread script; add exports map so users can do import { init } from 'z3-solver/singlethread'. - Update PUBLISHED_README.md: document the single-threaded variant, explain when to use it (no COOP/COEP headers), and provide a Web Worker usage example. - Update wasm.yml CI: add check-singlethread parallel job. - Update wasm-release.yml: build single-threaded artifact before publish. - Guard scoped_timer.cpp with #if defined(SINGLE_THREAD) && !defined(__EMSCRIPTEN_PTHREADS__) so that thread-based timer creation is skipped in single-threaded Emscripten builds (POLLING_TIMER covers the primary cancel_eh use-case). --- .github/workflows/wasm-release.yml | 7 +- .github/workflows/wasm.yml | 36 +++++- src/api/js/PUBLISHED_README.md | 38 +++++- src/api/js/package.json | 13 +++ src/api/js/scripts/build-wasm-singlethread.ts | 86 ++++++++++++++ src/api/js/scripts/make-cc-wrapper.ts | 110 +++++++++++++++--- src/api/js/src/browser-singlethread.test.ts | 41 +++++++ src/api/js/src/browser-singlethread.ts | 32 +++++ src/api/js/src/node-singlethread.test.ts | 37 ++++++ src/api/js/src/node-singlethread.ts | 34 ++++++ src/util/scoped_timer.cpp | 7 ++ 11 files changed, 419 insertions(+), 22 deletions(-) create mode 100644 src/api/js/scripts/build-wasm-singlethread.ts create mode 100644 src/api/js/src/browser-singlethread.test.ts create mode 100644 src/api/js/src/browser-singlethread.ts create mode 100644 src/api/js/src/node-singlethread.test.ts create mode 100644 src/api/js/src/node-singlethread.ts diff --git a/.github/workflows/wasm-release.yml b/.github/workflows/wasm-release.yml index a34346a4f6..7ee8c96ed2 100644 --- a/.github/workflows/wasm-release.yml +++ b/.github/workflows/wasm-release.yml @@ -48,7 +48,7 @@ jobs: - name: Build TypeScript run: npm run build:ts - - name: Build wasm + - name: Build wasm (threaded) run: | emsdk install ${EM_VERSION} emsdk activate ${EM_VERSION} @@ -57,6 +57,11 @@ jobs: which clang++ npm run build:wasm + - name: Build wasm (single-threaded) + run: | + source $(dirname $(which emsdk))/emsdk_env.sh + npm run build:wasm:singlethread + - name: Test run: npm test diff --git a/.github/workflows/wasm.yml b/.github/workflows/wasm.yml index 740b3b7b1a..08ec4f3763 100644 --- a/.github/workflows/wasm.yml +++ b/.github/workflows/wasm.yml @@ -17,7 +17,7 @@ permissions: jobs: check: - name: Check + name: Check (threaded) runs-on: ubuntu-latest steps: - name: Checkout @@ -52,3 +52,37 @@ jobs: - name: Test run: npm test + + check-singlethread: + name: Check (single-threaded) + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@v7.0.0 + + - name: Setup node + uses: actions/setup-node@v6 + with: + node-version: "lts/*" + + - name: Setup emscripten + uses: mymindstorm/setup-emsdk@v16 + with: + no-install: true + version: ${{env.EM_VERSION}} + actions-cache-folder: "emsdk-cache" + + - name: Install dependencies + run: npm ci + + - name: Build TypeScript + run: npm run build:ts + + - name: Build single-threaded wasm + run: | + emsdk install ${EM_VERSION} + emsdk activate ${EM_VERSION} + source $(dirname $(which emsdk))/emsdk_env.sh + which node + which clang++ + npm run build:wasm:singlethread diff --git a/src/api/js/PUBLISHED_README.md b/src/api/js/PUBLISHED_README.md index 85987ba7a2..59db2ef584 100644 --- a/src/api/js/PUBLISHED_README.md +++ b/src/api/js/PUBLISHED_README.md @@ -29,10 +29,46 @@ const api = await init({ ### Limitations -The package requires threads, which means you'll need to be running in an environment which supports `SharedArrayBuffer`. In browsers, in addition to ensuring the browser has implemented `SharedArrayBuffer`, you'll need to serve your page with [special headers](https://web.dev/coop-coep/). There's a [neat trick](https://github.com/gzuidhof/coi-serviceworker) for doing that client-side on e.g. Github Pages, though you shouldn't use that trick in more complex applications. +The default package requires threads, which means you'll need to be running in an environment which supports `SharedArrayBuffer`. In browsers, in addition to ensuring the browser has implemented `SharedArrayBuffer`, you'll need to serve your page with [special headers](https://web.dev/coop-coep/). There's a [neat trick](https://github.com/gzuidhof/coi-serviceworker) for doing that client-side on e.g. Github Pages, though you shouldn't use that trick in more complex applications. The Emscripten worker model will spawn multiple instances of `z3-built.js` for long-running operations. When building for the web, you should include that file as its own script on the page - using a bundler like webpack will prevent it from loading correctly. +#### Single-threaded build (no SharedArrayBuffer required) + +If you cannot set the COOP/COEP headers required by the default threaded build (for example because your application embeds cross-origin iframes such as YouTube), you can use the single-threaded variant instead: + +```javascript +// Node.js / bundler (no SharedArrayBuffer needed) +const { init } = require('z3-solver/singlethread'); +``` + +```typescript +// TypeScript +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) + +// 1. Load the single-threaded WASM artifact. +importScripts('z3-built-singlethread.js'); // exposes initZ3SingleThread + +// 2. Initialise Z3 (browser entry point reads initZ3SingleThread from global scope). +const { init } = await import('z3-solver/singlethread'); +const { Context } = await init(); +const { Solver, Int } = new Context('main'); + +// 3. Use Z3 normally – calls block this worker thread, not the main thread. +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 You can find the documentation for the high-level Z3 API [here](https://z3prover.github.io/api/html/js/index.html). There are some usage examples in `src/high-level/high-level.test.ts` diff --git a/src/api/js/package.json b/src/api/js/package.json index 8e0b4c912e..0768cd8908 100644 --- a/src/api/js/package.json +++ b/src/api/js/package.json @@ -18,6 +18,18 @@ "browser": "build/browser.js", "main": "build/node.js", "types": "build/node.d.ts", + "exports": { + ".": { + "types": "./build/node.d.ts", + "browser": "./build/browser.js", + "default": "./build/node.js" + }, + "./singlethread": { + "types": "./build/node-singlethread.d.ts", + "browser": "./build/browser-singlethread.js", + "default": "./build/node-singlethread.js" + } + }, "files": [ "build/**/*.{js,d.ts,wasm}" ], @@ -26,6 +38,7 @@ "build:ts:tsc": "tsc --pretty --project tsconfig.build.json ", "build:ts:generate": "ts-node --transpileOnly scripts/make-ts-wrapper.ts src/low-level/wrapper.__GENERATED__.ts src/low-level/types.__GENERATED__.ts", "build:wasm": "ts-node --transpileOnly ./scripts/build-wasm.ts", + "build:wasm:singlethread": "ts-node --transpileOnly ./scripts/build-wasm-singlethread.ts", "clean": "rimraf build 'src/**/*.__GENERATED__.*'", "lint": "prettier -c '{./,src/,scripts/,examples/}**/*.{js,ts}'", "format": "prettier --write '{./,src/,scripts/}**/*.{js,ts}'", diff --git a/src/api/js/scripts/build-wasm-singlethread.ts b/src/api/js/scripts/build-wasm-singlethread.ts new file mode 100644 index 0000000000..e38390a016 --- /dev/null +++ b/src/api/js/scripts/build-wasm-singlethread.ts @@ -0,0 +1,86 @@ +import assert from 'assert'; +import { SpawnOptions, spawnSync as originalSpawnSync } from 'child_process'; +import fs, { existsSync } from 'fs'; +import os from 'os'; +import path from 'path'; +import process from 'process'; +import { asyncFuncs } from './async-fns'; +import { makeCCSinglethreadWrapper } from './make-cc-wrapper'; +import { functions } from './parse-api'; + +console.log('--- Building single-threaded WASM (no SharedArrayBuffer required)'); + +// Single-threaded build: no -pthread / USE_PTHREADS. +// POLLING_TIMER gives timeout support via wall-clock polling rather than threads. +const SWAP_OPTS: SpawnOptions = { + shell: true, + stdio: 'inherit', + env: { + ...process.env, + CXXFLAGS: '-DSINGLE_THREAD -DPOLLING_TIMER -fexceptions -s DISABLE_EXCEPTION_CATCHING=0', + LDFLAGS: '-s WASM_BIGINT', + FPMATH_ENABLED: 'False', // Until Safari supports WASM SSE, we have to disable fast FP support + }, +}; + +function spawnSync(command: string, opts: SpawnOptions = {}) { + console.log(`- ${command}`); + // TODO(ritave): Create a splitter that keeps track of quoted strings + const [cmd, ...args] = command.split(' '); + const { error, ...rest } = originalSpawnSync(cmd, args, { ...SWAP_OPTS, ...opts }); + if (error !== undefined || rest.status !== 0) { + if (error !== undefined) { + console.error(error.message); + } else { + console.error(`Process exited with status ${rest.status}`); + } + process.exit(1); + } + return rest; +} + +function exportedFuncs(): string[] { + const extras = [ + '_malloc', + '_free', + '_set_throwy_error_handler', + '_set_noop_error_handler', + ...asyncFuncs.map(f => '_async_' + f), + ]; + + return [...extras, ...(functions as any[]).map(f => '_' + f.name)]; +} + +assert(fs.existsSync('./package.json'), 'Not in the root directory of js api'); +const z3RootDir = path.join(process.cwd(), '../../../'); + +// Single-threaded libz3.a is built in a separate directory to avoid +// conflicting with the threaded build in 'build/'. +const singlethreadBuildDir = 'build-singlethread'; +const singlethreadBuildPath = path.join(z3RootDir, singlethreadBuildDir); + +if (!existsSync(path.join(singlethreadBuildPath, 'Makefile'))) { + spawnSync( + `emconfigure python scripts/mk_make.py --staticlib --single-threaded --arm64=false --build=${singlethreadBuildDir}`, + { cwd: z3RootDir }, + ); +} + +spawnSync(`emmake make -j${os.cpus().length} libz3.a`, { cwd: singlethreadBuildPath }); + +const ccWrapperPath = 'build/async-fns-singlethread.cc'; +console.log(`- Building ${ccWrapperPath}`); +fs.mkdirSync(path.dirname(ccWrapperPath), { recursive: true }); +fs.writeFileSync(ccWrapperPath, makeCCSinglethreadWrapper()); + +const fns = JSON.stringify(exportedFuncs()); +// No PThread in exported methods for the single-threaded build. +const methods = '["ccall","FS","UTF8ToString","intArrayFromString","addFunction","removeFunction"]'; +const libz3a = path.normalize(`../../../${singlethreadBuildDir}/libz3.a`); +spawnSync( + `emcc build/async-fns-singlethread.cc ${libz3a} --std=c++20 --pre-js src/low-level/async-wrapper.js -fexceptions -s WASM_BIGINT -s MODULARIZE=1 -s 'EXPORT_NAME="initZ3SingleThread"' -s EXPORTED_RUNTIME_METHODS=${methods} -s EXPORTED_FUNCTIONS=${fns} -s DISABLE_EXCEPTION_CATCHING=0 -s SAFE_HEAP=0 -s ALLOW_MEMORY_GROWTH=1 -s INITIAL_MEMORY=64MB -s TOTAL_STACK=20MB -s ALLOW_TABLE_GROWTH=1 -I z3/src/api/ -o build/z3-built-singlethread.js`, +); + +fs.rmSync(ccWrapperPath); + +console.log('--- Single-threaded WASM build finished'); diff --git a/src/api/js/scripts/make-cc-wrapper.ts b/src/api/js/scripts/make-cc-wrapper.ts index e87aacebb9..2abbc15390 100644 --- a/src/api/js/scripts/make-cc-wrapper.ts +++ b/src/api/js/scripts/make-cc-wrapper.ts @@ -4,6 +4,34 @@ import path from 'path'; import { asyncFuncs } from './async-fns'; import { functions } from './parse-api'; +// Shared error handler code used by both threaded and single-threaded wrappers +const SHARED_ERROR_HANDLERS = ` +class Z3Exception : public std::exception { +public: + const std::string m_msg; + Z3Exception(const std::string& msg) : m_msg(msg) {} + virtual const char* what() const throw () { + return m_msg.c_str(); + } +}; + +void throwy_error_handler(Z3_context ctx, Z3_error_code c) { + throw Z3Exception(Z3_get_error_msg(ctx, c)); +} + +void noop_error_handler(Z3_context ctx, Z3_error_code c) { + // pass +} + +extern "C" void set_throwy_error_handler(Z3_context ctx) { + Z3_set_error_handler(ctx, throwy_error_handler); +} + +extern "C" void set_noop_error_handler(Z3_context ctx) { + Z3_set_error_handler(ctx, noop_error_handler); +} +`.trim(); + export function makeCCWrapper() { let wrappers = []; @@ -213,30 +241,74 @@ void wrapper_str(Args&&... args) { -class Z3Exception : public std::exception { -public: - const std::string m_msg; - Z3Exception(const std::string& msg) : m_msg(msg) {} - virtual const char* what() const throw () { - return m_msg.c_str(); +${SHARED_ERROR_HANDLERS} + +${wrappers.join('\n\n')} +`; +} + +/** + * Generates a C++ wrapper file for async Z3 functions that runs each function + * synchronously in the calling thread. This version does NOT use pthreads and + * therefore does NOT require SharedArrayBuffer / COOP-COEP headers. + * + * Intended to be paired with the Emscripten build flags: + * -DSINGLE_THREAD -DPOLLING_TIMER (no -pthread / USE_PTHREADS) + */ +export function makeCCSinglethreadWrapper() { + const wrappers: string[] = []; + + for (const fnName of asyncFuncs) { + const fn = functions.find(f => f.name === fnName); + if (fn == null) { + throw new Error(`could not find definition for ${fnName}`); + } + + const isString = fn.cRet === 'Z3_string'; + const returnType = isString ? 'auto' : fn.cRet; + + const paramList = fn.params + .map(p => `${p.isConst ? 'const ' : ''}${p.cType}${p.isPtr ? '*' : ''} ${p.name}${p.isArray ? '[]' : ''}`) + .join(', '); + + const callArgs = fn.params.map(p => p.name).join(', '); + + const resolveExpr = isString + ? `EM_ASM({ + resolve_async(UTF8ToString($0)); + }, result);` + : `EM_ASM({ + resolve_async($0); + }, result);`; + + wrappers.push( + ` +extern "C" void async_${fn.name}(${paramList}) { + try { + ${returnType} result = ${fn.name}(${callArgs}); + ${resolveExpr} + } catch (std::exception& e) { + EM_ASM({ + reject_async(new Error(UTF8ToString($0))); + }, e.what()); + } catch (...) { + EM_ASM({ + reject_async(new Error('failed with unknown exception')); + }); } -}; - -void throwy_error_handler(Z3_context ctx, Z3_error_code c) { - throw Z3Exception(Z3_get_error_msg(ctx, c)); } +`.trim(), + ); + } -void noop_error_handler(Z3_context ctx, Z3_error_code c) { - // pass -} + return `// THIS FILE IS AUTOMATICALLY GENERATED BY ${path.basename(__filename)} +// DO NOT EDIT IT BY HAND -extern "C" void set_throwy_error_handler(Z3_context ctx) { - Z3_set_error_handler(ctx, throwy_error_handler); -} +#include -extern "C" void set_noop_error_handler(Z3_context ctx) { - Z3_set_error_handler(ctx, noop_error_handler); -} +#include "../../z3.h" + +${SHARED_ERROR_HANDLERS} ${wrappers.join('\n\n')} `; diff --git a/src/api/js/src/browser-singlethread.test.ts b/src/api/js/src/browser-singlethread.test.ts new file mode 100644 index 0000000000..7162687d0f --- /dev/null +++ b/src/api/js/src/browser-singlethread.test.ts @@ -0,0 +1,41 @@ +const mockInitWrapper = jest.fn(); +const mockCreateApi = jest.fn(); + +jest.mock('./low-level', () => ({ + init: mockInitWrapper, + Z3Core: undefined, + Z3LowLevel: undefined, +})); +jest.mock('./high-level', () => ({ + createApi: mockCreateApi, +})); + +import { init } from './browser-singlethread'; + +describe('browser-singlethread init', () => { + beforeEach(() => { + delete (global as any).initZ3SingleThread; + mockInitWrapper.mockReset(); + mockCreateApi.mockReset(); + }); + + it('passes module overrides to the browser-singlethread initializer', async () => { + const initZ3SingleThread = jest.fn(); + const locateFile = jest.fn((file: string) => `https://example.test/${file}`); + const lowLevel = { Z3: { low: true }, em: { module: true } }; + const highLevel = { Context: jest.fn() }; + (global as any).initZ3SingleThread = initZ3SingleThread; + mockInitWrapper.mockResolvedValue(lowLevel); + mockCreateApi.mockReturnValue(highLevel); + + const api = await init({ locateFile }); + + expect(mockInitWrapper).toHaveBeenCalledWith(initZ3SingleThread, { locateFile }); + expect(mockCreateApi).toHaveBeenCalledWith(lowLevel.Z3, lowLevel.em); + expect(api).toEqual({ ...lowLevel, ...highLevel }); + }); + + it('throws when initZ3SingleThread is unavailable', async () => { + await expect(init()).rejects.toThrow('initZ3SingleThread was not found.'); + }); +}); diff --git a/src/api/js/src/browser-singlethread.ts b/src/api/js/src/browser-singlethread.ts new file mode 100644 index 0000000000..ff7cc90e8f --- /dev/null +++ b/src/api/js/src/browser-singlethread.ts @@ -0,0 +1,32 @@ +import { createApi, Z3HighLevel } from './high-level'; +import { init as initWrapper, Z3LowLevel, Z3ModuleOverrides } from './low-level'; +export * from './high-level/types'; +export { Z3Core, Z3LowLevel } from './low-level'; +export * from './low-level/types.__GENERATED__'; + +/** + * Browser entry point for the single-threaded Z3 build. + * + * This variant does NOT require SharedArrayBuffer or the COOP/COEP HTTP headers + * that the default (threaded) build needs. All Z3 operations run synchronously + * in the calling thread, so this build should be used inside a Web Worker to + * avoid blocking the main browser thread. + * + * Before calling `init()`, make sure the `z3-built-singlethread.js` script has + * been loaded (e.g. via `importScripts('z3-built-singlethread.js')` inside the + * 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; + if (initZ3 === undefined) { + throw new Error( + 'initZ3SingleThread was not found. ' + + 'Load z3-built-singlethread.js before calling init() ' + + '(e.g. importScripts("z3-built-singlethread.js") in a Web Worker).', + ); + } + + const lowLevel = await initWrapper(initZ3, moduleOverrides); + const highLevel = createApi(lowLevel.Z3, lowLevel.em); + return { ...lowLevel, ...highLevel }; +} diff --git a/src/api/js/src/node-singlethread.test.ts b/src/api/js/src/node-singlethread.test.ts new file mode 100644 index 0000000000..33cb64526e --- /dev/null +++ b/src/api/js/src/node-singlethread.test.ts @@ -0,0 +1,37 @@ +const mockInitModule = jest.fn(); +const mockInitWrapper = jest.fn(); +const mockCreateApi = jest.fn(); + +jest.mock('./z3-built-singlethread', () => mockInitModule, { virtual: true }); +jest.mock('./low-level', () => ({ + init: mockInitWrapper, + Z3Core: undefined, + Z3LowLevel: undefined, +})); +jest.mock('./high-level', () => ({ + createApi: mockCreateApi, +})); + +import { init } from './node-singlethread'; + +describe('node-singlethread init', () => { + beforeEach(() => { + mockInitModule.mockReset(); + mockInitWrapper.mockReset(); + mockCreateApi.mockReset(); + }); + + it('passes module overrides to the low-level initializer', async () => { + const locateFile = jest.fn((file: string) => `npm:z3-solver/build/${file}`); + const lowLevel = { Z3: { low: true }, em: { module: true } }; + const highLevel = { Context: jest.fn() }; + mockInitWrapper.mockResolvedValue(lowLevel); + mockCreateApi.mockReturnValue(highLevel); + + const api = await init({ locateFile }); + + expect(mockInitWrapper).toHaveBeenCalledWith(mockInitModule, { locateFile }); + expect(mockCreateApi).toHaveBeenCalledWith(lowLevel.Z3, lowLevel.em); + expect(api).toEqual({ ...lowLevel, ...highLevel }); + }); +}); diff --git a/src/api/js/src/node-singlethread.ts b/src/api/js/src/node-singlethread.ts new file mode 100644 index 0000000000..da257e3ecf --- /dev/null +++ b/src/api/js/src/node-singlethread.ts @@ -0,0 +1,34 @@ +// @ts-ignore no-implicit-any +import initModule = require('./z3-built-singlethread'); + +import { createApi, Z3HighLevel } from './high-level'; +import { init as initWrapper, Z3LowLevel, Z3ModuleOverrides } from './low-level'; +export * from './high-level/types'; +export { Z3Core, Z3LowLevel } from './low-level'; +export * from './low-level/types.__GENERATED__'; + +/** + * The main entry point to the single-threaded Z3 API. + * + * This variant does NOT require SharedArrayBuffer or the COOP/COEP HTTP headers + * that the default (threaded) build needs. All Z3 operations run synchronously + * in the calling thread, so this build should be used inside a Web Worker to + * avoid blocking the main browser thread. + * + * ```typescript + * 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)); + * console.log(await solver.check()); // 'sat' + * ``` + * @category Global */ +export async function init(moduleOverrides: Z3ModuleOverrides = {}): Promise { + const lowLevel = await initWrapper(initModule, moduleOverrides); + const highLevel = createApi(lowLevel.Z3, lowLevel.em); + return { ...lowLevel, ...highLevel }; +} diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index 286dcda8c4..65facb1582 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -87,6 +87,13 @@ scoped_timer::scoped_timer(unsigned ms, event_handler * eh) { r->set_auto_cancel(); return; } +#endif +// In single-threaded Emscripten builds (without pthreads), std::thread is not +// usable. Timeout support is provided via POLLING_TIMER for the primary use +// case (cancel_eh) above. Any other event-handler type simply gets +// no timeout rather than a crash. +#if defined(SINGLE_THREAD) && !defined(__EMSCRIPTEN_PTHREADS__) + return; #endif workers.lock(); if (available_workers.empty()) { From 8c80fe944063a36acfd1c902d0fc6b7c363189a5 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 13 Jul 2026 04:08:24 +0000 Subject: [PATCH 3/4] Address code review: extract INIT_GLOBAL constant in browser-singlethread.ts and fix Web Worker README example - browser-singlethread.ts: extract 'initZ3SingleThread' into INIT_GLOBAL constant to avoid duplication between the global lookup and error message - PUBLISHED_README.md: replace the dynamic import() in classic-worker example with consistent importScripts() pattern; add a separate module worker example using ES module import syntax --- src/api/js/PUBLISHED_README.md | 30 +++++++++++++++++++++----- src/api/js/src/browser-singlethread.ts | 7 ++++-- 2 files changed, 30 insertions(+), 7 deletions(-) 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).', ); From 1faba5c769e09cba3013f86b7af5772f1aea6bb5 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 13 Jul 2026 16:32:34 +0000 Subject: [PATCH 4/4] Fix missing std headers in singlethread WASM wrapper The makeCCSinglethreadWrapper() function generates a C++ file that uses SHARED_ERROR_HANDLERS (which references std::exception and std::string). The singlethread wrapper only included and ../../z3.h, missing and . The threaded wrapper gets those transitively through , but the singlethread wrapper does not include . Add the two missing includes to fix the build. --- src/api/js/scripts/make-cc-wrapper.ts | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/api/js/scripts/make-cc-wrapper.ts b/src/api/js/scripts/make-cc-wrapper.ts index 2abbc15390..30ed77455f 100644 --- a/src/api/js/scripts/make-cc-wrapper.ts +++ b/src/api/js/scripts/make-cc-wrapper.ts @@ -304,6 +304,9 @@ extern "C" void async_${fn.name}(${paramList}) { return `// THIS FILE IS AUTOMATICALLY GENERATED BY ${path.basename(__filename)} // DO NOT EDIT IT BY HAND +#include +#include + #include #include "../../z3.h"