Improve the SMT translation by translating axiom taclets (mostly for invariants)

[WolframPfeifer]

This PR adds axioms for some (dynamically generated) taclets to the SMT translation. Most of these taclets are axioms for class invariants (static/non-static, free, ...).

Additionally, the semantics of the bsum binder should be translated (not yet working).

Related Issue

This pull request addresses (parts of) #3555.

Plan

The goal was to make SaddleBackSearch and SumAndMax provable with SMT prep. macro + Z3. At the moment, most of the branches close but two subgoals are left open (probably because of bsum).

• Translate generated axiom taclets (static/non-static/free/free static inv., partial inv., represents axioms)
• Find a way to translate more complicated taclets (varcond, more complex schema variables...)
• Translate bsum, bprod, etc.? We looked into it a bit, maybe we could use the technique described in "Reasoning about comprehensions with first-order SMT solvers" (Leino and Monahan, 2009, https://dl.acm.org/doi/abs/10.1145/1529282.1529411).
• Code cleanup
• 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)

Some implementation details and considerations:

• At the moment, assertions for all the (generated invariant, model method definition, and represents) taclets are added eagerly. If that turns out to inflate the problem too much and induce a significant performance decrease, we could in the future try to add them lazily. However, in my manual experiments it did not make a massive difference (was still nearly instant).
• Note that there is a restriction that taclets with varconds can not be translated at all. Apparently, \notFreeIn does not count as a varcond however. This is not a problem here, since all the term schema variables are bound variables after translation.
• There was a restriction that the taclets to translates were only allowed to have SchemaVariables of type TermSV and FormulaSV. We relaxed that for VariableSV now (it worked out of the box with the same code after removing the check), since that is needed to translate taclets containing binders.
• The taclets to be translated are selected by name prefixes. In ModularSMTLib2Translator there is a list of prefixes. However, it is probably incomplete at the moment.

This was done during the 3rd HacKeYthon. Thanks also to @BookWood7th!

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

[codecov]

Codecov Report

Attention: Patch coverage is 35.00000% with 26 lines in your changes missing coverage. Please review.

Project coverage is 38.33%. Comparing base (cdb55b9) to head (442abfe).
Report is 1 commits behind head on main.

Files with missing lines	Patch %	Lines
...ilkd/key/smt/newsmt2/ModularSMTLib2Translator.java	42.85%	11 Missing and 1 partial ⚠️
.../uka/ilkd/key/smt/newsmt2/SMTTacletTranslator.java	0.00%	9 Missing ⚠️
...a/de/uka/ilkd/key/smt/SMTSolverImplementation.java	0.00%	3 Missing ⚠️
...ava/de/uka/ilkd/key/smt/AbstractSMTTranslator.java	0.00%	1 Missing ⚠️
...ain/java/de/uka/ilkd/key/smt/SMTObjTranslator.java	0.00%	1 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff            @@
##               main    #3564   +/-   ##
=========================================
  Coverage     38.33%   38.33%           
- Complexity    17259    17264    +5     
=========================================
  Files          2111     2111           
  Lines        127632   127654   +22     
  Branches      21461    21462    +1     
=========================================
+ Hits          48926    48937   +11     
- Misses        72695    72705   +10     
- Partials       6011     6012    +1     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.