Integrating OpenSMT with JavaSMT

[daniel-raffler]

Hello everyone,
I'm a student at Ludwig-Maximilians-Universität in Munich and have just started my bachelor's thesis. The goal is to add support for OpenSMT to the JavaSMT framework. JavaSMT is a library that provides a common interface for accessing SMT solvers from java programs. Application developers can easily switch between different solvers without having to rewrite their code. You can find more information in these two papers:

• JavaSMT 3: Interacting with SMT Solvers in Java
• JavaSMT: A Unified Interface for SMT Solvers in Java

And the github page can be found here.

As of now I'm still in the design phase, but there are some general questions I'd like to ask:

• One of the issues with integrating OpenSMT is that it requires a logic to be set before anything else can be done. This is in line with the SMT-LIB standard, but most other solvers are more lenient and will guess the right logic when none is specified. In fact JavaSMT does not even offer a way for the user to set a certain logic. There are obvious workarounds, such as caching the formulas in the abstraction layer and then only passing them to the solver once a logic is know, but a more direct approach would be preferred. Are there any plans to add something akin to the ALL logic from SMT-LIB 2.5 to OpenSMT?
• On a related matter: is there a simple way to switch logics at a later point? For instance one might want to start with QF_UF initially, but once a formula that uses integers is added an upgrade to QF_UFLIA is necessary. Is there a way to move the existing declarations over to the new logic?
• Is there an example for using arrays in OpenSMT? There are mkStore and mkSelect in Logic to handle arrays, but I'm not sure how to declare an array variable in the first place.
• Are there any plans to (officially) support bitvectors? The current implementation is limited to a fixed bitwidth and uses its own bitblaster interface instead of the main solver.

Any help would be greatly appreciated!

Daniel

[blishko]

Hi Daniel,

I will try to assist you with integrating OpenSMT to JavaSMT as much as I can.

One of the issues with integrating OpenSMT is that it requires a logic to be set before anything else can be done

Indeed, OpenSMT requires to set logic beforehand. This has been OpenSMT's philosophy for a long time. I support the move to the approach now adopted by most solvers, but it is not easy and would require substantial changes in OpenSMT's codebase and API. We currently do not have capacity to work on this.

On a related matter: is there a simple way to switch logics at a later point?

Unfortunately, no. This is related to the first question, where the philosophy was that you should specify the logic in which you are going to work beforehand.

Is there an example for using arrays in OpenSMT?

We probably do not have example at the moment, but I can write one.

Are there any plans to (officially) support bitvectors?

There are plans, but no time to realize them :) We welcome new contributors :)
The current implementation is very limited and should not be integrated with JavaSMT.

[daniel-raffler]

Hello Martin,
Thanks for adding the example for me! I've so far used a workaround, but this is certainly the better solution.

Ask for using qf_auflira as a logic: I did give it a try and patched in a method Logic::setLogic to assign the proper logic at a later point. The Idee was to initially set qf_auflira when the Logic is created and the switch to the actually needed logic just before the MainSolver is created. It did work for my example, but I was a little worried about introducing new bugs. At least one method in Logic (mkEq) actually depends on the Logic type selected. And I don't know if if the change would cause more issues with the actual solver component as I'm not familiar with that code.

We're therefore currently considering adding a way to select a specific logic to JavaSmt so that the problem can be left for the user to decide. However, l can have another look at using qf_auflira if I still have time left.

[blishko]

I've added QF_AUFLIRA logic (#634) and tested with a few SMT-LIB scripts, where it seems to work. Note that OpenSMT still cannot solve formulas mixing integers and reals, but you can use this general logic for creating both integers and real terms, depending on what the user wants.
However, it would be good if JavaSMT would support specifying the logic beforehand.

[daniel-raffler]

Hello Martin,
thanks a lot for the patch! This should really simplify things for me..

[blishko]

Hi Daniel,

I noticed that you also want to add the support for interpolation. This may not be compatible with the previous workaround with QF_AUFLIRA logic. OpenSMT currently supports interpolation only for QF_UF, QF_LRA and QF_LIA. I would really like to extend it to the more general logics, but I don't have the time at the moment.

[daniel-raffler]

Hello Martin,
I think we'll still have to add a mechanism to let the user set the logic. However, it will only be required for interpolation. Everything else should just work with the new logic you added. (Of course users may still want to pick a weaker logic for performance reasons)

Interpolation was actually one of the main selling points for adding OpenSMT to JavaSMT. Most solver don't support it and it's of interest for CPA Checker which is also being developed here and uses JavaSMT as its backend. If more general logics could be supported in the future we'd certainly be interested ;)