manually transferred and adapted from #3393 (due to changes in EqualityModuloProofIrrelevancy)

Author: WolframPfeifer

key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java

@@ -227,7 +227,9 @@ private TacletApp constructTacletApp(Node originalStep, Goal currGoal) {
         Taclet t = proof.getInitConfig().lookupActiveTaclet(new Name(tacletName));
         if (t == null) {
             // find the correct taclet
-            for (var partialApp : currGoal.indexOfTaclets().getPartialInstantiatedApps()) {
+            for (NoPosTacletApp partialApp : currGoal.indexOfTaclets()
+                    .getPartialInstantiatedApps()) {
+                System.out.println();
                 if (EqualityModuloProofIrrelevancy.equalsModProofIrrelevancy(partialApp,
                     originalTacletApp)) {
                     ourApp = partialApp;
@@ -239,7 +241,8 @@ private TacletApp constructTacletApp(Node originalStep, Goal currGoal) {
             }
             if (ourApp == null) {
                 throw new IllegalStateException(
-                    "proof replayer failed to find dynamically added taclet");
+                    "proof replayer failed to find dynamically added taclet at original node "
+                        + originalStep.serialNr());
             }
         } else {
             ourApp = NoPosTacletApp.createNoPosTacletApp(t);

key.core/src/main/java/de/uka/ilkd/key/rule/EqualityModuloProofIrrelevancy.java

@@ -14,12 +14,16 @@
 import de.uka.ilkd.key.logic.JavaBlock;
 import de.uka.ilkd.key.logic.op.*;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
+import de.uka.ilkd.key.rule.tacletbuilder.AntecSuccTacletGoalTemplate;
+import de.uka.ilkd.key.rule.tacletbuilder.RewriteTacletGoalTemplate;
 
 import org.key_project.logic.op.Operator;
 import org.key_project.logic.sort.Sort;
 import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.tacletbuilder.TacletGoalTemplate;
 import org.key_project.prover.sequent.PosInOccurrence;
+import org.key_project.prover.sequent.Semisequent;
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.prover.sequent.SequentFormula;
 import org.key_project.util.EqualsModProofIrrelevancyUtil;
@@ -286,9 +290,7 @@ public static int hashCodeModProofIrrelevancy(JavaBlock jb) {
      * @param that the second SequentFormula
      * @return true if both arguments are equal modulo proof irrelevancy
      */
-    public static boolean equalsModProofIrrelevancy(
-            SequentFormula _this,
-            SequentFormula that) {
+    public static boolean equalsModProofIrrelevancy(SequentFormula _this, SequentFormula that) {
         if (_this == that) {
             return true;
         }
@@ -306,11 +308,70 @@ public static boolean equalsModProofIrrelevancy(
      * @param sf the {@link SequentFormula} for which to compute the hash
      * @return the hash code modulo proof irrelevancy for the given argument
      */
-    public static int hashCodeModProofIrrelevancy(
-            SequentFormula sf) {
+    public static int hashCodeModProofIrrelevancy(SequentFormula sf) {
         return PROOF_IRRELEVANCY_PROPERTY.hashCodeModThisProperty((JTerm) sf.formula());
     }
 
+    // Sequent
+
+    /**
+     * test for equality modulo proof irrelevancy for the given arguments
+     *
+     * @param _this the first Sequent
+     * @param that the second Sequent
+     * @return true if both arguments are equal modulo proof irrelevancy
+     */
+    public static boolean equalsModProofIrrelevancy(Sequent _this, Sequent that) {
+        if (_this == that) {
+            return true;
+        } else if (_this == null || that == null) {
+            return false;
+        }
+        return equalsModProofIrrelevancy(_this.antecedent(), that.antecedent())
+                && equalsModProofIrrelevancy(_this.succedent(), that.succedent());
+    }
+
+    /**
+     * computes the hash code modulo proof irrelevancy for the given argument
+     *
+     * @param sequent the {@link Sequent} for which to compute the hash
+     * @return the hash code modulo proof irrelevancy for the given argument
+     */
+    public static int hashCodeModProofIrrelevancy(Sequent sequent) {
+        return Objects.hash(hashCodeModProofIrrelevancy(sequent.antecedent()),
+            hashCodeModProofIrrelevancy(sequent.succedent()));
+    }
+
+    // Semisequent
+
+    /**
+     * test for equality modulo proof irrelevancy for the given arguments
+     *
+     * @param _this the first Semisequent
+     * @param that the second Semisequent
+     * @return true if both arguments are equal modulo proof irrelevancy
+     */
+    public static boolean equalsModProofIrrelevancy(Semisequent _this, Semisequent that) {
+        if (_this == that) {
+            return true;
+        } else if (_this == null || that == null) {
+            return false;
+        }
+        return EqualsModProofIrrelevancyUtil.compareImmutableLists(_this.asList(), that.asList(),
+            EqualityModuloProofIrrelevancy::equalsModProofIrrelevancy);
+    }
+
+    /**
+     * computes the hash code modulo proof irrelevancy for the given argument
+     *
+     * @param semi the {@link Semisequent} for which to compute the hash
+     * @return the hash code modulo proof irrelevancy for the given argument
+     */
+    public static int hashCodeModProofIrrelevancy(Semisequent semi) {
+        return EqualsModProofIrrelevancyUtil.hashCodeIterable(semi.asList(),
+            EqualityModuloProofIrrelevancy::hashCodeModProofIrrelevancy);
+    }
+
     // RuleApp
 
     /**
@@ -412,7 +473,8 @@ public static int hashCodeModProofIrrelevancy(IBuiltInRuleApp ruleApp) {
      * @param that the second Taclet
      * @return true if both arguments are equal modulo proof irrelevancy
      */
-    public static boolean equalsModProofIrrelevancy(Taclet _this, Taclet that) {
+    public static boolean equalsModProofIrrelevancy(org.key_project.prover.rules.Taclet _this,
+            org.key_project.prover.rules.Taclet that) {
         if (that == _this)
             return true;
 
@@ -442,16 +504,17 @@ && equalsModProofIrrelevancy(if1.head(), if2.head())) {
             return false;
         }
 
-        return _this.goalTemplates().equals(that.goalTemplates());
+        return EqualsModProofIrrelevancyUtil.compareImmutableLists(_this.goalTemplates(),
+            that.goalTemplates(), EqualityModuloProofIrrelevancy::equalsModProofIrrelevancy);
     }
 
     /**
      * computes the hash code modulo proof irrelevancy for the given argument
      *
-     * @param taclet the {@link Taclet} for which to compute the hash
+     * @param taclet the Taclet for which to compute the hash
      * @return the hash code modulo proof irrelevancy for the given argument
      */
-    public static int hashCodeModProofIrrelevancy(Taclet taclet) {
+    public static int hashCodeModProofIrrelevancy(org.key_project.prover.rules.Taclet taclet) {
         Sequent sequentFormulas = taclet.assumesSequent();
         return hashCodeModProofIrrelevancy(sequentFormulas.getFormulaByNr(1));
     }
@@ -508,6 +571,102 @@ public static int hashCodeModProofIrrelevancy(TacletApp app) {
             app.rule());
     }
 
+    // TacletGoalTemplate
+
+    /**
+     * test for equality modulo proof irrelevancy for the given arguments
+     *
+     * @param _this the first TacletGoalTemplate
+     * @param that the second TacletGoalTemplate
+     * @return true if both arguments are equal modulo proof irrelevancy
+     */
+    public static boolean equalsModProofIrrelevancy(TacletGoalTemplate _this,
+            TacletGoalTemplate that) {
+        if (_this == that) {
+            return true;
+        } else if (_this == null || that == null) {
+            return false;
+        }
+        return equalsModProofIrrelevancy(_this.sequent(), that.sequent())
+                && EqualsModProofIrrelevancyUtil.compareImmutableLists(_this.rules(), that.rules(),
+                    EqualityModuloProofIrrelevancy::equalsModProofIrrelevancy);
+    }
+
+    /**
+     * computes the hash code modulo proof irrelevancy for the given argument
+     *
+     * @param t the {@link TacletGoalTemplate} for which to compute the hash
+     * @return the hash code modulo proof irrelevancy for the given argument
+     */
+    public static int hashCodeModProofIrrelevancy(TacletGoalTemplate t) {
+        return Objects.hash(hashCodeModProofIrrelevancy(t.sequent()),
+            EqualsModProofIrrelevancyUtil.hashCodeImmutableList(t.rules(),
+                EqualityModuloProofIrrelevancy::hashCodeModProofIrrelevancy));
+    }
+
+    // AntecSuccTacletGoalTemplate
+
+    /**
+     * test for equality modulo proof irrelevancy for the given arguments
+     *
+     * @param _this the first AntecSuccTacletGoalTemplate
+     * @param that the second AntecSuccTacletGoalTemplate
+     * @return true if both arguments are equal modulo proof irrelevancy
+     */
+    public static boolean equalsModProofIrrelevancy(AntecSuccTacletGoalTemplate _this,
+            AntecSuccTacletGoalTemplate that) {
+        if (_this == that) {
+            return true;
+        } else if (_this == null || that == null) {
+            return false;
+        }
+        return equalsModProofIrrelevancy((TacletGoalTemplate) _this, (TacletGoalTemplate) that)
+                && equalsModProofIrrelevancy(_this.replaceWith(), that.replaceWith());
+    }
+
+    /**
+     * computes the hash code modulo proof irrelevancy for the given argument
+     *
+     * @param t the {@link AntecSuccTacletGoalTemplate} for which to compute the hash
+     * @return the hash code modulo proof irrelevancy for the given argument
+     */
+    public static int hashCodeModProofIrrelevancy(AntecSuccTacletGoalTemplate t) {
+        return Objects.hash(hashCodeModProofIrrelevancy((TacletGoalTemplate) t),
+            hashCodeModProofIrrelevancy(t.replaceWith()));
+    }
+
+    // RewriteTacletGoalTemplate
+
+    /**
+     * test for equality modulo proof irrelevancy for the given arguments
+     *
+     * @param _this the first RewriteTacletGoalTemplate
+     * @param that the second RewriteTacletGoalTemplate
+     * @return true if both arguments are equal modulo proof irrelevancy
+     */
+    public static boolean equalsModProofIrrelevancy(RewriteTacletGoalTemplate _this,
+            RewriteTacletGoalTemplate that) {
+        if (_this == that) {
+            return true;
+        } else if (_this == null || that == null) {
+            return false;
+        }
+        return equalsModProofIrrelevancy((TacletGoalTemplate) _this, (TacletGoalTemplate) that)
+                && _this.replaceWith().equalsModProperty(that.replaceWith(),
+                    PROOF_IRRELEVANCY_PROPERTY);
+    }
+
+    /**
+     * computes the hash code modulo proof irrelevancy for the given argument
+     *
+     * @param t the {@link RewriteTacletGoalTemplate} for which to compute the hash
+     * @return the hash code modulo proof irrelevancy for the given argument
+     */
+    public static int hashCodeModProofIrrelevancy(RewriteTacletGoalTemplate t) {
+        return Objects.hash(hashCodeModProofIrrelevancy((TacletGoalTemplate) t),
+            t.replaceWith().hashCodeModProperty(PROOF_IRRELEVANCY_PROPERTY));
+    }
+
     // MatchConditions
     /**
      * test for equality modulo proof irrelevancy for the given arguments

key.util/src/main/java/org/key_project/util/EqualsModProofIrrelevancyUtil.java

@@ -76,15 +76,16 @@ public static <T> int hashCodeIterable(Iterable<T> iter, ToIntFunction<T> hasher
      * @param b second list
      * @return whether they are equal (same length, equal elements)
      */
-    public static <T> boolean compareImmutableLists(
-            ImmutableList<T> a, ImmutableList<T> b, BiPredicate<T, T> cmp) {
+    public static <T> boolean compareImmutableLists(ImmutableList<? extends T> a,
+            ImmutableList<? extends T> b,
+            BiPredicate<? super T, ? super T> cmp) {
         if (a == b || (a == null && b.size() == 0) || (b == null && a.size() == 0)) {
             return true;
         }
         if (a == null || b == null || (a.size() != b.size())) {
             return false;
         }
-        ImmutableList<T> remainderToCompare = a;
+        ImmutableList<? extends T> remainderToCompare = a;
         while (!remainderToCompare.isEmpty()) {
             final T obj1 = remainderToCompare.head();
             if (!cmp.test(obj1, b.head())) {