Add missing API bindings: importModelConverter, OnClause, and user propagator

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

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}.
      */