Formalize LocSet as Set of Locations

[Drodt]

Intended Change

Rely on the KeY formalization of parametric Set to express LocSet. We have:

\alias Loc = Pair<Object, Field>;
\alias LocSet = Set<Loc>;

Rules are adjusted accordingly.

Plan

• Fix tests.

Type of pull request

• Bug fix (non-breaking change which fixes an issue)
• Refactoring (behaviour should not change or only minimally change)
• New feature (non-breaking change which adds functionality)
• Breaking change (fix or feature that would cause existing functionality to change)
• There are changes to the (Java) code
• There are changes to the taclet rule base
• There are changes to the deployment/CI infrastructure (gradle, github, ...)
• Other:

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.

[unp1]

Thanks a lot! Great work. Only a few minor remarks/questions.

[unp1]

Please check if you want to keep the last two commits otherwise revert
They reeanble automatic proving of setExamples.key by moving the succedent version setEquaityToElementRight to generic sets (before only for locsets). That is not the general setEqualityToElement rule, which I think you did not want to be enabled automatically). If that includes also the more targeted right version, we can simply move it back or disable it for generic sets and add a duplicate for location sets.

The second commit restricts the elementOf decomposition rules to those cases where the decomposition is necessary. Such that the decomposition rules are only applied where it makes sense and otherwise using the normal one without decomposition.

Feel free to revert both commits or to only pick what you want.

[unp1]

Thanks a lot. I approved. But please make sure you are fine with my last commit (I wanted to have it done yesterday, but decided to get some sleepp at 5 a.m.) It makes the strategies a bit more useful (comm, assoc and distribute are now set strategy internal not relying on the quantifier heuristic) as well as additional simplification rules (+ their soundness proofs). Sorry that the PR adds now more lines then before, but that is misleading, still much more deleted and the vast majorit are the saved soundness proofs.

[mattulbrich]

Thanks, guys for your effort here! Sounds very reasonable and I am looking forward to having a decent set datatype in KeY!