Closed tobias-rnh closed 5 months ago
While testing the behaviour of the old equalsModProofIrrelevancy for terms to move it to a TermProperty, I discovered the following behaviour: If you take an unlabeled term and compare it to the same term with a proof-irrelevant label attached, equalsModProofIrrelevancy returns true, no matter on what term it is called. If however you take two labeled terms, that only have proof-irrelevant labels attached, but differ in the amount of those, equalsModProofIrrelevancy returns false, no matter on what term it is called.
I could imagine that this behaviour is not intended. But just to make sure that I do not break the intended behaviour, I wanted to ask @FliegendeWurst and @WolframPfeifer how equalsModProofIrrelevancy should act in these situations.
If this behaviour is indeed not intended, I would simply change it in my implementation. Otherwise, I will of course keep it this way. Thank you for your time!
If however you take two labeled terms, that only have proof-irrelevant labels attached, but differ in the amount of those, equalsModProofIrrelevancy returns false, no matter on what term it is called.
That is indeed a bug. It should return true.
Attention: Patch coverage is 59.19118%
with 111 lines
in your changes are missing coverage. Please review.
Project coverage is 37.88%. Comparing base (
8bf8306
) to head (438a94d
).
:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.
I have again checked that all calls of equalsModProperty
use the right property to match the calls to prior equalsMod...
methods.
Only in TestApplyUpdateOnRigidCondition
, equalsModProofIrrelevancy
was replaced by equalsModProperty
with RENAMING_PROPERTY
.
This is okay and wanted as it actually should have been equalsModRenaming
in the first place.
Apart from that, everything is as it should be and tests are passing.
Intended Change
There were four different functions concerned with equality of terms other than the usual
equals
, namelyequalsModRenaming
,equalsModTermLabels
,equalsModIrrelevantTermLabels
andequalsModProofIrrelevancy
. Now, there is a new InterfaceEqualsModProperty
, which is extended byTerm
, with a single methodequalsModProperty
that takes two parameters: the object to be compared and one of the new typeTermProperty
, that implements the desired behavior of what to be ignored during the equality check. The changes can be found in a new package called equality in the logic package of key.core. TheTermProperty
s are designed as a singleton and can be accessed through their respective static constants, e.g.IRRELEVANT_TERM_LABELS_PROPERTY
inIrrelevantTermLabelsProperty
.Term
now no longer implements the InterfaceEqualsModProofIrrelevancy
. Therefore it might be a problem if you wanted to use terms in anEquivalenceDirectedGraph
.Type of pull request
Ensuring quality
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.