Fixes in Java's User Propagator (#7088)

* Fixed decide callback for Java user propagators * Java User Prop: - Added return value to conflict - Added consequence method - Added missing access modifier to decideWrapper * Removed type parameters of expressions in UserPropagatorBase * Renamed propagateConflict to propagateConsequence
Z3Prover · Jan 18, 2024 · d2706ba · d2706ba
1 parent 2c55aa5
commit d2706ba
Show file tree

Hide file tree

Showing 3 changed files with 31 additions and 17 deletions.
diff --git a/scripts/update_api.py b/scripts/update_api.py
@@ -641,8 +641,8 @@ def mk_java(java_src, java_dir, package_name):
   public static native void propagateRegisterEq(Object o, long ctx, long solver);
   public static native void propagateRegisterDecide(Object o, long ctx, long solver);
   public static native void propagateRegisterFinal(Object o, long ctx, long solver);
-  public static native void propagateConflict(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 void propagateAdd(Object o, long ctx, long solver, long javainfo, long e);
+  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);
 
@@ -698,6 +698,8 @@ def mk_java(java_src, java_dir, package_name):
     protected abstract void createdWrapper(long le);
 
     protected abstract void fixedWrapper(long lvar, long lvalue);
+
+    protected abstract void decideWrapper(long lvar, int bit, boolean is_pos);
   }
     """)
     java_native.write('\n')

diff --git a/src/api/java/NativeStatic.txt b/src/api/java/NativeStatic.txt
@@ -150,7 +150,7 @@ static void final_eh(void* _p, Z3_solver_callback cb) {
 static void decide_eh(void* _p, Z3_solver_callback cb, Z3_ast _val, unsigned bit, bool is_pos) {
   JavaInfo *info = static_cast<JavaInfo*>(_p);
   ScopedCB scoped(info, cb);
-  info->jenv->CallVoidMethod(info->jobj, info->decide, (jlong)_val);
+  info->jenv->CallVoidMethod(info->jobj, info->decide, (jlong)_val, bit, is_pos);
 }
 
 DLL_VIS JNIEXPORT jlong JNICALL Java_com_microsoft_z3_Native_propagateInit(JNIEnv *jenv, jclass cls, jobject jobj, jlong ctx, jlong solver) {
@@ -166,7 +166,7 @@ DLL_VIS JNIEXPORT jlong JNICALL Java_com_microsoft_z3_Native_propagateInit(JNIEn
   info->fixed = jenv->GetMethodID(jcls, "fixedWrapper", "(JJ)V");
   info->eq = jenv->GetMethodID(jcls, "eqWrapper", "(JJ)V");
   info->final = jenv->GetMethodID(jcls, "finWrapper", "()V");
-  info->decide = jenv->GetMethodID(jcls, "decideWrapper", "(JII)V");
+  info->decide = jenv->GetMethodID(jcls, "decideWrapper", "(JIZ)V");
 
   if (!info->push || !info->pop || !info->fresh || !info->created || !info->fixed || !info->eq || !info->final || !info->decide) {
     assert(false);
@@ -203,15 +203,16 @@ DLL_VIS JNIEXPORT void JNICALL Java_com_microsoft_z3_Native_propagateRegisterDec
   Z3_solver_propagate_decide((Z3_context)ctx, (Z3_solver)solver, decide_eh);
 }
 
-DLL_VIS JNIEXPORT void JNICALL Java_com_microsoft_z3_Native_propagateConflict(JNIEnv * jenv, jclass cls, jobject jobj, jlong ctx, jlong solver, jlong javainfo, long num_fixed, jlongArray fixed, long num_eqs, jlongArray eq_lhs, jlongArray eq_rhs, jlong conseq) {
+DLL_VIS JNIEXPORT jboolean JNICALL Java_com_microsoft_z3_Native_propagateConsequence(JNIEnv * jenv, jclass cls, jobject jobj, jlong ctx, jlong solver, jlong javainfo, long num_fixed, jlongArray fixed, long num_eqs, jlongArray eq_lhs, jlongArray eq_rhs, jlong conseq) {
   JavaInfo *info = (JavaInfo*)javainfo;
   GETLONGAELEMS(Z3_ast, fixed, _fixed);
   GETLONGAELEMS(Z3_ast, eq_lhs, _eq_lhs);
   GETLONGAELEMS(Z3_ast, eq_rhs, _eq_rhs);
-  Z3_solver_propagate_consequence((Z3_context)ctx, info->cb, num_fixed, _fixed, num_eqs, _eq_lhs, _eq_rhs, (Z3_ast)conseq);
+  bool retval = Z3_solver_propagate_consequence((Z3_context)ctx, info->cb, num_fixed, _fixed, num_eqs, _eq_lhs, _eq_rhs, (Z3_ast)conseq);
   RELEASELONGAELEMS(fixed, _fixed);
   RELEASELONGAELEMS(eq_lhs, _eq_lhs);
   RELEASELONGAELEMS(eq_rhs, _eq_rhs);
+  return (jboolean) retval;
 }
 
 DLL_VIS JNIEXPORT void JNICALL Java_com_microsoft_z3_Native_propagateAdd(JNIEnv * jenv, jclass cls, jobject jobj, jlong ctx, jlong solver, jlong javainfo, jlong e) {
@@ -227,8 +228,8 @@ DLL_VIS JNIEXPORT void JNICALL Java_com_microsoft_z3_Native_propagateAdd(JNIEnv
 }
 
 
-DLL_VIS JNIEXPORT bool JNICALL Java_com_microsoft_z3_Native_propagateNextSplit(JNIEnv * jenv, jclass cls, jobject jobj, jlong ctx, jlong solver, jlong javainfo, jlong e, long idx, int phase) {
+DLL_VIS JNIEXPORT jboolean JNICALL Java_com_microsoft_z3_Native_propagateNextSplit(JNIEnv * jenv, jclass cls, jobject jobj, jlong ctx, jlong solver, jlong javainfo, jlong e, long idx, int phase) {
   JavaInfo *info = (JavaInfo*)javainfo;
   Z3_solver_callback cb = info->cb;
-  return Z3_solver_next_split((Z3_context)ctx, cb, (Z3_ast)e, idx, Z3_lbool(phase));
+  return (jboolean) Z3_solver_next_split((Z3_context)ctx, cb, (Z3_ast)e, idx, Z3_lbool(phase));
 }
diff --git a/src/api/java/UserPropagatorBase.java b/src/api/java/UserPropagatorBase.java
@@ -60,36 +60,47 @@ protected final void fixedWrapper(long lvar, long lvalue) {
         fixed(var, value);
     }
 
+    @Override
+    protected final void decideWrapper(long lvar, int bit, boolean is_pos) {
+        Expr var = new Expr(ctx, lvar);
+        decide(var, bit, is_pos);
+    }
+
     public abstract void push();
 
     public abstract void pop(int number);
 
     public abstract UserPropagatorBase fresh(Context ctx);
 
-    public <R extends Sort> void created(Expr<R> ast) {}
+    public void created(Expr<?> ast) {}
 
-    public <R extends Sort> void fixed(Expr<R> var, Expr<R> value) {}
+    public void fixed(Expr<?> var, Expr<?> value) {}
 
-    public <R extends Sort> void eq(Expr<R> x, Expr<R> y) {}
+    public void eq(Expr<?> x, Expr<?> y) {}
+
+    public void decide(Expr<?> var, int bit, boolean is_pos) {}
 
     public void fin() {}
 
-    public final <R extends Sort> void add(Expr<R> expr) {
+    public final void add(Expr<?> expr) {
         Native.propagateAdd(this, ctx.nCtx(), solver.getNativeObject(), javainfo, expr.getNativeObject());
     }
 
-    public final <R extends Sort> void conflict(Expr<R>[] fixed) {
-        conflict(fixed, new Expr[0], new Expr[0]);
+    public final boolean conflict(Expr<?>[] fixed) {
+        return conflict(fixed, new Expr[0], new Expr[0]);
+    }
+
+    public final boolean conflict(Expr<?>[] fixed, Expr<?>[] lhs, Expr<?>[] rhs) {
+        return consequence(fixed, lhs, rhs, ctx.mkBool(false));
     }
 
-    public final <R extends Sort> void conflict(Expr<R>[] fixed, Expr<R>[] lhs, Expr<R>[] rhs) {
-        AST conseq = ctx.mkBool(false);
-        Native.propagateConflict(
+    public final boolean consequence(Expr<?>[] fixed, Expr<?>[] lhs, Expr<?>[] rhs, Expr<?> conseq) {
+        return Native.propagateConsequence(
             this, ctx.nCtx(), solver.getNativeObject(), javainfo,
             fixed.length, AST.arrayToNative(fixed), lhs.length, AST.arrayToNative(lhs), AST.arrayToNative(rhs), conseq.getNativeObject());
     }
 
-    public final <R extends Sort> boolean nextSplit(Expr<R> e, long idx, Z3_lbool phase) {
+    public final boolean nextSplit(Expr<?> e, long idx, Z3_lbool phase) {
         return Native.propagateNextSplit(
             this, ctx.nCtx(), solver.getNativeObject(), javainfo,
             e.getNativeObject(), idx, phase.toInt());