import type { CallbackRegistry } from './callback-registry.js';
import type { UnsafeZ3Api, EmscriptenModule, Z3_context, Z3_solver, ClauseStreamCallbacks, Disposer } from './types.js';
/**
 * Register a clause lifecycle event stream on a solver.
 *
 * Z3's CDCL(T) engine emits events when clauses are added, inferred,
 * or deleted during search. This function wires those events to a JS
 * callback with structured event data.
 *
 * C signature:
 *   void Z3_solver_register_on_clause(
 *     Z3_context c, Z3_solver s, void* user_context,
 *     Z3_on_clause_eh on_clause_eh)
 *
 * Callback signature:
 *   void on_clause(void* ctx, Z3_ast proof_hint, unsigned n,
 *                  unsigned const* deps, Z3_ast_vector literals)
 *
 * Returns a disposer that removes the WASM callback pointer.
 */
export declare function registerClauseStream(mod: EmscriptenModule, raw: UnsafeZ3Api, registry: CallbackRegistry, ctx: Z3_context, solver: Z3_solver, callbacks: ClauseStreamCallbacks): Disposer;
/**
 * Read the deps array from a clause event.
 *
 * The on_clause callback receives a pointer to an array of unsigned ints
 * (dependency indices). This helper reads `n` values from that pointer.
 */
export declare function readClauseDeps(mod: EmscriptenModule, depsPtr: number, n: number): number[];
//# sourceMappingURL=callbacks.d.ts.map