Running SMT solvers without type hierarchy encoding

[WolframPfeifer]

Related Issue

This pull request addresses #1703.

Intended Change

This PR adds an option which allows disabling the type hierarchy in the SMT translation. With that option set, the translation is still sound, but possibly "less complete" than the original translation, but might find some proofs faster, since the embeddings necessary to encode the type hierarchy can mislead the solvers.

Plan

Important

Note: At the moment, the feature is only partially implemented, which leads to many exceptions when trying to run an SMT solver.!

• Fix and finish implementation
• At the moment, a new solver is added (Z3 variant without type hierarchy translation). Maybe it is better to have a toggle that applies to all solvers.
• Document the changes

Type of pull request

• New feature (non-breaking change which adds functionality)
• There are changes to the (Java) code

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
• I added new test case(s) for new functionality.
• I have tested the feature as follows: ...
• I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

This feature was mostly implemented during the 2nd HacKeYthon 2024.
Thanks to @BookWood7th, @roundEaredSengi and @vb213!

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.