mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-01 11:16:54 +00:00
Code Activity

Implement register_on_clause for OCaml and TypeScript bindings

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-26 04:04:27 +00:00
parent c4f85493a7
commit 234913bf56
11 changed files with 159 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/api/js/package-lock.json generated
View file

@ -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"

4
src/api/js/scripts/build-wasm.ts
View file

@ -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);

2
src/api/js/src/browser.ts
View file

@ -11,6 +11,6 @@ export async function init(): Promise<Z3LowLevel & Z3HighLevel> {
}
const lowLevel = await initWrapper(initZ3);
const highLevel = createApi(lowLevel.Z3);
const highLevel = createApi(lowLevel.Z3, lowLevel.em);
return { ...lowLevel, ...highLevel };
}

54
src/api/js/src/high-level/high-level.ts
View file

@ -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<Name>;
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<Name> | null, deps: number[], clause: AstVector<Name, Bool<Name>>) => 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<Name, Bool<Name>>;
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<Name> {

18
src/api/js/src/high-level/types.ts
View file

@ -1422,6 +1422,24 @@ export interface Solver<Name extends string = 'main'> {
* 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<Name> | null, deps: number[], clause: AstVector<Name, Bool<Name>>) => void,
): void;
}
export interface Optimize<Name extends string = 'main'> {

2
src/api/js/src/jest.ts
View file

@ -11,7 +11,7 @@ export * from './low-level/types.__GENERATED__';
export async function init(): Promise<Z3HighLevel & Z3LowLevel> {
const lowLevel = await initWrapper(initModule);
const highLevel = createApi(lowLevel.Z3);
const highLevel = createApi(lowLevel.Z3, lowLevel.em);
return { ...lowLevel, ...highLevel };
}

2
src/api/js/src/node.ts
View file

@ -33,6 +33,6 @@ export * from './low-level/types.__GENERATED__';
* @category Global */
export async function init(): Promise<Z3HighLevel & Z3LowLevel> {
const lowLevel = await initWrapper(initModule);
const highLevel = createApi(lowLevel.Z3);
const highLevel = createApi(lowLevel.Z3, lowLevel.em);
return { ...lowLevel, ...highLevel };
}