Modularity for Proof Strategies

[Drodt]

Intended Change

Part of the modularization effort.

Splits the JavaCardDLStrategy into multiple different strategies, responsible for smaller sets of rule sets.

• The FOLStrategy handles basic logic parts, such as propositional rules and quantifier instantiation
• The JFOLStrategy is more tuned to JFOL, including heap and integer logic (for quantification)
• The IntegerStrategy handles integers
• The SymExStrategy handles symbolic execution
• The StringFactory handles strings
• JavaCardDLStrategy handles "the rest"

All are composed by the ModularJavaDLStrategy.

Plan

• Documentation
• Performance tests
• Clean up

Type of pull request

• Refactoring (behaviour should not change or only minimally change)
• New feature (non-breaking change which adds functionality)
• There are changes to the (Java) code
• There are changes to the taclet rule base

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.
• For new Gradle modules: I added the Gradle module to the test matrix in
  .github/workflows/tests.yml

Additional information and contact(s)

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