Java API for custom User Propagators

[ThomasHaas]

I have a custom theory solver implemented in Java that currently interacts with Z3 in an offline-scheme, meaning it waits for Z3 to produce a full model, extracts theory literals (only booleans) performs theory reasoning, and then generates boolean lemmas that get added to the solver. This approach works quite well, but I suspect a lot more performance can be gained with an incremental online integration. Rewriting the solver into C++ and integrating it into Z3 is not really an option though.

Now I'm wondering if it is possible to effectively use the user propagators of Z3 to integrate a Java-based theory solver with Z3. I do have some concerns, though.

• I know that the Java API does not expose user propagators, but the C++ and the Python API do. How does one go about extending the Java API to support this feature? I know that there issrc/api/java and that there is the mk_make.py script. I don't fully understand the process though. For example, is the Native class used throughout the src/api/java generated by mk_make.py (I didn't find it). Does Native already expose the necessary functionality but the Java API simple misses a nice wrapper?
• Is it even reasonable to have a custom theory solver on the Java-side? Are there any crucial limitations to what the user propagators can do?

I know that my questions are not very concrete, but maybe I can still find some help :).

[NikolajBjorner]

For .net I had to change update_api.py to declare callbacks

    for name, ret, sig in Closures:
        sig = sig.replace("void*","voidp").replace("unsigned","uint")
        sig = sig.replace("Z3_ast*","ref IntPtr").replace("uint*","ref uint").replace("Z3_lbool*","ref int")
        ret = ret.replace("void*","voidp").replace("unsigned","uint")
        if "*" in sig or "*" in ret:
            continue
        dotnet.write('        [UnmanagedFunctionPointer(CallingConvention.Cdecl)]\n')
        dotnet.write('        public delegate %s %s(%s);\n' % (ret,name,sig))

    dotnet.write('        public class LIB\n')
    dotnet.write('        {\n')
    dotnet.write('            const string Z3_DLL_NAME = \"libz3\";\n'
                 '            \n')
    dotnet.write('            [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]\n')
    dotnet.write('            public extern static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1);\n\n')

Something similar has to be done for Java. At this point only the error handler is declared for Java.

[ThomasHaas]

Oh, I didn't know that .NET already has bindings for the user propagators. Seeing the C# code helps me to understand how the Java wrapper should work. But unfortunately, Java also has this whole JNI-business going on, which I think will require quite a bit of work. Especially handling callbacks to the Java-side likely requires some workarounds as Java does not directly support function pointers. The pointer to update_api.py helped me to understand where and how the JNI wrapper gets generated though, so thank you for that.

Edit: I found the JNI-wrapper to already contain functions to register callbacks like e.g.

DLL_VIS JNIEXPORT void JNICALL Java_com_microsoft_z3_Native_INTERNALsolverPropagateFixed(JNIEnv * jenv, jclass cls, jlong a0, jlong a1, jlong a2) {
  Z3_solver_propagate_fixed((Z3_context)a0, (Z3_solver)a1, (Z3_fixed_eh*)a2);
}

But as far as I can see, there is no way to obtain for any Java-side function a corresponding function pointer a2, that can be passed to this JNI function. Am I right about this? And if so, is this the only missing piece to support user propagators in Java? My idea would be to do something along the line of this:

public interface FixedEh {
       // contains a single method matching the native function pointer
}
//......

native long INTERNALFixedEhToPtr(FixedEh fixedEh); // Creates a native function ptr in the JNI-Wrapper that calls invokes the provided Java-side function. Returns the pointer.
// This function likely needs to create a C-Object that keeps a reference to the JNI-object instance correspinding to <fixedEh>. How to deal with deleting this object again?

// ----- Usage ----

FixedEh callback = myJavasideFunction; // Get function we want to invoke.
long funcPtr = INTERNALFixedEhToPtr(callback); // Create native function ptr to register as callback
INTERNALsolverPropagateFixed(context, solver, funcPtr); // Register native function ptr

Does this sound reasonable? I'm not at all familar with JNI, so maybe someone with more insight has a better idea?

[ThomasHaas]

I got some time to look more into this JNI business and I noticed something odd. On the Java-side in Native.java, the methods that register callbacks like INTERNALsolverPropagateInit take the function pointers as objects from type LongPtr, i.e. a Java class that wraps a single long value. The corresponding JNI wrapper function, however, takes a plain jlong and not a jobject as parameter. This seems like a type-mismatch in the signatures. I think the native side is correct though and the parameter on the Java side should be a plain long instead of LongPtr.

[NikolajBjorner]

None of the callback functionality is tested or exposed over Java at this point. The culprit for your observation centers around code like in update_api.py

def type2javaw(ty):
    global Type2JavaW
    if (ty >= FIRST_FN_ID):
        return 'jlong'
    else:
        return Type2JavaW[ty]

that sets a default type.

[ThomasHaas]

I'm under the impression that it might be best to actually create a whole UserPropagator object on the C++-side that wraps a Java-sided user propagator object (as a jobject) and then forwards the callbacks to that one. But this requires quite a bit of wrapper code that doesn't fit well into the automatically generated one I believe. On the other hand, handling any form of callbacks to Java seems to require some form of JNI-wrapper classes (either ones that wrap the the individual java-sided callback methods or one that wraps the whole user propagator).

[NikolajBjorner]

I created the file https://github.com/Z3Prover/z3/blob/master/src/api/java/NativeStatic.txt to allow adding wrapper functionality more easily. It is used by auto-generation (I need to take away the first line that says the file itself is automatically generated, because it is a lie).

[ThomasHaas]

I saw that change but I was a little hesitant with writing full on wrapper code/classes there, cause at the moment the manually written code is just helper functions/macros. I will see if I can manually write a C++ user propagator that relays all callbacks to the Java side and then see how much of this process can be automated.

[NikolajBjorner]

Thanks, sounds like a good plan. If there is a prescription of how to automate it, then it may be possible to communicate it in case you are not comfortable with changing update_api.py (which is fairly bloated).

Note that the C# propagator is still work in progress. We are testing it and finding quirks in the process so developing the wrapper is better done in sync with an application.

Nikolaj

[d1tto]

I look at the c++ and python api implementations, and it seems possible to consider using a similar approach. We can implement a wrapper function in jni code and then call the virtual methods implemented in java code (if we can). I haven't written jni code before, here's my pseudo-code: Native.cpp

struct JavaInfo {
    JNIEnv *jenv;
    jclass  cls;
    jobject jobj; // point to the object of the baseclass of `UserPropgatorBase`
};

map<joject, Z3_solver_callback> cb_map;
struct scope_cb {
    scoped_cb(jobject jobj, Z3_solver_callback cb) {
        map[jobj] = cb;
    }
    ~scoped_cb() {
        map[jobj] = nullptr;
    }
};

// default callback. pop_eh and fresh_eh are similar to push_eh
static void push_eh(void* _p, Z3_solver_callback cb) {
    JavaInfo *info = static_cast<JavaInfo*>(_p);
    scoped_cb _cb(info->jobj, cb);
    jmethodID methodID = getMethodID(info->jenv, info->cls, "pushWrapper", ...);
    CallVoidMethod(info->jenv, info->jobj, methodID, ...); // try to call the method overrided
}

JNIEXPORT jvoid JNICALL Java_com_microsoft_z3_Native_propagateInit(JNIEnv * jenv, jclass cls, jobject jobj, jlong ctx, jlong solver) {
    JavaInfo info = {
        .jenv = jenv,
        .cls = cls,
        .jobj = jobj
    };
    Z3_solver_propagate_init(ctx, solver, &info, push_eh, pop_eh, fresh_eh);
}

// callback needs to be registered
static void fixed_eh(void* _p, Z3_solver_callback cb, Z3_ast _var, Z3_ast _value) {
    JavaInfo *info = static_cast<JavaInfo*>(_p);
        scoped_cb _cb(info->jobj, cb);
    jmethodID methodID = getMethodID(info->jenv, info->cls, "fixedWrapper", ...);
    CallVoidMethod(info->jenv, info->jobj, methodID, _var, _value); // I don't know if I can do this.
}

JNIEXPORT jvoid JNICALL Java_com_microsoft_z3_Native_registerFixed(JNIEnv * jenv, jclass cls, jobject jobj, jlong ctx, jlong solver) {
    JavaInfo info = {
        .jenv = jenv,
        .cls = cls,
        .jobj = jobj
    };
    Z3_solver_propagate_fixed(ctx, solver, fixed_eh);
}

UserPropgatorBase.java

class UserPropgatorBase {
       UserPropgatorBase() {
        propagateInit(ctx, solver);
    }

    void pushWrapper() {
        ...
        }

    void fixedWrapper(AST var, AST value) {
        ...
    }
}

Is it feasible to do so?

[NikolajBjorner]

Adding user propagator to Java is of course feasible. The trick is to test it.

[ThomasHaas]

The pseudo-code looks fine in principle, but there are many details that need you need to take care of. For example, you cannot just hold a jobject that was passed from Java to C inside a struct. You need to call NewGlobalRef(jenv, jobject) to obtain global/persistence references that you can store. I think there is a similar issue with keeping the jenv stored correctly. Also, I'm not sure if you can use those references as keys in a map (do you even need that cb_map?).

You will also need to heap-allocateJavaInfo structs so you can pass their addresses to the Z3_solver_propagate_init function. To avoid memory leaks, you need to clean up both JavaInfo and the created global refs (using DeleteGlobalRef) somehow. I don't know what the best approach to this is though.

Of course, there is also the error handling that is missing.

[d1tto]

Thank you for your help. With your help, I've written some code not pretty in z3-javabindings. The code has some strange indentation. This code can interact with the simple test code below. What are the defects of these codes that need to be modified

class Test extends UserPropagatorBase {
    public Test(Context context, Solver solver) {
        super(context, solver);
        registerCreated();
        registerFixed();
        registerFinal();
    }

    private List<Expr> fixedValue = new LinkedList<Expr>();

    @Override
    public void push() {
        System.out.println("my push");
    }

    @Override
    public void pop(int i) {
        System.out.println("my pop");
    }

    @Override
    public void fin() {
        conflict(fixedValue.toArray(new Expr[0]));
        System.out.println("my final");
    }

    @Override
    public UserPropagatorBase fresh(Context context) {
        System.out.println("my fresh");
        return this;
    }

    @Override
    public void fixed(Expr var, Expr value) {
        System.out.println("fixed: ");
        System.out.println(var);
        System.out.println(value);
        fixedValue.add(var);
    }
}

public class Main {
    public static void main(String[] args) {
        Context ctx = new Context();
        Solver solver = ctx.mkSolver();
        Test ms = new Test(ctx, solver);
        Sort stringSort = ctx.getStringSort();

        Sort[] params = {stringSort, stringSort};
        FuncDecl equalDecl = ctx.mkPropagateFunction(ctx.mkSymbol("Equal"), params, ctx.mkBoolSort());

        Symbol[] syms1 = {ctx.mkSymbol("String")};
        Sort[] sorts1 = {stringSort};
        Symbol[] syms2 = {ctx.mkSymbol("Equal")};
        FuncDecl[] decls = {equalDecl};
        Expr[] exprs = ctx.parseSMTLIB2File("/home/wxy/Desktop/z3/myz3-test/tests/test.smt", syms1, sorts1, syms2, decls);
        solver.add(exprs);
        if (solver.check() == Status.SATISFIABLE) {
            Model model = solver.getModel();
            System.out.println(model);
        }
    }
}

Adding user propagator to Java is of course feasible. The trick is to test it.

The pseudo-code looks fine in principle, but there are many details that need you need to take care of. For example, you cannot just hold a jobject that was passed from Java to C inside a struct. You need to call NewGlobalRef(jenv, jobject) to obtain global/persistence references that you can store. I think there is a similar issue with keeping the jenv stored correctly. Also, I'm not sure if you can use those references as keys in a map (do you even need that cb_map?).

You will also need to heap-allocateJavaInfo structs so you can pass their addresses to the Z3_solver_propagate_init function. To avoid memory leaks, you need to clean up both JavaInfo and the created global refs (using DeleteGlobalRef) somehow. I don't know what the best approach to this is though.

Of course, there is also the error handling that is missing.

[NikolajBjorner]

Native.propagateInit(this, ctx.nCtx(), solver.getNativeObject());

This call creates a JavaInfo C++ object and stores it in a global map. https://github.com/d1tto/z3-JavaBindings/blob/e858d06107ae9b401898089177ed865f8c7dc772/src/api/java/NativeStatic.txt#L162

Instead of returning void, return this object and store it in UserPropagatorBase?

[NikolajBjorner]

I would punt on implementing decide fully for a first pass. It has more complicated calling conventions. The python bindings currently don't implement decide (correctly).

https://github.com/d1tto/z3-JavaBindings/blob/e858d06107ae9b401898089177ed865f8c7dc772/src/api/java/NativeStatic.txt#L153

[ThomasHaas]

I'm wondering if it is possible to make the exposure of the UserPropagator feature less dependent on the Z3 Java API. Currently, the code in Native.java and its native counterpart are totally independent of Z3's Java API. In fact, the API just "wraps" Native.java into a more user-friendly package. A nice consequence of this is that one can define alternative APIs around Native.java, for example as done by JavaSMT. However, the current proposal (as far as I understand) breaks this clean separation. While I understand that this is no real concern for the development of Z3 (why would you bother about external APIs?), I think it might not be too hard to keep the separation to a certain extent. I haven't thought this through yet, but my suggestion is to have in Native.java a NativeUserPropagator class that contains all the event handler functions but without any implicit wrapping of the parameters into Z3's API types. Then the Z3 Java API can have a UserPropagator(Base) that internally keeps a custom implementation (subclass) of NativeUserPropagator that wraps the parameters according to the API and then delegates the call up to the user-implemented UserPropagator. This way, externally defined APIs can reuse NativeUserPropagator but provide their own API-compatible wrappings.

[d1tto]

I updated my code based on your advice. I created NativeUserPropagator class in Native.java and wrappers for each callback function. In addition, I store the address of JavaInfo object in NativeUserPropagator instead of global map. Is there any chance that this code will be merged?

[NikolajBjorner]

If you add a pull request.