Combine equalsMod... methods

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java

@@ -75,6 +75,9 @@
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
+import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY;
+import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY;
+
 /**
  * Provides utility methods for symbolic execution with KeY.
  *
@@ -391,7 +394,7 @@ else if (term.op() == Junctor.NOT) {
      * @return true if the term represents the one
      */
     private static boolean isOne(Term subOne, IntegerLDT integerLDT) {
-        return subOne.equalsModIrrelevantTermLabels(integerLDT.one());
+        return subOne.equalsModProperty(integerLDT.one(), IRRELEVANT_TERM_LABELS_PROPERTY);
     }
 
     /**
@@ -1982,13 +1985,16 @@ private static void collectSpecifcationCasesPreconditions(Term normalExcDefiniti
             List<Term> exceptinalConditions) throws ProofInputException {
         if (term.op() == Junctor.AND) {
             Term lastChild = term.sub(term.arity() - 1);
-            if (lastChild.equalsModIrrelevantTermLabels(normalExcDefinition)
-                    || lastChild.equalsModIrrelevantTermLabels(exceptionalExcDefinition)) {
+            if (lastChild.equalsModProperty(normalExcDefinition, IRRELEVANT_TERM_LABELS_PROPERTY)
+                    || lastChild.equalsModProperty(exceptionalExcDefinition,
+                        IRRELEVANT_TERM_LABELS_PROPERTY)) {
                 // Nothing to do, condition is just true
             } else {
                 Term firstChild = term.sub(0);
-                if (firstChild.equalsModIrrelevantTermLabels(normalExcDefinition)
-                        || firstChild.equalsModIrrelevantTermLabels(exceptionalExcDefinition)) {
+                if (firstChild
+                        .equalsModProperty(normalExcDefinition, IRRELEVANT_TERM_LABELS_PROPERTY)
+                        || firstChild.equalsModProperty(exceptionalExcDefinition,
+                            IRRELEVANT_TERM_LABELS_PROPERTY)) {
                     // Nothing to do, condition is just true
                 } else {
                     for (int i = 0; i < term.arity(); i++) {
@@ -2000,47 +2006,56 @@ private static void collectSpecifcationCasesPreconditions(Term normalExcDefiniti
             }
         } else if (term.op() == Junctor.IMP) {
             Term leftTerm = term.sub(0);
-            if (leftTerm.equalsModIrrelevantTermLabels(normalExcDefinition)
-                    || leftTerm.equalsModIrrelevantTermLabels(exceptionalExcDefinition)) {
+            if (leftTerm.equalsModProperty(normalExcDefinition, IRRELEVANT_TERM_LABELS_PROPERTY)
+                    || leftTerm.equalsModProperty(exceptionalExcDefinition,
+                        IRRELEVANT_TERM_LABELS_PROPERTY)) {
                 // Nothing to do, condition is just true
             } else {
                 Term rightTerm = term.sub(1);
                 // Deal with heavy weight specification cases
                 if (rightTerm.op() == Junctor.AND && rightTerm.sub(0).op() == Junctor.IMP
                         && rightTerm.sub(0).sub(0)
-                                .equalsModIrrelevantTermLabels(normalExcDefinition)) {
+                                .equalsModProperty(normalExcDefinition,
+                                    IRRELEVANT_TERM_LABELS_PROPERTY)) {
                     normalConditions.add(leftTerm);
                 } else if (rightTerm.op() == Junctor.AND && rightTerm.sub(1).op() == Junctor.IMP
                         && rightTerm.sub(1).sub(0)
-                                .equalsModIrrelevantTermLabels(exceptionalExcDefinition)) {
+                                .equalsModProperty(exceptionalExcDefinition,
+                                    IRRELEVANT_TERM_LABELS_PROPERTY)) {
                     exceptinalConditions.add(leftTerm);
                 }
                 // Deal with light weight specification cases
                 else if (rightTerm.op() == Junctor.IMP
-                        && rightTerm.sub(0).equalsModIrrelevantTermLabels(normalExcDefinition)) {
+                        && rightTerm.sub(0).equalsModProperty(normalExcDefinition,
+                            IRRELEVANT_TERM_LABELS_PROPERTY)) {
                     normalConditions.add(leftTerm);
                 } else if (rightTerm.op() == Junctor.IMP && rightTerm.sub(0)
-                        .equalsModIrrelevantTermLabels(exceptionalExcDefinition)) {
+                        .equalsModProperty(exceptionalExcDefinition,
+                            IRRELEVANT_TERM_LABELS_PROPERTY)) {
                     exceptinalConditions.add(leftTerm);
                 } else {
                     Term excCondition = rightTerm;
                     // Check if right child is exception definition
                     if (excCondition.op() == Junctor.AND) {
                         excCondition = excCondition.sub(excCondition.arity() - 1);
                     }
-                    if (excCondition.equalsModIrrelevantTermLabels(normalExcDefinition)) {
+                    if (excCondition.equalsModProperty(normalExcDefinition,
+                        IRRELEVANT_TERM_LABELS_PROPERTY)) {
                         normalConditions.add(leftTerm);
                     } else if (excCondition
-                            .equalsModIrrelevantTermLabels(exceptionalExcDefinition)) {
+                            .equalsModProperty(exceptionalExcDefinition,
+                                IRRELEVANT_TERM_LABELS_PROPERTY)) {
                         exceptinalConditions.add(leftTerm);
                     } else {
                         // Check if left child is exception definition
                         if (rightTerm.op() == Junctor.AND) {
                             excCondition = rightTerm.sub(0);
-                            if (excCondition.equalsModIrrelevantTermLabels(normalExcDefinition)) {
+                            if (excCondition.equalsModProperty(normalExcDefinition,
+                                IRRELEVANT_TERM_LABELS_PROPERTY)) {
                                 normalConditions.add(leftTerm);
                             } else if (excCondition
-                                    .equalsModIrrelevantTermLabels(exceptionalExcDefinition)) {
+                                    .equalsModProperty(exceptionalExcDefinition,
+                                        IRRELEVANT_TERM_LABELS_PROPERTY)) {
                                 exceptinalConditions.add(leftTerm);
                             } else {
                                 throw new ProofInputException("Exeptional condition expected, "
@@ -2671,7 +2686,7 @@ private static boolean checkReplaceTerm(Term toCheck, PosInOccurrence posInOccur
             Term replaceTerm) {
         Term termAtPio = followPosInOccurrence(posInOccurrence, toCheck);
         if (termAtPio != null) {
-            return termAtPio.equalsModRenaming(replaceTerm);
+            return termAtPio.equalsModProperty(replaceTerm, RENAMING_PROPERTY);
         } else {
             return false;
         }
@@ -3417,11 +3432,13 @@ private static List<Term> findSkolemReplacements(Sequent sequent, Term skolemCon
             if (term != skolemEquality) {
                 int skolemCheck = checkSkolemEquality(term);
                 if (skolemCheck == -1) {
-                    if (term.sub(0).equalsModIrrelevantTermLabels(skolemConstant)) {
+                    if (term.sub(0).equalsModProperty(skolemConstant,
+                        IRRELEVANT_TERM_LABELS_PROPERTY)) {
                         result.add(term.sub(1));
                     }
                 } else if (skolemCheck == 1) {
-                    if (term.sub(1).equalsModIrrelevantTermLabels(skolemConstant)) {
+                    if (term.sub(1).equalsModProperty(skolemConstant,
+                        IRRELEVANT_TERM_LABELS_PROPERTY)) {
                         result.add(term.sub(0));
                     }
                 }
@@ -3511,7 +3528,8 @@ public static Term computePathCondition(Node parentNode, Node childNode, boolean
                 }
                 childNode = parent;
             }
-            if (services.getTermBuilder().ff().equalsModIrrelevantTermLabels(pathCondition)) {
+            if (services.getTermBuilder().ff().equalsModProperty(pathCondition,
+                IRRELEVANT_TERM_LABELS_PROPERTY)) {
                 throw new ProofInputException(
                     "Path condition computation failed because the result is false.");
             }

key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryBlockComputationMacro.java

@@ -24,6 +24,8 @@
 
 import org.key_project.util.collection.ImmutableList;
 
+import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY;
+
 
 /**
  *
@@ -78,7 +80,7 @@ public boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrenc
         final Term selfComposedExec =
             f.create(InfFlowPOSnippetFactory.Snippet.SELFCOMPOSED_BLOCK_WITH_PRE_RELATION);
 
-        return posInOcc.subTerm().equalsModRenaming(selfComposedExec);
+        return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_PROPERTY);
     }
 
     @Override

key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryLoopComputationMacro.java

@@ -25,6 +25,8 @@
 
 import org.key_project.util.collection.ImmutableList;
 
+import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY;
+
 public class StartAuxiliaryLoopComputationMacro extends AbstractProofMacro
         implements StartSideProofMacro {
 
@@ -75,7 +77,7 @@ public boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrenc
         final Term selfComposedExec =
             f.create(InfFlowPOSnippetFactory.Snippet.SELFCOMPOSED_LOOP_WITH_INV_RELATION);
 
-        return posInOcc.subTerm().equalsModRenaming(selfComposedExec);
+        return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_PROPERTY);
     }
 
     @Override

key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryMethodComputationMacro.java

@@ -22,6 +22,8 @@
 
 import org.key_project.util.collection.ImmutableList;
 
+import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY;
+
 /**
  *
  * @author christoph
@@ -67,7 +69,7 @@ public boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrenc
         final Term selfComposedExec =
             f.create(InfFlowPOSnippetFactory.Snippet.SELFCOMPOSED_EXECUTION_WITH_PRE_RELATION);
 
-        return posInOcc.subTerm().equalsModRenaming(selfComposedExec);
+        return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_PROPERTY);
     }
 
     @Override

key.core/src/main/java/de/uka/ilkd/key/logic/BoundVariableTools.java

@@ -13,6 +13,8 @@
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableSet;
 
+import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY;
+
 
 /**
  * Some generally useful tools for dealing with arrays of bound variables
@@ -206,7 +208,7 @@ public boolean equalsModRenaming(ImmutableArray<QuantifiableVariable> vars0, Ter
             return false;
         }
         if (vars0.size() == 0) {
-            return term0.equalsModRenaming(term1);
+            return term0.equalsModProperty(term1, RENAMING_PROPERTY);
         }
 
         final ImmutableArray<QuantifiableVariable> unifiedVars = unifyVariableArrays(vars0, vars1,
@@ -215,7 +217,7 @@ public boolean equalsModRenaming(ImmutableArray<QuantifiableVariable> vars0, Ter
         final Term renamedTerm0 = renameVariables(term0, vars0, unifiedVars, services);
         final Term renamedTerm1 = renameVariables(term1, vars1, unifiedVars, services);
 
-        return renamedTerm0.equalsModRenaming(renamedTerm1);
+        return renamedTerm0.equalsModProperty(renamedTerm1, RENAMING_PROPERTY);
     }
 
     /**

key.core/src/main/java/de/uka/ilkd/key/logic/JavaBlock.java

@@ -4,7 +4,6 @@
 package de.uka.ilkd.key.logic;
 
 import de.uka.ilkd.key.java.JavaProgramElement;
-import de.uka.ilkd.key.java.NameAbstractionTable;
 import de.uka.ilkd.key.java.StatementBlock;
 import de.uka.ilkd.key.pp.PrettyPrinter;
 
@@ -91,31 +90,6 @@ public boolean equals(Object o) {
         }
     }
 
-    /**
-     * returns true if the given ProgramElement is equal to the one of the JavaBlock modulo renaming
-     * (see comment in SourceElement)
-     */
-    public boolean equalsModRenaming(Object o, NameAbstractionTable nat) {
-        if (!(o instanceof JavaBlock)) {
-            return false;
-        }
-        return equalsModRenaming(((JavaBlock) o).program(), nat);
-    }
-
-
-    /**
-     * returns true if the given ProgramElement is equal to the one of the JavaBlock modulo renaming
-     * (see comment in SourceElement)
-     */
-    private boolean equalsModRenaming(JavaProgramElement pe, NameAbstractionTable nat) {
-        if (pe == null && program() == null) {
-            return true;
-        } else if (pe != null && program() != null) {
-            return program().equalsModRenaming(pe, nat);
-        }
-        return false;
-    }
-
     /**
      * returns the java program
      *

key.core/src/main/java/de/uka/ilkd/key/logic/LabeledTermImpl.java

@@ -6,6 +6,10 @@
 import java.util.Objects;
 import java.util.stream.Collectors;
 
+import de.uka.ilkd.key.logic.equality.ProofIrrelevancyProperty;
+import de.uka.ilkd.key.logic.equality.RenamingProperty;
+import de.uka.ilkd.key.logic.equality.TermEqualsModProperty;
+import de.uka.ilkd.key.logic.equality.TermProperty;
 import de.uka.ilkd.key.logic.label.TermLabel;
 import de.uka.ilkd.key.logic.op.Operator;
 import de.uka.ilkd.key.logic.op.QuantifiableVariable;
@@ -16,16 +20,25 @@
 import org.key_project.util.java.CollectionUtil;
 
 /**
+ * <p>
  * The labeled term class is used for terms that have a label attached.
+ * </p>
+ *
+ * Two labeled terms are equal if they have equal term structure and equal annotations. In contrast,
+ * the method {@link TermEqualsModProperty#equalsModProperty(Object, TermProperty)} can be used to
+ * compare terms while ignoring certain given properties. E.g. by using
+ * {@link RenamingProperty#RENAMING_PROPERTY}, just the term structures modulo renaming are compared
+ * whilst ignoring annotations.
+ * <p>
+ * Prior implementations of {@link EqualsModProofIrrelevancy} are now in
+ * {@link ProofIrrelevancyProperty}.
+ * </p>
  *
- * Two labeled terms are equal if they have equal term structure and equal annotations. In contrast
- * the method {@link Term#equalsModRenaming(Term)} does not care about annotations and will just
- * compare the term structure alone modula renaming.
  *
  * @see Term
  * @see TermImpl
  */
-class LabeledTermImpl extends TermImpl implements EqualsModProofIrrelevancy {
+class LabeledTermImpl extends TermImpl {
 
     /**
      * @see #getLabels()
@@ -38,7 +51,7 @@
      * @param op the top level operator
      * @param subs the Term that are the subterms of this term
      * @param boundVars logic variables bound by the operator
-     * @param labels the terms labels (must not be null or empty)
+     * @param labels the term's labels (must not be null or empty)
      * @param origin a String with origin information
      */
     public LabeledTermImpl(Operator op, ImmutableArray<Term> subs,
@@ -143,43 +156,6 @@
         return hash;
     }
 
-    @Override
-    public boolean equalsModProofIrrelevancy(Object o) {
-        if (!super.equalsModProofIrrelevancy(o)) {
-            return false;
-        }
-
-        if (o instanceof LabeledTermImpl cmp) {
-            if (labels.size() == cmp.labels.size()) {
-                for (int i = 0, sz = labels.size(); i < sz; i++) {
-                    // skip irrelevant (origin) labels that differ for no real reason
-                    if (!labels.get(i).isProofRelevant()) {
-                        continue;
-                    }
-                    // this is not optimal, but as long as number of labels limited ok
-                    if (!cmp.labels.contains(labels.get(i))) {
-                        return false;
-                    }
-                }
-                return true;
-            }
-            return false;
-        } else {
-            return o.getClass() == TermImpl.class;
-        }
-    }
-
-    @Override
-    public int hashCodeModProofIrrelevancy() {
-        int hash = super.hashCodeModProofIrrelevancy();
-        for (int i = 0, sz = labels.size(); i < sz; i++) {
-            if (labels.get(i).isProofRelevant()) {
-                hash += 7 * labels.get(i).hashCode();
-            }
-        }
-        return hash;
-    }
-
     @Override
     public String toString() {
         StringBuilder result = new StringBuilder(super.toString());

key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java

@@ -9,6 +9,8 @@
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 
+import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY;
+
 
 /**
  * This class represents the succedent or antecendent part of a sequent. It is more or less a list
@@ -184,7 +186,8 @@ private SemisequentChangeInfo insertAndRemoveRedundancyHelper(int idx,
             searchList = searchList.tail();
 
             if (sequentFormula != null
-                    && cf.formula().equalsModRenaming(sequentFormula.formula())) {
+                    && cf.formula().equalsModProperty(sequentFormula.formula(),
+                        RENAMING_PROPERTY)) {
                 semiCI.rejectedFormula(sequentFormula);
                 return semiCI; // semisequent already contains formula