Merge pull request #8735 from Z3Prover/copilot/fix-discussed-issues

Add missing API bindings: importModelConverter, OnClause, and user propagator (Go/Java)

scripts/update_api.py

@@ -647,6 +647,8 @@ def mk_java(java_src, java_dir, package_name):
   public static native boolean propagateConsequence(Object o, long ctx, long solver, long javainfo, int num_fixed, long[] fixed, long num_eqs, long[] eq_lhs, long[] eq_rhs, long conseq);
   public static native boolean propagateNextSplit(Object o, long ctx, long solver, long javainfo, long e, long idx, int phase);
   public static native void propagateDestroy(Object o, long ctx, long solver, long javainfo);
+  public static native long onClauseInit(Object o, long ctx, long solver);
+  public static native void onClauseDestroy(long javainfo);
 
   public static abstract class UserPropagatorBase implements AutoCloseable {
     protected long ctx;

src/api/go/propagator.go

@@ -0,0 +1,278 @@
+package z3
+
+/*
+#include "z3.h"
+#include <stdint.h>
+
+// Declarations for C helper functions defined in propagator_bridge.c
+extern void z3go_solver_propagate_init(Z3_context ctx, Z3_solver s, uintptr_t user_ctx);
+extern void z3go_solver_propagate_fixed(Z3_context ctx, Z3_solver s);
+extern void z3go_solver_propagate_final(Z3_context ctx, Z3_solver s);
+extern void z3go_solver_propagate_eq(Z3_context ctx, Z3_solver s);
+extern void z3go_solver_propagate_diseq(Z3_context ctx, Z3_solver s);
+extern void z3go_solver_propagate_created(Z3_context ctx, Z3_solver s);
+extern void z3go_solver_propagate_decide(Z3_context ctx, Z3_solver s);
+extern void z3go_solver_propagate_on_binding(Z3_context ctx, Z3_solver s);
+extern void z3go_solver_register_on_clause(Z3_context ctx, Z3_solver s, uintptr_t user_ctx);
+*/
+import "C"
+import (
+	"runtime/cgo"
+)
+
+// UserPropagator implements a custom theory propagator for Z3.
+// Embed this type and override callback methods to implement a propagator.
+//
+// Example usage:
+//
+//	type MyPropagator struct {
+//	    z3.UserPropagator
+//	}
+//
+//	func (p *MyPropagator) Push() { ... }
+//	func (p *MyPropagator) Pop(n uint) { ... }
+//	func (p *MyPropagator) Fresh(ctx *z3.Context) z3.UserPropagatorCallbacks { return &MyPropagator{} }
+type UserPropagator struct {
+	ctx    *Context
+	solver *Solver
+	cb     C.Z3_solver_callback // current callback context, valid only during a callback
+	handle cgo.Handle           // handle for passing to C as void* context
+	iface  UserPropagatorCallbacks
+}
+
+// UserPropagatorCallbacks is the interface that a user propagator must implement.
+// Push, Pop, and Fresh are mandatory. The other callbacks are optional.
+type UserPropagatorCallbacks interface {
+	// Push is called when the solver creates a new backtracking scope.
+	Push()
+	// Pop is called when the solver backtracks n scopes.
+	Pop(n uint)
+	// Fresh is called when the solver spawns a new internal solver instance.
+	// Return a propagator for the new context. The callbacks registered on the
+	// original propagator will also be registered on the fresh one.
+	Fresh(ctx *Context) UserPropagatorCallbacks
+}
+
+// FixedHandler is implemented by propagators that handle fixed-value assignments.
+type FixedHandler interface {
+	Fixed(term *Expr, value *Expr)
+}
+
+// FinalHandler is implemented by propagators that handle the final check.
+// The final check is invoked when all decision variables have been assigned.
+type FinalHandler interface {
+	Final()
+}
+
+// EqHandler is implemented by propagators that handle expression equalities.
+type EqHandler interface {
+	Eq(a *Expr, b *Expr)
+}
+
+// DiseqHandler is implemented by propagators that handle expression disequalities.
+type DiseqHandler interface {
+	Diseq(a *Expr, b *Expr)
+}
+
+// CreatedHandler is implemented by propagators that handle term creation events.
+// Terms are created when they use a function declared with PropagatorDeclare.
+type CreatedHandler interface {
+	Created(t *Expr)
+}
+
+// DecideHandler is implemented by propagators that handle solver decision events.
+type DecideHandler interface {
+	Decide(t *Expr, idx uint, phase bool)
+}
+
+// OnBindingHandler is implemented by propagators that handle quantifier binding events.
+// Return false to block the instantiation.
+type OnBindingHandler interface {
+	OnBinding(q *Expr, inst *Expr) bool
+}
+
+// newUserPropagator creates a new UserPropagator wrapping the given callbacks.
+func newUserPropagator(ctx *Context, solver *Solver, iface UserPropagatorCallbacks) *UserPropagator {
+	p := &UserPropagator{
+		ctx:    ctx,
+		solver: solver,
+		iface:  iface,
+	}
+	p.handle = cgo.NewHandle(p)
+	C.z3go_solver_propagate_init(ctx.ptr, solver.ptr, C.uintptr_t(p.handle))
+	return p
+}
+
+// Close releases the resources associated with this propagator.
+// It must be called when the propagator is no longer needed.
+func (p *UserPropagator) Close() {
+	if p.handle != 0 {
+		p.handle.Delete()
+		p.handle = 0
+	}
+}
+
+// RegisterFixed registers the fixed-value callback.
+// The propagator's iface must implement FixedHandler.
+func (p *UserPropagator) RegisterFixed() {
+	C.z3go_solver_propagate_fixed(p.ctx.ptr, p.solver.ptr)
+}
+
+// RegisterFinal registers the final-check callback.
+// The propagator's iface must implement FinalHandler.
+func (p *UserPropagator) RegisterFinal() {
+	C.z3go_solver_propagate_final(p.ctx.ptr, p.solver.ptr)
+}
+
+// RegisterEq registers the equality callback.
+// The propagator's iface must implement EqHandler.
+func (p *UserPropagator) RegisterEq() {
+	C.z3go_solver_propagate_eq(p.ctx.ptr, p.solver.ptr)
+}
+
+// RegisterDiseq registers the disequality callback.
+// The propagator's iface must implement DiseqHandler.
+func (p *UserPropagator) RegisterDiseq() {
+	C.z3go_solver_propagate_diseq(p.ctx.ptr, p.solver.ptr)
+}
+
+// RegisterCreated registers the term-creation callback.
+// The propagator's iface must implement CreatedHandler.
+func (p *UserPropagator) RegisterCreated() {
+	C.z3go_solver_propagate_created(p.ctx.ptr, p.solver.ptr)
+}
+
+// RegisterDecide registers the decision callback.
+// The propagator's iface must implement DecideHandler.
+func (p *UserPropagator) RegisterDecide() {
+	C.z3go_solver_propagate_decide(p.ctx.ptr, p.solver.ptr)
+}
+
+// RegisterOnBinding registers the quantifier-binding callback.
+// The propagator's iface must implement OnBindingHandler.
+func (p *UserPropagator) RegisterOnBinding() {
+	C.z3go_solver_propagate_on_binding(p.ctx.ptr, p.solver.ptr)
+}
+
+// Add registers an expression for propagation.
+// Only Bool and BitVector expressions can be registered.
+// May be called during a callback (uses the solver callback) or outside (uses the solver directly).
+func (p *UserPropagator) Add(e *Expr) {
+	if p.cb != nil {
+		C.Z3_solver_propagate_register_cb(p.ctx.ptr, p.cb, e.ptr)
+	} else {
+		C.Z3_solver_propagate_register(p.ctx.ptr, p.solver.ptr, e.ptr)
+	}
+}
+
+// Consequence propagates a consequence based on fixed terms.
+// fixed is the list of fixed terms used as premises.
+// Returns true if the propagation was accepted.
+func (p *UserPropagator) Consequence(fixed []*Expr, consequence *Expr) bool {
+	return p.ConsequenceWithEqs(fixed, nil, nil, consequence)
+}
+
+// ConsequenceWithEqs propagates a consequence based on fixed values and equalities.
+// fixed are the premise fixed terms, lhs/rhs are equality premises, consequence is the result.
+// Returns true if the propagation was accepted.
+func (p *UserPropagator) ConsequenceWithEqs(fixed []*Expr, lhs []*Expr, rhs []*Expr, consequence *Expr) bool {
+	numFixed := C.uint(len(fixed))
+	numEqs := C.uint(len(lhs))
+	var fixedPtr *C.Z3_ast
+	var lhsPtr *C.Z3_ast
+	var rhsPtr *C.Z3_ast
+	if numFixed > 0 {
+		cFixed := make([]C.Z3_ast, numFixed)
+		for i, e := range fixed {
+			cFixed[i] = e.ptr
+		}
+		fixedPtr = &cFixed[0]
+	}
+	if numEqs > 0 {
+		cLhs := make([]C.Z3_ast, numEqs)
+		cRhs := make([]C.Z3_ast, numEqs)
+		for i := range lhs {
+			cLhs[i] = lhs[i].ptr
+			cRhs[i] = rhs[i].ptr
+		}
+		lhsPtr = &cLhs[0]
+		rhsPtr = &cRhs[0]
+	}
+	result := C.Z3_solver_propagate_consequence(p.ctx.ptr, p.cb,
+		numFixed, fixedPtr,
+		numEqs, lhsPtr, rhsPtr,
+		consequence.ptr)
+	return result == C.bool(true)
+}
+
+// NextSplit overrides the solver's next variable to split on.
+// This should be called during the Decide callback to override the decision.
+// phase: -1 for false, 0 for default, 1 for true (as Z3_lbool values).
+func (p *UserPropagator) NextSplit(e *Expr, idx uint, phase int) bool {
+	result := C.Z3_solver_next_split(p.ctx.ptr, p.cb, e.ptr, C.uint(idx), C.Z3_lbool(phase))
+	return result == C.bool(true)
+}
+
+// PropagatorDeclare creates an uninterpreted function declaration for the user propagator.
+// When expressions using this function are created, the Created callback is invoked.
+func (ctx *Context) PropagatorDeclare(name string, domain []*Sort, rangeSort *Sort) *FuncDecl {
+	sym := ctx.MkStringSymbol(name)
+	n := C.uint(len(domain))
+	var domainPtr *C.Z3_sort
+	if n > 0 {
+		cDomain := make([]C.Z3_sort, n)
+		for i, s := range domain {
+			cDomain[i] = s.ptr
+		}
+		domainPtr = &cDomain[0]
+	}
+	result := C.Z3_solver_propagate_declare(ctx.ptr, sym.ptr, n, domainPtr, rangeSort.ptr)
+	return newFuncDecl(ctx, result)
+}
+
+// NewUserPropagator attaches a user propagator to the solver.
+// The callbacks object must implement UserPropagatorCallbacks (Push, Pop, Fresh).
+// Optional callbacks (Fixed, Final, Eq, Diseq, Created, Decide, OnBinding)
+// are registered by calling the corresponding Register* methods on the returned propagator.
+//
+// The propagator must be closed by calling Close() when no longer needed.
+func (s *Solver) NewUserPropagator(callbacks UserPropagatorCallbacks) *UserPropagator {
+	return newUserPropagator(s.ctx, s, callbacks)
+}
+
+// OnClauseHandler is the callback function type for clause inference events.
+// proofHint is a partial derivation justifying the inference (may be nil).
+// deps contains dependency indices.
+// literals is the inferred clause as an AST vector.
+// The lifetime of proofHint and literals is limited to the callback scope.
+type OnClauseHandler func(proofHint *Expr, deps []uint, literals *ASTVector)
+
+// OnClause registers a callback for clause inferences during solving.
+// Useful for observing learned clauses, custom learning strategies,
+// clause sharing in parallel solvers, and proof extraction.
+// Call Close when the callback is no longer needed.
+type OnClause struct {
+	handle  cgo.Handle
+	ctx     *Context
+	handler OnClauseHandler
+}
+
+// NewOnClause registers a callback for clause inferences on the given solver.
+// The returned OnClause must be closed by calling Close() when done.
+func (s *Solver) NewOnClause(handler OnClauseHandler) *OnClause {
+	oc := &OnClause{
+		ctx:     s.ctx,
+		handler: handler,
+	}
+	oc.handle = cgo.NewHandle(oc)
+	C.z3go_solver_register_on_clause(s.ctx.ptr, s.ptr, C.uintptr_t(oc.handle))
+	return oc
+}
+
+// Close releases the resources associated with this on-clause callback.
+func (oc *OnClause) Close() {
+	if oc.handle != 0 {
+		oc.handle.Delete()
+		oc.handle = 0
+	}
+}

src/api/go/propagator_bridge.c

@@ -0,0 +1,93 @@
+#include "z3.h"
+#include "_cgo_export.h"
+#include <stdint.h>
+
+/* Bridge functions that adapt C callback signatures to exported Go functions.
+ * The user context (void*) is stored/received as uintptr_t to avoid unsafe pointer
+ * conversion warnings in Go. */
+
+static void propagator_push_bridge(void* ctx, Z3_solver_callback cb) {
+    goPushCb((uintptr_t)ctx, cb);
+}
+
+static void propagator_pop_bridge(void* ctx, Z3_solver_callback cb, unsigned num_scopes) {
+    goPopCb((uintptr_t)ctx, cb, num_scopes);
+}
+
+static void* propagator_fresh_bridge(void* ctx, Z3_context new_context) {
+    return (void*)goFreshCb((uintptr_t)ctx, new_context);
+}
+
+static void propagator_fixed_bridge(void* ctx, Z3_solver_callback cb, Z3_ast t, Z3_ast value) {
+    goFixedCb((uintptr_t)ctx, cb, t, value);
+}
+
+static void propagator_eq_bridge(void* ctx, Z3_solver_callback cb, Z3_ast s, Z3_ast t) {
+    goEqCb((uintptr_t)ctx, cb, s, t);
+}
+
+static void propagator_diseq_bridge(void* ctx, Z3_solver_callback cb, Z3_ast s, Z3_ast t) {
+    goDiseqCb((uintptr_t)ctx, cb, s, t);
+}
+
+static void propagator_final_bridge(void* ctx, Z3_solver_callback cb) {
+    goFinalCb((uintptr_t)ctx, cb);
+}
+
+static void propagator_created_bridge(void* ctx, Z3_solver_callback cb, Z3_ast t) {
+    goCreatedCb((uintptr_t)ctx, cb, t);
+}
+
+static void propagator_decide_bridge(void* ctx, Z3_solver_callback cb, Z3_ast t, unsigned idx, bool phase) {
+    goDecideCb((uintptr_t)ctx, cb, t, idx, phase);
+}
+
+static bool propagator_on_binding_bridge(void* ctx, Z3_solver_callback cb, Z3_ast q, Z3_ast inst) {
+    return goOnBindingCb((uintptr_t)ctx, cb, q, inst);
+}
+
+static void on_clause_bridge(void* ctx, Z3_ast proof_hint, unsigned n, unsigned const* deps, Z3_ast_vector literals) {
+    goOnClauseCb((uintptr_t)ctx, proof_hint, n, (unsigned*)deps, literals);
+}
+
+/* C helper functions that Go calls to register callbacks.
+ * These take uintptr_t for the user context and cast it to void* internally. */
+
+void z3go_solver_propagate_init(Z3_context ctx, Z3_solver s, uintptr_t user_ctx) {
+    Z3_solver_propagate_init(ctx, s, (void*)user_ctx,
+        propagator_push_bridge,
+        propagator_pop_bridge,
+        propagator_fresh_bridge);
+}
+
+void z3go_solver_propagate_fixed(Z3_context ctx, Z3_solver s) {
+    Z3_solver_propagate_fixed(ctx, s, propagator_fixed_bridge);
+}
+
+void z3go_solver_propagate_final(Z3_context ctx, Z3_solver s) {
+    Z3_solver_propagate_final(ctx, s, propagator_final_bridge);
+}
+
+void z3go_solver_propagate_eq(Z3_context ctx, Z3_solver s) {
+    Z3_solver_propagate_eq(ctx, s, propagator_eq_bridge);
+}
+
+void z3go_solver_propagate_diseq(Z3_context ctx, Z3_solver s) {
+    Z3_solver_propagate_diseq(ctx, s, propagator_diseq_bridge);
+}
+
+void z3go_solver_propagate_created(Z3_context ctx, Z3_solver s) {
+    Z3_solver_propagate_created(ctx, s, propagator_created_bridge);
+}
+
+void z3go_solver_propagate_decide(Z3_context ctx, Z3_solver s) {
+    Z3_solver_propagate_decide(ctx, s, propagator_decide_bridge);
+}
+
+void z3go_solver_propagate_on_binding(Z3_context ctx, Z3_solver s) {
+    Z3_solver_propagate_on_binding(ctx, s, propagator_on_binding_bridge);
+}
+
+void z3go_solver_register_on_clause(Z3_context ctx, Z3_solver s, uintptr_t user_ctx) {
+    Z3_solver_register_on_clause(ctx, s, (void*)user_ctx, on_clause_bridge);
+}

src/api/go/propagator_callbacks.go

@@ -0,0 +1,163 @@
+package z3
+
+/*
+#include "z3.h"
+#include <stdint.h>
+*/
+import "C"
+import (
+	"runtime/cgo"
+	"unsafe"
+)
+
+// goPushCb is exported to C as a callback for Z3_push_eh.
+//
+//export goPushCb
+func goPushCb(ctx C.uintptr_t, cb C.Z3_solver_callback) {
+	p := cgo.Handle(ctx).Value().(*UserPropagator)
+	old := p.cb
+	p.cb = cb
+	defer func() { p.cb = old }()
+	p.iface.Push()
+}
+
+// goPopCb is exported to C as a callback for Z3_pop_eh.
+//
+//export goPopCb
+func goPopCb(ctx C.uintptr_t, cb C.Z3_solver_callback, numScopes C.uint) {
+	p := cgo.Handle(ctx).Value().(*UserPropagator)
+	old := p.cb
+	p.cb = cb
+	defer func() { p.cb = old }()
+	p.iface.Pop(uint(numScopes))
+}
+
+// goFreshCb is exported to C as a callback for Z3_fresh_eh.
+//
+//export goFreshCb
+func goFreshCb(ctx C.uintptr_t, newContext C.Z3_context) C.uintptr_t {
+	p := cgo.Handle(ctx).Value().(*UserPropagator)
+	freshCtx := &Context{ptr: newContext}
+	freshIface := p.iface.Fresh(freshCtx)
+	freshProp := &UserPropagator{
+		ctx:   freshCtx,
+		iface: freshIface,
+	}
+	freshProp.handle = cgo.NewHandle(freshProp)
+	return C.uintptr_t(freshProp.handle)
+}
+
+// goFixedCb is exported to C as a callback for Z3_fixed_eh.
+//
+//export goFixedCb
+func goFixedCb(ctx C.uintptr_t, cb C.Z3_solver_callback, t C.Z3_ast, value C.Z3_ast) {
+	p := cgo.Handle(ctx).Value().(*UserPropagator)
+	if h, ok := p.iface.(FixedHandler); ok {
+		old := p.cb
+		p.cb = cb
+		defer func() { p.cb = old }()
+		h.Fixed(newExpr(p.ctx, t), newExpr(p.ctx, value))
+	}
+}
+
+// goEqCb is exported to C as a callback for Z3_eq_eh (equality).
+//
+//export goEqCb
+func goEqCb(ctx C.uintptr_t, cb C.Z3_solver_callback, s C.Z3_ast, t C.Z3_ast) {
+	p := cgo.Handle(ctx).Value().(*UserPropagator)
+	if h, ok := p.iface.(EqHandler); ok {
+		old := p.cb
+		p.cb = cb
+		defer func() { p.cb = old }()
+		h.Eq(newExpr(p.ctx, s), newExpr(p.ctx, t))
+	}
+}
+
+// goDiseqCb is exported to C as a callback for Z3_eq_eh (disequality).
+//
+//export goDiseqCb
+func goDiseqCb(ctx C.uintptr_t, cb C.Z3_solver_callback, s C.Z3_ast, t C.Z3_ast) {
+	p := cgo.Handle(ctx).Value().(*UserPropagator)
+	if h, ok := p.iface.(DiseqHandler); ok {
+		old := p.cb
+		p.cb = cb
+		defer func() { p.cb = old }()
+		h.Diseq(newExpr(p.ctx, s), newExpr(p.ctx, t))
+	}
+}
+
+// goFinalCb is exported to C as a callback for Z3_final_eh.
+//
+//export goFinalCb
+func goFinalCb(ctx C.uintptr_t, cb C.Z3_solver_callback) {
+	p := cgo.Handle(ctx).Value().(*UserPropagator)
+	if h, ok := p.iface.(FinalHandler); ok {
+		old := p.cb
+		p.cb = cb
+		defer func() { p.cb = old }()
+		h.Final()
+	}
+}
+
+// goCreatedCb is exported to C as a callback for Z3_created_eh.
+//
+//export goCreatedCb
+func goCreatedCb(ctx C.uintptr_t, cb C.Z3_solver_callback, t C.Z3_ast) {
+	p := cgo.Handle(ctx).Value().(*UserPropagator)
+	if h, ok := p.iface.(CreatedHandler); ok {
+		old := p.cb
+		p.cb = cb
+		defer func() { p.cb = old }()
+		h.Created(newExpr(p.ctx, t))
+	}
+}
+
+// goDecideCb is exported to C as a callback for Z3_decide_eh.
+//
+//export goDecideCb
+func goDecideCb(ctx C.uintptr_t, cb C.Z3_solver_callback, t C.Z3_ast, idx C.uint, phase C.bool) {
+	p := cgo.Handle(ctx).Value().(*UserPropagator)
+	if h, ok := p.iface.(DecideHandler); ok {
+		old := p.cb
+		p.cb = cb
+		defer func() { p.cb = old }()
+		h.Decide(newExpr(p.ctx, t), uint(idx), phase == C.bool(true))
+	}
+}
+
+// goOnBindingCb is exported to C as a callback for Z3_on_binding_eh.
+//
+//export goOnBindingCb
+func goOnBindingCb(ctx C.uintptr_t, cb C.Z3_solver_callback, q C.Z3_ast, inst C.Z3_ast) C.bool {
+	p := cgo.Handle(ctx).Value().(*UserPropagator)
+	if h, ok := p.iface.(OnBindingHandler); ok {
+		old := p.cb
+		p.cb = cb
+		defer func() { p.cb = old }()
+		if h.OnBinding(newExpr(p.ctx, q), newExpr(p.ctx, inst)) {
+			return C.bool(true)
+		}
+		return C.bool(false)
+	}
+	return C.bool(true)
+}
+
+// goOnClauseCb is exported to C as a callback for Z3_on_clause_eh.
+//
+//export goOnClauseCb
+func goOnClauseCb(ctx C.uintptr_t, proofHint C.Z3_ast, n C.uint, deps *C.uint, literals C.Z3_ast_vector) {
+	oc := cgo.Handle(ctx).Value().(*OnClause)
+	var ph *Expr
+	if proofHint != nil {
+		ph = newExpr(oc.ctx, proofHint)
+	}
+	goDepSlice := make([]uint, uint(n))
+	if n > 0 {
+		depSlice := (*[1 << 28]C.uint)(unsafe.Pointer(deps))[:n:n]
+		for i := uint(0); i < uint(n); i++ {
+			goDepSlice[i] = uint(depSlice[i])
+		}
+	}
+	vec := newASTVector(oc.ctx, literals)
+	oc.handler(ph, goDepSlice, vec)
+}

src/api/go/solver.go

@@ -350,6 +350,13 @@ func (s *Solver) SolveFor(variables []*Expr, terms []*Expr, guards []*Expr) {
 	C.Z3_solver_solve_for(s.ctx.ptr, s.ptr, varVec, termVec, guardVec)
 }
 
+// ImportModelConverter imports the model converter from src into this solver.
+// This transfers model simplifications from one solver instance to another,
+// useful when combining results from multiple solver instances.
+func (dst *Solver) ImportModelConverter(src *Solver) {
+	C.Z3_solver_import_model_converter(dst.ctx.ptr, src.ptr, dst.ptr)
+}
+
 // Model represents a Z3 model (satisfying assignment).
 type Model struct {
 	ctx *Context

src/api/java/NativeStatic.txt

@@ -241,3 +241,40 @@ DLL_VIS JNIEXPORT jboolean JNICALL Java_com_microsoft_z3_Native_propagateNextSpl
   Z3_solver_callback cb = info->cb;
   return (jboolean) Z3_solver_next_split((Z3_context)ctx, cb, (Z3_ast)e, idx, Z3_lbool(phase));
 }
+
+struct JavaOnClauseInfo {
+  JNIEnv *jenv = nullptr;
+  jobject jobj = nullptr;
+  jmethodID on_clause = nullptr;
+};
+
+static void java_on_clause_eh(void* _p, Z3_ast proof_hint, unsigned n, unsigned const* deps, Z3_ast_vector literals) {
+  JavaOnClauseInfo *info = static_cast<JavaOnClauseInfo*>(_p);
+  jintArray jdeps = info->jenv->NewIntArray((jsize)n);
+  info->jenv->SetIntArrayRegion(jdeps, 0, (jsize)n, (jint*)deps);
+  info->jenv->CallVoidMethod(info->jobj, info->on_clause, (jlong)proof_hint, jdeps, (jlong)literals);
+  info->jenv->DeleteLocalRef(jdeps);
+}
+
+DLL_VIS JNIEXPORT jlong JNICALL Java_com_microsoft_z3_Native_onClauseInit(JNIEnv *jenv, jclass cls, jobject jobj, jlong ctx, jlong solver) {
+  JavaOnClauseInfo *info = new JavaOnClauseInfo;
+  info->jenv = jenv;
+  info->jobj = jenv->NewGlobalRef(jobj);
+  jclass jcls = jenv->GetObjectClass(info->jobj);
+  info->on_clause = jenv->GetMethodID(jcls, "onClauseWrapper", "(J[IJ)V");
+  if (!info->on_clause) {
+    jenv->DeleteGlobalRef(info->jobj);
+    delete info;
+    return 0;
+  }
+  Z3_solver_register_on_clause((Z3_context)ctx, (Z3_solver)solver, info, java_on_clause_eh);
+  return (jlong)info;
+}
+
+DLL_VIS JNIEXPORT void JNICALL Java_com_microsoft_z3_Native_onClauseDestroy(JNIEnv *jenv, jclass cls, jlong javainfo) {
+  JavaOnClauseInfo *info = (JavaOnClauseInfo*)javainfo;
+  if (info) {
+    info->jenv->DeleteGlobalRef(info->jobj);
+    delete info;
+  }
+}

src/api/java/OnClause.java

@@ -0,0 +1,85 @@
+/**
+Copyright (c) 2012-2014 Microsoft Corporation
+   
+Module Name:
+
+    OnClause.java
+
+Abstract:
+
+    Callback on clause inferences
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-19
+
+Notes:
+
+**/
+
+package com.microsoft.z3;
+
+/**
+ * Clause inference callback.
+ * <p>
+ * Allows users to observe clauses learned during solving.
+ * Useful for custom learning strategies, clause sharing in parallel solvers,
+ * debugging, and proof extraction.
+ * </p>
+ * <p>
+ * Usage: create an instance, override {@link #onClause(Expr, int[], ASTVector)},
+ * and close the instance when done.
+ * </p>
+ **/
+public class OnClause implements AutoCloseable {
+
+    private long javainfo;
+    private final Context ctx;
+
+    /**
+     * Creates an on-clause callback for the given solver.
+     *
+     * @param ctx    The Z3 context
+     * @param solver The solver to register the callback with
+     * @throws Z3Exception
+     **/
+    public OnClause(Context ctx, Solver solver) {
+        this.ctx = ctx;
+        javainfo = Native.onClauseInit(this, ctx.nCtx(), solver.getNativeObject());
+    }
+
+    /**
+     * Called when a clause is inferred during solving.
+     * <p>
+     * The life-time of {@code proof_hint} and {@code literals} is limited to
+     * the scope of this callback. If you want to store them, you must duplicate
+     * the expressions or extract the literals before returning.
+     * </p>
+     *
+     * @param proof_hint A partial or comprehensive derivation justifying the inference (may be null)
+     * @param deps       Dependency indices
+     * @param literals   The inferred clause as a vector of literals
+     **/
+    public void onClause(Expr<?> proof_hint, int[] deps, ASTVector literals) {}
+
+    /**
+     * Internal wrapper called from JNI. Do not override.
+     **/
+    final void onClauseWrapper(long proofHintPtr, int[] deps, long literalsPtr) {
+        Expr<?> proof_hint = proofHintPtr != 0 ? (Expr<?>) Expr.create(ctx, proofHintPtr) : null;
+        ASTVector literals = new ASTVector(ctx, literalsPtr);
+        onClause(proof_hint, deps, literals);
+    }
+
+    /**
+     * Unregisters the callback and frees associated resources.
+     * Must be called when the callback is no longer needed.
+     **/
+    @Override
+    public void close() {
+        if (javainfo != 0) {
+            Native.onClauseDestroy(javainfo);
+            javainfo = 0;
+        }
+    }
+}

src/api/java/Solver.java

@@ -548,6 +548,16 @@ public class Solver extends Z3Object {
                                      var.getNativeObject(), value.getNativeObject());
     }
 
+    /**
+     * Import model converter from other solver.
+     *
+     * @param src The solver to import the model converter from
+     **/
+    public void importModelConverter(Solver src)
+    {
+        Native.solverImportModelConverter(getContext().nCtx(), src.getNativeObject(), getNativeObject());
+    }
+
     /**
      * Create a clone of the current solver with respect to{@code ctx}.
      */