Map with new equalities (#3486)

key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java

@@ -5,6 +5,7 @@
 
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.label.TermLabel;
+import de.uka.ilkd.key.logic.util.EqualityUtils;
 
 import org.key_project.util.collection.ImmutableArray;
 
@@ -82,9 +83,29 @@ public <V> boolean equalsModThisProperty(Term term1, Term term2, V... v) {
         return true;
     }
 
+    /**
+     * Computes the hash code of {@code term} while ignoring irrelevant labels.
+     *
+     * @param term the term to compute the hash code for
+     * @return the hash code
+     */
     @Override
     public int hashCodeModThisProperty(Term term) {
-        throw new UnsupportedOperationException(
-            "Hashing of terms modulo irrelevant term labels not yet implemented!");
+        int hashcode = 5;
+        hashcode = hashcode * 17 + term.op().hashCode();
+        hashcode = hashcode * 17 + EqualityUtils
+                .hashCodeModPropertyOfIterable(IRRELEVANT_TERM_LABELS_PROPERTY, term.subs());
+        hashcode = hashcode * 17 + term.boundVars().hashCode();
+        hashcode = hashcode * 17 + term.javaBlock().hashCode();
+
+        final ImmutableArray<TermLabel> labels = term.getLabels();
+        for (int i = 0, sz = labels.size(); i < sz; i++) {
+            final TermLabel currentLabel = labels.get(i);
+            if (currentLabel.isProofRelevant()) {
+                hashcode += 7 * currentLabel.hashCode();
+            }
+        }
+
+        return hashcode;
     }
 }

key.core/src/main/java/de/uka/ilkd/key/logic/equality/ProofIrrelevancyProperty.java

@@ -8,11 +8,13 @@
 
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.label.TermLabel;
+import de.uka.ilkd.key.logic.util.EqualityUtils;
 
 import org.key_project.util.EqualsModProofIrrelevancy;
 import org.key_project.util.EqualsModProofIrrelevancyUtil;
 import org.key_project.util.collection.ImmutableArray;
 
+
 /**
  * A property that can be used in
  * {@link EqualsModProperty#equalsModProperty(Object, Property, Object[])} for terms.
@@ -104,7 +106,8 @@ public <V> boolean equalsModThisProperty(Term term1, Term term2, V... v) {
      */
     @Override
     public int hashCodeModThisProperty(Term term) {
-        int hashcode = Objects.hash(term.op(), hashCodeIterable(term.subs()),
+        int hashcode = Objects.hash(term.op(),
+            EqualityUtils.hashCodeModPropertyOfIterable(PROOF_IRRELEVANCY_PROPERTY, term.subs()),
             EqualsModProofIrrelevancyUtil.hashCodeIterable(term.boundVars()), term.javaBlock());
 
         // part from LabeledTermImpl
@@ -117,29 +120,4 @@ public int hashCodeModThisProperty(Term term) {
         }
         return hashcode;
     }
-
-    // -------------------------- Utility methods --------------------------------- //
-
-    /**
-     * Compute the hashcode mod proof irrelevancy of an iterable of terms using the elements'
-     * {@link EqualsModProperty} implementation.
-     *
-     * @param iter iterable of terms
-     * @return combined hashcode
-     */
-    public static int hashCodeIterable(Iterable<? extends Term> iter) {
-        // adapted from Arrays.hashCode
-        if (iter == null) {
-            return 0;
-        }
-
-        int result = 1;
-
-        for (Term element : iter) {
-            result = 31 * result + (element == null ? 0
-                    : element.hashCodeModProperty(PROOF_IRRELEVANCY_PROPERTY));
-        }
-
-        return result;
-    }
 }

key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java

@@ -3,6 +3,8 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.logic.equality;
 
+import java.util.*;
+
 import de.uka.ilkd.key.java.JavaNonTerminalProgramElement;
 import de.uka.ilkd.key.java.NameAbstractionTable;
 import de.uka.ilkd.key.java.SourceElement;
@@ -100,13 +102,54 @@ public <V> boolean equalsModThisProperty(SourceElement se1, SourceElement se2, V
         return hasNext1 == hasNext2;
     }
 
+    // TODO: hashCodeModThisProperty currently does not take a NameAbstractionTable as an argument.
+    // This is because the current implementation of hashCodeModThisProperty is not parameterized
+    // with a vararg. Variables occurring in multiple formulas and JavaBlocks are considered in
+    // isolation as a newly created NameAbstractionTable that does not contain entries from previous
+    // JavaBlocks is used. This could possibly lead to more collisions but if this is a concern, the
+    // method can be changed to also take a generic vararg. That way, the NameAbstractionTable can
+    // be passed to the method and hash codes can take previous usage of variables into account.
     @Override
     public int hashCodeModThisProperty(SourceElement sourceElement) {
-        throw new UnsupportedOperationException(
-            "Hashing of SourceElements modulo renaming not yet implemented!");
+        /*
+         * Currently, the best approach seems to be to walk through the SourceElement with a
+         * SyntaxElementCursor and sum up hash codes.
+         */
+
+        NameAbstractionMap absMap = new NameAbstractionMap();
+
+        int hashCode = 1;
+        SyntaxElementCursor c = sourceElement.getCursor();
+        SyntaxElement next;
+
+        do {
+            // First node can never be null as cursor is initialized with 'this'
+            next = c.getCurrentNode();
+            // Handle special cases so that hashCodeModThisProperty follows equalsModThisProperty
+            if (next instanceof LabeledStatement ls) {
+                hashCode = 31 * hashCode + ls.getChildCount();
+                absMap.add(ls);
+            } else if (next instanceof VariableSpecification vs) {
+                hashCode = 31 * hashCode + vs.getChildCount();
+                hashCode =
+                    31 * hashCode + 17 * ((vs.getType() == null) ? 0 : vs.getType().hashCode())
+                            + vs.getDimensions();
+                absMap.add(vs);
+            } else if (next instanceof ProgramVariable || next instanceof ProgramElementName) {
+                hashCode = 31 * hashCode + absMap.getAbstractName((SourceElement) next);
+            } else if (next instanceof JavaNonTerminalProgramElement jnte) {
+                hashCode = 31 * hashCode + jnte.getChildCount();
+            } else {
+                // In the standard case, we just use the default hashCode implementation
+                hashCode = 31 * hashCode + next.hashCode();
+            }
+            // walk to the next nodes in the tree
+        } while (c.goToNext());
+
+        return hashCode;
     }
 
-    /* --------------------- Helper methods for special cases ---------------------- */
+    /*------------- Helper methods for special cases in equalsModThisProperty --------------*/
     /**
      * Handles the standard case of comparing two {@link SyntaxElement}s modulo renaming.
      *
@@ -252,5 +295,46 @@ private boolean handleProgramVariableOrElementName(SyntaxElement se1, SyntaxElem
     }
 
 
-    /* ------------------ End of helper methods for special cases ------------------ */
+    /* ---------- End of helper methods for special cases in equalsModThisProperty ---------- */
+
+    /**
+     * A helper class to map {@link SourceElement}s to an abstract name.
+     * <p>
+     * As names are abstracted from in this property, we need to give named elements abstract names
+     * for them to be used in the hash code. This approach is similar to
+     * {@link NameAbstractionTable}, where we collect elements with names in the order they are
+     * declared. Each element is associated with the number of previously added elements, which is
+     * then used as the abstract name.
+     */
+    private static class NameAbstractionMap {
+        /**
+         * The map that associates {@link SourceElement}s with their abstract names.
+         */
+        private final Map<SourceElement, Integer> map = new HashMap<>();
+
+        /**
+         * Adds a {@link SourceElement} to the map.
+         *
+         * @param element the {@link SourceElement} to be added
+         */
+        public void add(SourceElement element) {
+            map.put(element, map.size());
+        }
+
+        /**
+         * Returns the abstract name of a {@link SourceElement} or {@code -1} if the element is not
+         * in the map.
+         * <p>
+         * A common case for a look-up of an element that is not in the map, is a built-in datatype,
+         * e.g., the {@link ProgramElementName} {@code int}.
+         *
+         * @param element the {@link SourceElement} whose abstract name should be returned
+         * @return the abstract name of the {@link SourceElement} or {@code -1} if the element is
+         *         not in the map
+         */
+        public int getAbstractName(SourceElement element) {
+            final Integer result = map.get(element);
+            return result != null ? result : -1;
+        }
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java

@@ -56,10 +56,16 @@ public <V> boolean equalsModThisProperty(Term term1, Term term2, V... v) {
             ImmutableSLList.nil(), null);
     }
 
+    /**
+     * Computes the hash code of {@code term} modulo bound renaming.
+     *
+     * @param term the term to compute the hash code for
+     * @return the hash code
+     */
     @Override
     public int hashCodeModThisProperty(Term term) {
-        throw new UnsupportedOperationException(
-            "Hashing of terms modulo renaming not yet implemented!");
+        // Labels can be completely ignored
+        return hashTermHelper(term, ImmutableSLList.nil(), 1);
     }
 
     // equals modulo renaming logic
@@ -160,6 +166,15 @@ private boolean unifyHelp(Term t0, Term t1, ImmutableList<QuantifiableVariable>
         return descendRecursively(t0, t1, ownBoundVars, cmpBoundVars, nat);
     }
 
+    /**
+     * Handles the case where the first term is a quantifiable variable.
+     *
+     * @param t0 the first term
+     * @param t1 the second term
+     * @param ownBoundVars variables bound above the current position in {@code t0}
+     * @param cmpBoundVars variables bound above the current position in {@code t1}
+     * @return <code>true</code> iff the quantifiable variables are equal modulo renaming
+     */
     private boolean handleQuantifiableVariable(Term t0, Term t1,
             ImmutableList<QuantifiableVariable> ownBoundVars,
             ImmutableList<QuantifiableVariable> cmpBoundVars) {
@@ -174,6 +189,16 @@ && compareBoundVariables((QuantifiableVariable) t0.op(),
      */
     private static final NameAbstractionTable FAILED = new NameAbstractionTable();
 
+    /**
+     * Checks whether the given {@link JavaBlock}s are equal modulo renaming and returns the updated
+     * {@link NameAbstractionTable} or {@link #FAILED} if the {@link JavaBlock}s are not equal.
+     *
+     * @param jb0 the first {@link JavaBlock} to compare
+     * @param jb1 the second {@link JavaBlock} to compare
+     * @param nat the {@link NameAbstractionTable} used for the comparison
+     * @return the updated {@link NameAbstractionTable} if the {@link JavaBlock}s are equal modulo
+     *         renaming or {@link #FAILED} if they are not
+     */
     private static NameAbstractionTable handleJava(JavaBlock jb0, JavaBlock jb1,
             NameAbstractionTable nat) {
         if (!jb0.isEmpty() || !jb1.isEmpty()) {
@@ -211,6 +236,17 @@ public static boolean javaBlocksNotEqualModRenaming(JavaBlock jb1, JavaBlock jb2
         return true;
     }
 
+    /**
+     * Recursively descends into the subterms of the given terms and checks if they are equal modulo
+     * renaming.
+     *
+     * @param t0 the first term
+     * @param t1 the second term
+     * @param ownBoundVars variables bound above the current position in {@code t0}
+     * @param cmpBoundVars variables bound above the current position in {@code t1}
+     * @param nat the {@link NameAbstractionTable} used for the comparison
+     * @return <code>true</code> iff the subterms are equal modulo renaming
+     */
     private boolean descendRecursively(Term t0, Term t1,
             ImmutableList<QuantifiableVariable> ownBoundVars,
             ImmutableList<QuantifiableVariable> cmpBoundVars, NameAbstractionTable nat) {
@@ -244,6 +280,14 @@ private boolean descendRecursively(Term t0, Term t1,
         return true;
     }
 
+
+    /**
+     * Checks if the given {@link NameAbstractionTable} is not null. If it is null, a new
+     * {@link NameAbstractionTable} is created and returned.
+     *
+     * @param nat the {@link NameAbstractionTable} to check
+     * @return the given {@code nat} if it is not null, a new {@link NameAbstractionTable} otherwise
+     */
     private static NameAbstractionTable checkNat(NameAbstractionTable nat) {
         if (nat == null) {
             return new NameAbstractionTable();
@@ -252,4 +296,105 @@ private static NameAbstractionTable checkNat(NameAbstractionTable nat) {
     }
     // end of equals modulo renaming logic
 
+
+    /* -------- Helper methods for hashCodeModThisProperty --------- */
+
+    /**
+     * Helps to compute the hash code of a term modulo bound renaming.
+     * <p>
+     * This method takes care of the top level of the term and calls the recursive helper method
+     * {@link #recursiveHelper(Term, ImmutableList, int)} to take care of the subterms.
+     *
+     * @param term the term to compute the hash code for
+     * @param nameAbstractionList the list of bound variables that is used to abstract from the
+     *        variable names
+     * @param hashCode the accumulated hash code (should be 1 for the first call)
+     * @return the hash code
+     */
+    private int hashTermHelper(Term term, ImmutableList<QuantifiableVariable> nameAbstractionList,
+            int hashCode) {
+        // mirrors the implementation of unifyHelp that is responsible for equality modulo renaming
+        hashCode = 17 * hashCode + term.sort().hashCode();
+        hashCode = 17 * hashCode + term.arity();
+
+        final Operator op = term.op();
+        if (op instanceof QuantifiableVariable qv) {
+            hashCode = 17 * hashCode + hashQuantifiableVariable(qv, nameAbstractionList);
+        } else if (op instanceof Modality mod) {
+            hashCode = 17 * hashCode + mod.kind().hashCode();
+            hashCode = 17 * hashCode + hashJavaBlock(mod);
+        } else if (op instanceof ProgramVariable pv) {
+            hashCode = 17 * hashCode + pv.hashCodeModProperty(RENAMING_SOURCE_ELEMENT_PROPERTY);
+        }
+
+        return recursiveHelper(term, nameAbstractionList, hashCode);
+    }
+
+    /**
+     * Computes the hash code of a quantifiable variable modulo bound renaming.
+     * <p>
+     * If the variable is bound, the hash code is computed based on the index of the variable in the
+     * list of bound variables.
+     * If the variable is not bound, the hash code is computed based on the variable itself.
+     *
+     * @param qv the {@link QuantifiableVariable} to compute the hash code for
+     * @param nameAbstractionList the list of bound variables that is used to abstract from the
+     *        variable names
+     * @return the hash code
+     */
+    private int hashQuantifiableVariable(QuantifiableVariable qv,
+            ImmutableList<QuantifiableVariable> nameAbstractionList) {
+        final int index = indexOf(qv, nameAbstractionList);
+        // if the variable is bound, we just need to consider the place it is bound at and abstract
+        // from the name
+        return index == -1 ? qv.hashCode() : index;
+    }
+
+    /**
+     * Computes the hash code of a Java block modulo bound renaming.
+     * <p>
+     * The hash code is computed based on the hash code of the program element of the Java block.
+     *
+     * @param mod the {@link Modality} to compute the hash code for
+     * @return the hash code
+     */
+    private int hashJavaBlock(Modality mod) {
+        final JavaBlock jb = mod.program();
+        if (!jb.isEmpty()) {
+            final JavaProgramElement jpe = jb.program();
+            return jpe != null ? jpe.hashCodeModProperty(RENAMING_SOURCE_ELEMENT_PROPERTY) : 0;
+        }
+        // if the Java block is empty, we do not add anything to the hash code
+        return 0;
+    }
+
+    /**
+     * Recursively computes the hash code of a term modulo bound renaming.
+     * <p>
+     * This method iterates over the subterms of the given term and calls
+     * {@link #hashTermHelper(Term, ImmutableList, int)} for each subterm.
+     *
+     * @param term the term to compute the hash code for
+     * @param nameAbstractionList the list of bound variables that is used to abstract from the
+     *        variable names
+     * @param hashCode the accumulated hash code
+     * @return the hash code
+     */
+    private int recursiveHelper(Term term, ImmutableList<QuantifiableVariable> nameAbstractionList,
+            int hashCode) {
+        for (int i = 0; i < term.arity(); i++) {
+            ImmutableList<QuantifiableVariable> subBoundVars = nameAbstractionList;
+
+            for (int j = 0; j < term.varsBoundHere(i).size(); j++) {
+                final QuantifiableVariable qVar = term.varsBoundHere(i).get(j);
+                hashCode = 17 * hashCode + qVar.sort().hashCode();
+                subBoundVars = subBoundVars.prepend(qVar);
+            }
+
+            hashCode = hashTermHelper(term.sub(i), subBoundVars, hashCode);
+        }
+        return hashCode;
+    }
+
+    /* ----- End of helper methods for hashCodeModThisProperty ----- */
 }