From c4f85493a745cf8ebdb176ed9578ff62acc709fd Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 26 Feb 2026 03:33:58 +0000 Subject: [PATCH 1/2] Initial plan From 234913bf56717865510b52117871664bcc5d02db Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 26 Feb 2026 04:04:27 +0000 Subject: [PATCH 2/2] Implement register_on_clause for OCaml and TypeScript bindings Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/api/js/package-lock.json | 8 +-- src/api/js/scripts/build-wasm.ts | 4 +- src/api/js/src/browser.ts | 2 +- src/api/js/src/high-level/high-level.ts | 54 +++++++++++++++++++- src/api/js/src/high-level/types.ts | 18 +++++++ src/api/js/src/jest.ts | 2 +- src/api/js/src/node.ts | 2 +- src/api/ml/z3.ml | 5 ++ src/api/ml/z3.mli | 7 +++ src/api/ml/z3native.ml.pre | 3 ++ src/api/ml/z3native_stubs.c.pre | 68 +++++++++++++++++++++++++ 11 files changed, 159 insertions(+), 14 deletions(-) diff --git a/src/api/js/package-lock.json b/src/api/js/package-lock.json index acfa8eb8b..a93b8c8a8 100644 --- a/src/api/js/package-lock.json +++ b/src/api/js/package-lock.json @@ -74,7 +74,6 @@ "resolved": "https://registry.npmjs.org/@babel/core/-/core-7.19.3.tgz", "integrity": "sha512-WneDJxdsjEvyKtXKsaBGbDeiyOjR5vYq4HcShxnIbG0qixpoHjI3MqeZM9NDvsojNCEBItQE4juOo/bU6e72gQ==", "dev": true, - "peer": true, "dependencies": { "@ampproject/remapping": "^2.1.0", "@babel/code-frame": "^7.18.6", @@ -1553,8 +1552,7 @@ "version": "17.0.45", "resolved": "https://registry.npmjs.org/@types/node/-/node-17.0.45.tgz", "integrity": "sha512-w+tIMs3rq2afQdsPJlODhoUEKzFP1ayaoyl1CcnwtIlsVe7K7bA1NGm4s3PraqTLlXnbIN84zuBlxBWo1u9BLw==", - "dev": true, - "peer": true + "dev": true }, "node_modules/@types/prettier": { "version": "2.7.1", @@ -1928,7 +1926,6 @@ "url": "https://tidelift.com/funding/github/npm/browserslist" } ], - "peer": true, "dependencies": { "caniuse-lite": "^1.0.30001400", "electron-to-chromium": "^1.4.251", @@ -3315,7 +3312,6 @@ "resolved": "https://registry.npmjs.org/jest/-/jest-28.1.3.tgz", "integrity": "sha512-N4GT5on8UkZgH0O5LUavMRV1EDEhNTL0KEfRmDIeZHSV7p2XgLoY9t9VDUgL6o+yfdgYHVxuz81G8oB9VG5uyA==", "dev": true, - "peer": true, "dependencies": { "@jest/core": "^28.1.3", "@jest/types": "^28.1.3", @@ -6544,7 +6540,6 @@ "resolved": "https://registry.npmjs.org/ts-node/-/ts-node-10.9.1.tgz", "integrity": "sha512-NtVysVPkxxrwFGUUxGYhfux8k78pQB3JqYBXlLRZgdGUqTO5wU/UyHop5p70iEbGhB7q5KmiZiU0Y3KlJrScEw==", "dev": true, - "peer": true, "dependencies": { "@cspotcode/source-map-support": "^0.8.0", "@tsconfig/node10": "^1.0.7", @@ -6664,7 +6659,6 @@ "integrity": "sha512-i5t66RHxDvVN40HfDd1PsEThGNnlMCMT3jMUuoh9/0TaqWevNontacunWyN02LA9/fIbEWlcHZcgTKb9QoaLfg==", "dev": true, "license": "Apache-2.0", - "peer": true, "bin": { "tsc": "bin/tsc", "tsserver": "bin/tsserver" diff --git a/src/api/js/scripts/build-wasm.ts b/src/api/js/scripts/build-wasm.ts index 970ed06f0..0e01abfbf 100644 --- a/src/api/js/scripts/build-wasm.ts +++ b/src/api/js/scripts/build-wasm.ts @@ -72,10 +72,10 @@ fs.mkdirSync(path.dirname(ccWrapperPath), { recursive: true }); fs.writeFileSync(ccWrapperPath, makeCCWrapper()); const fns = JSON.stringify(exportedFuncs()); -const methods = '["PThread","ccall","FS","UTF8ToString","intArrayFromString"]'; +const methods = '["PThread","ccall","FS","UTF8ToString","intArrayFromString","addFunction","removeFunction"]'; const libz3a = path.normalize('../../../build/libz3.a'); spawnSync( - `emcc build/async-fns.cc ${libz3a} --std=c++20 --pre-js src/low-level/async-wrapper.js -g2 -pthread -fexceptions -s WASM_BIGINT -s USE_PTHREADS=1 -s PTHREAD_POOL_SIZE=0 -s PTHREAD_POOL_SIZE_STRICT=0 -s MODULARIZE=1 -s 'EXPORT_NAME="initZ3"' -s EXPORTED_RUNTIME_METHODS=${methods} -s EXPORTED_FUNCTIONS=${fns} -s DISABLE_EXCEPTION_CATCHING=0 -s SAFE_HEAP=0 -s TOTAL_MEMORY=2GB -s TOTAL_STACK=20MB -I z3/src/api/ -o build/z3-built.js`, + `emcc build/async-fns.cc ${libz3a} --std=c++20 --pre-js src/low-level/async-wrapper.js -g2 -pthread -fexceptions -s WASM_BIGINT -s USE_PTHREADS=1 -s PTHREAD_POOL_SIZE=0 -s PTHREAD_POOL_SIZE_STRICT=0 -s MODULARIZE=1 -s 'EXPORT_NAME="initZ3"' -s EXPORTED_RUNTIME_METHODS=${methods} -s EXPORTED_FUNCTIONS=${fns} -s DISABLE_EXCEPTION_CATCHING=0 -s SAFE_HEAP=0 -s TOTAL_MEMORY=2GB -s TOTAL_STACK=20MB -s ALLOW_TABLE_GROWTH=1 -I z3/src/api/ -o build/z3-built.js`, ); fs.rmSync(ccWrapperPath); diff --git a/src/api/js/src/browser.ts b/src/api/js/src/browser.ts index 2a3b8ff5b..1a6e41f39 100644 --- a/src/api/js/src/browser.ts +++ b/src/api/js/src/browser.ts @@ -11,6 +11,6 @@ export async function init(): Promise { } const lowLevel = await initWrapper(initZ3); - const highLevel = createApi(lowLevel.Z3); + const highLevel = createApi(lowLevel.Z3, lowLevel.em); return { ...lowLevel, ...highLevel }; } diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 367696a12..fc22f2ac6 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -152,7 +152,7 @@ function isCoercibleRational(obj: any): obj is CoercibleRational { return r; } -export function createApi(Z3: Z3Core): Z3HighLevel { +export function createApi(Z3: Z3Core, em?: any): Z3HighLevel { // TODO(ritave): Create a custom linting rule that checks if the provided callbacks to cleanup // Don't capture `this` const cleanup = new FinalizationRegistry<() => void>(callback => callback()); @@ -1998,6 +1998,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel { readonly ctx: Context; private _ptr: Z3_solver | null; + // Tracks a registered on_clause WASM callback index so it can be cleaned up + private _onClauseCallbackIdx!: { value: number | null }; get ptr(): Z3_solver { _assertPtr(this._ptr); return this._ptr; @@ -2013,7 +2015,20 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } this._ptr = myPtr; Z3.solver_inc_ref(contextPtr, myPtr); - cleanup.register(this, () => Z3.solver_dec_ref(contextPtr, myPtr), this); + // Shared mutable holder so registerOnClause and the cleanup closure see the same slot + const onClauseCallbackIdx: { value: number | null } = { value: null }; + this._onClauseCallbackIdx = onClauseCallbackIdx; + cleanup.register( + this, + () => { + Z3.solver_dec_ref(contextPtr, myPtr); + if (onClauseCallbackIdx.value !== null && em) { + em.removeFunction(onClauseCallbackIdx.value); + onClauseCallbackIdx.value = null; + } + }, + this, + ); } set(key: string, value: any): void { @@ -2260,11 +2275,46 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } release() { + // Clean up any registered on_clause callback + if (this._onClauseCallbackIdx.value !== null && em) { + em.removeFunction(this._onClauseCallbackIdx.value); + this._onClauseCallbackIdx.value = null; + } Z3.solver_dec_ref(contextPtr, this.ptr); // Mark the ptr as null to prevent double free this._ptr = null; cleanup.unregister(this); } + + registerOnClause( + callback: (proofHint: Expr | null, deps: number[], clause: AstVector>) => void, + ): void { + if (!em) { + throw new Error('registerOnClause requires the Emscripten module; pass it to createApi'); + } + // Remove any previously registered callback before registering a new one + if (this._onClauseCallbackIdx.value !== null) { + em.removeFunction(this._onClauseCallbackIdx.value); + this._onClauseCallbackIdx.value = null; + } + // Signature: void(void* ctx, Z3_ast proof_hint, unsigned n, const unsigned* deps, Z3_ast_vector literals) + const cCallback = em.addFunction( + (_ctxPtr: number, proofHintPtr: number, n: number, depsPtr: number, literalsPtr: number) => { + const proofHint = proofHintPtr ? _toExpr(proofHintPtr as unknown as Z3_ast) : null; + const deps: number[] = []; + for (let i = 0; i < n; i++) { + deps.push(em.HEAPU32[(depsPtr >> 2) + i]); + } + const clause = new AstVectorImpl(literalsPtr as unknown as Z3_ast_vector) as AstVector>; + callback(proofHint, deps, clause); + }, + 'viiiii', + ); + this._onClauseCallbackIdx.value = cCallback; + // solver_register_on_clause is not auto-wrapped (has void* and fnptr params), + // so we call the raw Emscripten export directly. + em._Z3_solver_register_on_clause(contextPtr as unknown as number, this.ptr as unknown as number, 0, cCallback); + } } class OptimizeImpl implements Optimize { diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index e070c4b58..8089480b6 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -1422,6 +1422,24 @@ export interface Solver { * but calling this eagerly can help release memory sooner. */ release(): void; + + /** + * Register a callback that is invoked when clauses are inferred during solving. + * The callback is called when a clause is: + * - asserted to the CDCL engine (input clause after pre-processing) + * - inferred by CDCL(T) using a SAT or theory conflict/propagation + * - deleted by the CDCL(T) engine + * + * Requires the Emscripten module to be passed to `createApi`. + * + * @param callback - Function called with: + * - proofHint: optional proof hint expression (may be null) + * - deps: array of clause dependency indices + * - clause: the clause as a vector of literals + */ + registerOnClause( + callback: (proofHint: Expr | null, deps: number[], clause: AstVector>) => void, + ): void; } export interface Optimize { diff --git a/src/api/js/src/jest.ts b/src/api/js/src/jest.ts index 9cbab31f1..7e8ed3f9e 100644 --- a/src/api/js/src/jest.ts +++ b/src/api/js/src/jest.ts @@ -11,7 +11,7 @@ export * from './low-level/types.__GENERATED__'; export async function init(): Promise { const lowLevel = await initWrapper(initModule); - const highLevel = createApi(lowLevel.Z3); + const highLevel = createApi(lowLevel.Z3, lowLevel.em); return { ...lowLevel, ...highLevel }; } diff --git a/src/api/js/src/node.ts b/src/api/js/src/node.ts index 9e503edcd..87be038e5 100644 --- a/src/api/js/src/node.ts +++ b/src/api/js/src/node.ts @@ -33,6 +33,6 @@ export * from './low-level/types.__GENERATED__'; * @category Global */ export async function init(): Promise { const lowLevel = await initWrapper(initModule); - const highLevel = createApi(lowLevel.Z3); + const highLevel = createApi(lowLevel.Z3, lowLevel.em); return { ...lowLevel, ...highLevel }; } diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 96e4ab1b6..aefd2bc4c 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -2019,6 +2019,11 @@ struct List.iter (fun e -> Z3native.ast_vector_push (gc x) term_vec e) terms; List.iter (fun e -> Z3native.ast_vector_push (gc x) guard_vec e) guards; Z3native.solver_solve_for (gc x) x var_vec term_vec guard_vec + + let register_on_clause (s:solver) (callback: Expr.expr option -> int list -> Expr.expr list -> unit) = + Z3native.solver_register_on_clause (gc s) s (fun proof_hint deps lits -> + let lits_list = AST.ASTVector.to_expr_list lits in + callback proof_hint deps lits_list) end diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index f9c0de47c..90687011d 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -3496,6 +3496,13 @@ sig variables are the variables to solve for, terms are the substitution terms, and guards are Boolean guards for the substitutions. *) val solve_for : solver -> Expr.expr list -> Expr.expr list -> Expr.expr list -> unit + + (** Register a callback that is invoked when clauses are inferred during solving. + The callback is called when a clause is asserted to the CDCL engine, inferred + by CDCL(T), or deleted by the CDCL(T) engine. + The callback receives an optional proof hint expression, a list of dependency + indices, and the inferred clause as a list of literal expressions. *) + val register_on_clause : solver -> (Expr.expr option -> int list -> Expr.expr list -> unit) -> unit end (** Fixedpoint solving *) diff --git a/src/api/ml/z3native.ml.pre b/src/api/ml/z3native.ml.pre index fe4e8a194..291bc3f59 100644 --- a/src/api/ml/z3native.ml.pre +++ b/src/api/ml/z3native.ml.pre @@ -37,3 +37,6 @@ type rcf_num = ptr external set_internal_error_handler : ptr -> unit = "n_set_internal_error_handler" + +external solver_register_on_clause : context -> solver -> (ast option -> int list -> ast_vector -> unit) -> unit + = "n_solver_register_on_clause" diff --git a/src/api/ml/z3native_stubs.c.pre b/src/api/ml/z3native_stubs.c.pre index c8afe90b9..2d4ce0709 100644 --- a/src/api/ml/z3native_stubs.c.pre +++ b/src/api/ml/z3native_stubs.c.pre @@ -476,3 +476,71 @@ CAMLprim DLL_PUBLIC value n_mk_config() { /* cleanup and return */ CAMLreturn(result); } + +/* on_clause callback infrastructure */ + +typedef struct { + value callback; /* OCaml callback closure, registered as global root */ + Z3_context_plus cp; /* solver's context, for wrapping AST values */ +} ml_on_clause_ctx; + +static void caml_ml_on_clause_eh(void* ctx, Z3_ast proof_hint, unsigned n, unsigned const* deps, Z3_ast_vector literals) { + CAMLparam0(); + CAMLlocal5(cb, ph_opt, deps_cons, lv, cell); + CAMLlocal1(ast_v); + unsigned i; + ml_on_clause_ctx* oc; + Z3_context_plus cp; + + oc = (ml_on_clause_ctx*)ctx; + cb = oc->callback; + cp = oc->cp; + + /* Build proof_hint as OCaml ast option */ + if (proof_hint == NULL) { + ph_opt = Val_int(0); /* None */ + } else { + ast_v = caml_alloc_custom_mem(&Z3_ast_plus_custom_ops, sizeof(Z3_ast_plus), 8); + *(Z3_ast_plus*)Data_custom_val(ast_v) = Z3_ast_plus_mk(cp, proof_hint); + ph_opt = caml_alloc_small(1, 0); /* Some */ + Field(ph_opt, 0) = ast_v; + } + + /* Build deps as OCaml int list, constructed right-to-left */ + deps_cons = Val_int(0); /* [] */ + for (i = n; i-- > 0; ) { + cell = caml_alloc_small(2, 0); + Field(cell, 0) = Val_int((int)deps[i]); + Field(cell, 1) = deps_cons; + deps_cons = cell; + } + + /* Create literals as ast_vector OCaml value */ + lv = caml_alloc_custom_mem(&Z3_ast_vector_plus_custom_ops, sizeof(Z3_ast_vector_plus), 32); + *(Z3_ast_vector_plus*)Data_custom_val(lv) = Z3_ast_vector_plus_mk(cp, literals); + + caml_callback3(cb, ph_opt, deps_cons, lv); + + CAMLreturn0; +} + +CAMLprim DLL_PUBLIC value n_solver_register_on_clause(value ctx_v, value solver_v, value cb_v) { + CAMLparam3(ctx_v, solver_v, cb_v); + Z3_context_plus cp; + Z3_solver_plus* sp; + ml_on_clause_ctx* oc; + + cp = *(Z3_context_plus*)Data_custom_val(ctx_v); + sp = (Z3_solver_plus*)Data_custom_val(solver_v); + + oc = (ml_on_clause_ctx*)malloc(sizeof(ml_on_clause_ctx)); + if (!oc) caml_raise_out_of_memory(); + + oc->callback = cb_v; + oc->cp = cp; + caml_register_global_root(&oc->callback); + + Z3_solver_register_on_clause(cp->ctx, sp->p, (void*)oc, caml_ml_on_clause_eh); + + CAMLreturn(Val_unit); +}