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.

Additionally, this PR provides

• Many additional rules for sets and locsets (proven sound with KeY by @unp1)
• Additional strategies for sets and locsets, allowing easy use for other KeY instances in the future
• Proper LDT support for parametric sorts
• Improved and fixed matching for parametric functions with parametric sorts
• Pair is now parametric and has some additional rules
• SMT translation and Well-Definedness checks now consider set operations, not just LocSet

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 added new test case(s) for new functionality.
• I have tested the feature as follows: Tested using existing test suite
• I have checked that runtime performance has not deteriorated.

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!

[Drodt]

Why do we assume this? o2 appears only here. Is it an error or for performance?

[Drodt]

If it is not an error, I can undo my last commit (9eeedc6)

[unp1]

The problem was that I could not proof the taclet without the assumption (Z3 could), I did not find the proof argument that there are at least two elements of type java.lang.Object :-) The only one I could construct is 'null'. I am not sure if Z3s ability to close the proof came from translating taclets (in which case I could just not combine it) or some hard encoded information that the set of objects infinite.

I wanted to discuss it first, if everyone is fine to add an axiom stating that the java.lang.Object domain is infinite. I would like to state it as a general property (and not to hardcode it as a wellformed property). The wellformedness was also why I could not use instanceAllocation to get a second object.

But in the meantime I did not want to give up on the taclet and used the assumes as a workaround.

[unp1]

But you seem to have managed it 👍 So no objections from my side, the taclet is much more powerful that way.