-
Notifications
You must be signed in to change notification settings - Fork 1.5k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Java API for custom User Propagators #6097
Comments
For .net I had to change update_api.py to declare callbacks
Something similar has to be done for Java. At this point only the error handler is declared for Java. |
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. Edit:
But as far as I can see, there is no way to obtain for any Java-side function a corresponding function pointer
Does this sound reasonable? I'm not at all familar with JNI, so maybe someone with more insight has a better idea? |
Make it easier to add native methods for callbacks (for user propagator) #6097 The Java User propagator wrapper should define a base class with virtual methods that can be invoked from functions defined in NativeStatic.txt
I got some time to look more into this JNI business and I noticed something odd. |
None of the callback functionality is tested or exposed over Java at this point.
that sets a default type. |
I'm under the impression that it might be best to actually create a whole |
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). |
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. |
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. Nikolaj |
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: 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? |
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. You will also need to heap-allocate Of course, there is also the error handling that is missing. |
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
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);
}
}
}
|
This call creates a JavaInfo C++ object and stores it in a global map. Instead of returning void, return this object and store it in UserPropagatorBase? |
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). |
I'm wondering if it is possible to make the exposure of the UserPropagator feature less dependent on the Z3 Java API. |
I updated my code based on your advice. I created |
If you add a pull request. |
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.
src/api/java
and that there is themk_make.py
script. I don't fully understand the process though. For example, is theNative
class used throughout thesrc/api/java
generated bymk_make.py
(I didn't find it). DoesNative
already expose the necessary functionality but the Java API simple misses a nice wrapper?I know that my questions are not very concrete, but maybe I can still find some help :).
The text was updated successfully, but these errors were encountered: