User-provided theory solvers in JavaSMT

[ThomasHaas]

Z3 has a feature called user propagators which allows users to provide their own (simple) theory solvers.
Recently, they added Java bindings for this feature as well (merged into master but not yet part of the release version).
We would like to use this in our JavaSMT-based project.

Here is the main question: would you even want to provide such a feature over the JavaSMT interface with only one supporting solver?
If so, we are willing to implement this feature and create a PR.
We have already tried to implement it and it didn't seem too hard to support. However, we failed to understand the build system and how to manually update to a newer (manually built) Z3 version, so we were not able to test it yet.

[kfriedberger]

Hi Thomas,
thanks for your interest in JavaSMT and the idea for extending the interface with a new feature.
JavaSMT has always contained solver-specific code for some features, like interpolation or unsat cores, which are not available in all SMT solvers.

Your request targets Z3, which is a solver with a very broad API, including goal-based solving, theory handling and user propagators. We do not want to copy the complete API and features from Z3, because the user of suh features would then also be bound to Z3, just with the steps through JavaSMT.

I currently may not have fully unterstood the API and I do not yet see the benefit or full potential for that feature. However, if you are willing to provide a well-written pull-request, such that the maintenance of the code is not too complex, we will take a look. Do you plan to make the API solver-independent, i.e. fully implemented with JavaSMT's base classes for Formulas and FormulaTypes?

Our build steps for Z3 depend mainly on the original Z3 binary libraries, see 'doc/Developers-How-to-Release-into-Ivy.md'. You can compile Z3 on your own and simply include the files in the environment. Example: for Linux include 'libz3.so' in the LD_LIBRARY_PATH and provide the Z3.jar in the Java classpath.

Best
Karlheinz

[ThomasHaas]

The idea was to make a solver-independent frontend, i.e., to make it work purely over BooleanFormula (Z3 user propagators can only implement theory solvers for boolean theories). I nudged the Z3 Java binding developer to make the bindings API independent, so that other APIs can be written around it, cause I wanted to have this feature together with the JavaSMT API :).

Some background:
We use JavaSMT in our project because we found other solvers to outperform Z3 by over and order of magnitude in certain tasks, so flexibility in the backend is something we don't wanna miss.
We also have a custom theory solver that currently operates "offline": we ask for a full model from the SMT solver, check this model with the theory solver, and then compute explanations of theory inconsistency if needed.
I believe that running this theory solver "online" could give considerable performance improvements, but at the same time we do not want to fully stick to Z3 since it performs badly in some tasks, and there are cases where we cannot even run our own theory solver at all.

A rough sketch of what I have in mind for theory solvers would be this:

// In ProverEnvironment
   public void registerTheorySolver(TheorySolver solver);
   public void registerTheoryLiteral(BooleanFormula literal, TheorySolver solver); // Register what literals should be handled by the solver.
   
   
// Theory solver interface
public interface TheorySolver {
       // the following methods are called by the SMT engine (naming subject to change)
       void onPop() // Solver backtracks
       void onPush(int level): // Solver pushes new decision level
       void onFixed(BooleanFormula lit, boolean value); // Solver fixed value of a literal (decision or unit propagation)
       void onFinish() // Solver terminated
       // ... possibly more
       
       void setSMTBackend(SMTBackend backend); // Used to inject a backend to communicate with
       // In onFixed and onFinish, the theory solver can call backend.propagate/backend.conflict to do theory propagation and raise conflicts
}


// SMT backend (there would only exist a Z3SMTBackend for now)
public interface SMTBackend {

     void propagate(BooleanFormula[] fixedLiterals, BooleanFormula consequence); //   "/\fixedLiterals  =>  consequence"
     default void conflict (BooleanFormula[] fixedLiterals) { 
             propagate(fixedLiterals, makeFalse()); //  /\fixedLiterals => false
     }
}

Our build steps for Z3 depend mainly on the original Z3 binary libraries, see 'doc/Developers-How-to-Release-into-Ivy.md'. You can compile Z3 on your own and simply include the files in the environment. Example: for Linux include 'libz3.so' in the LD_LIBRARY_PATH and provide the Z3.jar in the Java classpath.

Thank you for the pointers. We (or rather my student) already ran into problems a few times, so I expect to ask some more detailed questions regarding the build/release process of JavaSMT.

With best regards,
Thomas

[ThomasHaas]

I want to give an update on this.
We have successfully implemented the Z3 user propagators (at least parts of it) in JavaSMT and they work like a charm.
We observed orders of magnitude speed up on model enumeration of the Nqueens problem (compared against the standard blocking clauses approach). To our surprise, the overhead of communicating with the native solver over Java seems to be almost negligible.

I will open a PR in the coming days. However, this feature requires the newest release of Z3 which is not yet available via JavaSMT's ivy repo I believe. For now I just locally built Z3, added it to the JavaSMT project, and removed the outdated version from build.xml (which is an ugly hack, but I didn't wanna bother too much with the build system for now).

[kfriedberger]

User propagator is integrated into JavaSMT since v5.0.0.