Improve SMT translation

[WolframPfeifer]

At the moment, our SMT translation is "weaker" than the internal strategy of KeY. This can be seen for instance in some of our examples, where the built-in strategy is able to close some goals but SMT is not.

Underlying problem

The problem is that some information, such as the object/class invariants, is not translated to SMT, and other information that is translated, such as type hierarchy and embedding, might hinder the solver.

Usage Scenario

A good idea would be to just choose auto-provable an example from those shipped with KeY, and try to make it provable with SMT solvers:

1. Load built-in example, for instance Algorithms -> SaddlebackSearch.
2. Run the macro "SMT preparation".
3. Run an SMT solver.

In this example, not all branches are closed afterwards (it is closeable automatically with the built-in strategy in about 26k steps). Some insights are:

• There are some very easy branches where the object invariant has to be proven, which is actually just true in this case, but the SMT solver does not know about it and instead only sees an uninterpreted symbol.
• When One-Step-Simplification is disabled in the Strategy Settings, the updates do not get applied in the "SMT preparation" step. It seems that the SMT solver does not find a solution for some of the branches. Not sure how updates are treated at the moment ("let" expressions?), so that is a point for investigation and possible improvement.

Improvement Ideas

• Develop a translation for invariants.
• Implement a better treatment for some operators/types (e.g. bounded sums or sequences).
• Another point that hinders the SMT solver might be the type hierarchy and embedding of int/boolean into a "Universe" type U (see Option to disable the type hierarchy in the SMT translation #1703).
• ...

Additional context

This is a candidate group topic for the 3rd HacKeYthon. It supersedes #1703 now, which was only part of the problem.

[mattulbrich]

What about other constructs beyond invariants?

• Model method contracts
• Model method definitions
• Model field definitions (generalised case of invariants)
• dependency reasoning

We should investigate which constructs are the reason why Z3 cannot close relevant KeY examples automatically.
It might also be that a collection of smaller taclets from KeY need to be marked for inclusion into the SMT translation.

[WolframPfeifer]

I totally agree. That could be the task at the HacKeYthon, and I think it would greatly improve KeY by the SMT translation more useful. The borderline that I would draw is at the Java taclets: I think that the symbolic execution should be done by KeY.

It will be to investigate what the performance impact of providing all this additional information is for the SMT solving (in particular, I am thinking of invariants for recursive structures, such as trees). If it is too large, we could also consider an incremental process, i.e. translating only the first-order part in the beginning (with relatively small timeouts), and then gradually adding more formulas.