Z3 Java Application Development

Question

I am developing a rulebased system application using Java and HTML (Jsp), MySQL DB and Apache Tomcat Server. Basically I need to build a system to store rules in my database and then check for the satisfiablity of the rules in my DB. I have researched on this and found Z3 as a suitable tool for this purpose. My aim is to write a script in java to produce an output which is understandable to z3 of the type given on - https://rise4fun.com/z3 . For this as suggested in a different answer by a user, it was suggested that the easiest way was to write my script in java to produce the z3 code and then feed it to z3 to check whether it is sat or unsat. Now Im confused as to how I can integrate this into my project ? Is the only way to deal with the problem to try and run the z3 java bindings which shall make it very difficult to work with ? I basically need a standalone service such as https://rise4fun.com/z3 which takes my input and gives me the output and that can be integrated into my project. Even a jar file will do. Something that can be integrated with eclipse maybe

Answer 1

There isn't an obvious answer to your question since it all "depends" on what your project parameters are.

Z3 bindings come in different flavors. The C/C++/Java ones are fairly low-level. You can use them to access all SMTLib functionality, and also extra things. You can build standalone executables and ship them. That's all great. But it comes at the cost of being quite low level, hard to program and get right, debug, and maintain. I'd strongly caution against using them especially if you're new to SMT solving in general.

The Python bindings, on the other hand, is quite higher level. It does require an installation of Z3 on the target machine. If you can use that, I'd recommend doing so as it is the easiest to use.

If you have to stick to Java, and if you're a newcomer, I'd recommend sticking to SMTLib format: Generate text files containing your input, send to Z3 via a file-system pipe, or with a call to system or such, and parse the results back. That'll make sure you have the right framework built. Once you're comfortable with that, you can directly use the Java bindings to gain speed and also get rid of the requirement that z3 needs to be installed on the target machine.

As an example of how different the styles would be check-out this answer: https://stackoverflow.com/a/50576844/936310 There, a floating-point SMT problem is tackled first using the C bindings, and then Python, and Haskell; and you can see the difference. Your Java solution will look a lot like the C version.