Merge pull request #8781 from Z3Prover/copilot/fix-ts-ocaml-issues

Add register_on_clause to OCaml and TypeScript bindings

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,
+      "dev": true
-      "peer": 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"

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

src/api/js/src/browser.ts

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

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<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> {

src/api/js/src/high-level/types.ts

@@ -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'> {

src/api/js/src/jest.ts

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

src/api/js/src/node.ts

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

src/api/ml/z3.ml

@@ -2020,6 +2020,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
 
 

src/api/ml/z3.mli

@@ -3499,6 +3499,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 *)

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"

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);
+}