From 8ceeef752fbc906bf8dc182e72a30fa70cbd61c0 Mon Sep 17 00:00:00 2001 From: Tobias Date: Fri, 26 Jul 2024 16:20:58 +0200 Subject: [PATCH] adapt equality modulo renaming to rusty_while --- .../rusty/ast/stmt/LetStatement.java | 8 + .../rusty/logic/FormulaChangeInfo.java | 21 + .../rusty/logic/NameAbstractionTable.java | 60 +++ .../key_project/rusty/logic/Semisequent.java | 85 +++- .../logic/equality/EqualsModProperty.java | 13 + .../rusty/logic/equality/Property.java | 24 ++ .../RenamingProgramElementProperty.java | 284 +++++++++++++ .../logic/equality/RenamingTermProperty.java | 383 ++++++++++++++++++ 8 files changed, 877 insertions(+), 1 deletion(-) create mode 100644 keyext.rusty_while/src/main/java/org/key_project/rusty/logic/FormulaChangeInfo.java create mode 100644 keyext.rusty_while/src/main/java/org/key_project/rusty/logic/NameAbstractionTable.java create mode 100644 keyext.rusty_while/src/main/java/org/key_project/rusty/logic/equality/EqualsModProperty.java create mode 100644 keyext.rusty_while/src/main/java/org/key_project/rusty/logic/equality/Property.java create mode 100644 keyext.rusty_while/src/main/java/org/key_project/rusty/logic/equality/RenamingProgramElementProperty.java create mode 100644 keyext.rusty_while/src/main/java/org/key_project/rusty/logic/equality/RenamingTermProperty.java diff --git a/keyext.rusty_while/src/main/java/org/key_project/rusty/ast/stmt/LetStatement.java b/keyext.rusty_while/src/main/java/org/key_project/rusty/ast/stmt/LetStatement.java index e6f3320d5fe..f53c77a1e24 100644 --- a/keyext.rusty_while/src/main/java/org/key_project/rusty/ast/stmt/LetStatement.java +++ b/keyext.rusty_while/src/main/java/org/key_project/rusty/ast/stmt/LetStatement.java @@ -36,6 +36,14 @@ public int getChildCount() { return 3; } + public Type getType() { + return type; + } + + public Pattern getPattern() { + return pat; + } + @Override public String toString() { return "let " + pat + ": " + type + " = " + init; diff --git a/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/FormulaChangeInfo.java b/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/FormulaChangeInfo.java new file mode 100644 index 00000000000..687976fe866 --- /dev/null +++ b/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/FormulaChangeInfo.java @@ -0,0 +1,21 @@ +package org.key_project.rusty.logic; + +public record FormulaChangeInfo(PosInOccurrence positionOfModification, SequentFormula newFormula) { + + public SequentFormula getOriginalFormula() { + return positionOfModification().sequentFormula(); + } + + /** + * @return position within the original formula + */ + @Override + public PosInOccurrence positionOfModification() { + return positionOfModification; + } + + public String toString() { + return "Replaced " + positionOfModification + " with " + newFormula; + } + +} diff --git a/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/NameAbstractionTable.java b/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/NameAbstractionTable.java new file mode 100644 index 00000000000..0143240ce86 --- /dev/null +++ b/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/NameAbstractionTable.java @@ -0,0 +1,60 @@ +package org.key_project.rusty.logic; + +import org.key_project.rusty.ast.RustyProgramElement; + +import java.util.Iterator; +import java.util.LinkedList; +import java.util.List; + +public class NameAbstractionTable { + + /** + * The order in which symbols are declared in the two terms or programs that are compared. The + * latest declaration of a symbol will be the first matching entry in the list + */ + private List declarations0 = null, declarations1 = null; + + /** + * adds the given two elements to the table + * + * @param pe1 RustyProgramElement to be added + * @param pe2 RustyProgramElement to be added + */ + public void add(RustyProgramElement pe1, RustyProgramElement pe2) { + if (declarations0 == null) { + declarations0 = new LinkedList<>(); + declarations1 = new LinkedList<>(); + } + + declarations0.add(0, pe1); + declarations1.add(0, pe2); + } + + /** + * tests if the given elements have been assigned to the same abstract name. + * + * @param pe0 RustyProgramElement + * @param pe1 RustyProgramElement + * @returns true if the pe1 and pe2 have been assigned to the same name + */ + public boolean sameAbstractName(RustyProgramElement pe0, RustyProgramElement pe1) { + if (declarations0 != null) { + final Iterator it0 = declarations0.iterator(); + final Iterator it1 = declarations1.iterator(); + + while (it0.hasNext()) { + // both lists are assumed to hold the same number of elements + final Object o0 = it0.next(); + final Object o1 = it1.next(); + + if (pe0.equals(o0)) { + return pe1.equals(o1); + } else if (pe1.equals(o1)) { + return false; + } + } + } + + return pe0.equals(pe1); + } +} diff --git a/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/Semisequent.java b/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/Semisequent.java index 13396044c91..12950b69d85 100644 --- a/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/Semisequent.java +++ b/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/Semisequent.java @@ -10,6 +10,8 @@ import org.jspecify.annotations.NonNull; +import static org.key_project.rusty.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY; + public class Semisequent implements Iterable { /** the empty semisequent (using singleton pattern) */ public static final Semisequent EMPTY_SEMISEQUENT = new Empty(); @@ -21,6 +23,18 @@ private Semisequent() { seqList = ImmutableSLList.nil(); } + /** + * Create a new Semisequent from an ordered collection of formulas. + * The provided list must be redundancy free, i.e., the created sequent must be exactly + * the same as when creating the sequent by subsequently inserting all formulas + * + * @param seqList list of sequent formulas + */ + public Semisequent(ImmutableList seqList) { + assert !seqList.isEmpty(); + this.seqList = seqList; + } + /** * creates a new Semisequent with the Semisequent elements in seqList */ @@ -34,7 +48,7 @@ public Semisequent(SequentFormula seqFormula) { * returning same semisequent if inserting would create redundancies * * @param idx int encoding the place the element has to be put - * @param sequentFormula {@link de.uka.ilkd.key.logic.SequentFormula} to be inserted + * @param sequentFormula {@link SequentFormula} to be inserted * @return a semi sequent change information object with the new semisequent and information * which formulas have been added or removed */ @@ -63,6 +77,75 @@ public boolean isEmpty() { return seqList.isEmpty(); } + /** + * inserts new SequentFormula at index idx and removes duplicates, perform simplifications etc. + * + * @param fci null if the formula to be added is new, otherwise an object telling which formula + * is replaced with the new formula sequentFormula, and what are the + * differences between the two formulas + * @return a semi sequent change information object with the new semisequent and information + * which formulas have been added or removed + */ + private SemisequentChangeInfo insertAndRemoveRedundancyHelper(int idx, + SequentFormula sequentFormula, SemisequentChangeInfo semiCI, FormulaChangeInfo fci) { + + // Search for equivalent formulas and weakest constraint + ImmutableList searchList = semiCI.getFormulaList(); + final SequentFormula[] newSeqList = new SequentFormula[searchList.size()]; + SequentFormula cf; + int pos = -1; + + while (!searchList.isEmpty()) { + ++pos; + cf = searchList.head(); + searchList = searchList.tail(); + + if (sequentFormula != null + && RENAMING_TERM_PROPERTY.equalsModThisProperty(cf.formula(), sequentFormula.formula())) { + semiCI.rejectedFormula(sequentFormula); + return semiCI; // semisequent already contains formula + + } + newSeqList[pos] = cf; + } + + + // compose resulting formula list + if (fci == null) { + semiCI.addedFormula(idx, sequentFormula); + } else { + semiCI.modifiedFormula(idx, fci); + } + + final ImmutableList orig = semiCI.getFormulaList(); + pos = Math.min(idx, orig.size()); + + searchList = semiCI.getFormulaList().take(pos).prepend(sequentFormula); + + while (pos > 0) { + --pos; + searchList = searchList.prepend(newSeqList[pos]); + } + + // add new formula list to result object + semiCI.setFormulaList(searchList); + + return semiCI; + } + + /** + * . inserts new SequentFormula at index {@code idx} and removes duplicates, perform + * simplifications etc. + * + * @param sequentFormula the SequentFormula to be inserted at position idx + * @param idx an int that means insert sequentFormula at the idx-th position in the semisequent + * @return new Semisequent with sequentFormula at index idx and removed redundancies + */ + private SemisequentChangeInfo removeRedundance(int idx, SequentFormula sequentFormula) { + return insertAndRemoveRedundancyHelper(idx, sequentFormula, + new SemisequentChangeInfo(seqList), null); + } + /** * gets the element at a specific index * diff --git a/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/equality/EqualsModProperty.java b/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/equality/EqualsModProperty.java new file mode 100644 index 00000000000..ff78250cbaa --- /dev/null +++ b/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/equality/EqualsModProperty.java @@ -0,0 +1,13 @@ +package org.key_project.rusty.logic.equality; + +public interface EqualsModProperty { + boolean equalsModProperty(Object o, Property property, V... v); + + /** + * Computes the hash code according to the given ignored {@code property}. + * + * @param property the ignored property according to which the hash code is computed + * @return the hash code of this object + */ + int hashCodeModProperty(Property property); +} diff --git a/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/equality/Property.java b/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/equality/Property.java new file mode 100644 index 00000000000..4fa37148edb --- /dev/null +++ b/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/equality/Property.java @@ -0,0 +1,24 @@ +package org.key_project.rusty.logic.equality; + +public interface Property { + /** + * Checks {@code t1} and {@code t2} for equality ignoring a certain property. + * + * @param t1 the first element of the equality check + * @param t2 the second element of the equality check + * @param v the additional arguments needed for the equality check + * @return whether {@code t1} and {@code t2} are equal ignoring a certain property + * @param the type of the additional parameters needed for the comparison + */ + boolean equalsModThisProperty(T t1, T t2, V... v); + + /** + * Computes the hash code of {@code t} in a context where + * {@link this#equalsModThisProperty(Object, Object, Object[])} + * is used as an equality check, so that it can be used in, e.g., a HashMap. + * + * @param t the object to compute the hash code for + * @return the hash code of {@code t} ignoring a certain property + */ + int hashCodeModThisProperty(T t); +} diff --git a/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/equality/RenamingProgramElementProperty.java b/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/equality/RenamingProgramElementProperty.java new file mode 100644 index 00000000000..6471d641f3e --- /dev/null +++ b/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/equality/RenamingProgramElementProperty.java @@ -0,0 +1,284 @@ +package org.key_project.rusty.logic.equality; + +import org.key_project.logic.Name; +import org.key_project.logic.SyntaxElement; +import org.key_project.logic.SyntaxElementCursor; +import org.key_project.rusty.ast.stmt.LetStatement; +import org.key_project.rusty.logic.NameAbstractionTable; +import org.key_project.rusty.ast.RustyProgramElement; +import org.key_project.rusty.logic.op.ProgramVariable; + +import java.util.HashMap; +import java.util.Map; + +public class RenamingProgramElementProperty implements Property { + /** + * The single instance of this property. + */ + public static final RenamingProgramElementProperty RENAMING_PROGRAM_ELEMENT_PROPERTY = + new RenamingProgramElementProperty(); + + /** + * This constructor is private as a single instance of this class should be shared. The instance + * can be accessed + * through {@link RenamingProgramElementProperty#RENAMING_PROGRAM_ELEMENT_PROPERTY} and is used as + * a parameter for + * {@link EqualsModProperty#equalsModProperty(Object, Property, Object[])}. + */ + private RenamingProgramElementProperty() {} + + /** + * Checks if {@code rpe2} is a source element syntactically equal to {@code rpe1} modulo renaming. + *

+ * When this method is supplied with a {@link NameAbstractionTable}, it will use this table to + * compare the abstract names of the source elements. If no {@link NameAbstractionTable} is + * supplied, a new one will be created. + * + * @param rpe1 the first element of the equality check + * @param rpe2 the second element of the equality check + * @param v can be a single {@link NameAbstractionTable} for this equality check + * @return {@code true} iff {@code rpe2} is a source element syntactically equal to {@code rpe1} + * modulo renaming + * @param is supposed to be {@link NameAbstractionTable} for this equality check + */ + @Override + public boolean equalsModThisProperty(RustyProgramElement rpe1, RustyProgramElement rpe2, V... v) { + NameAbstractionTable nat; + if (v.length > 0 && (v[0] instanceof NameAbstractionTable n)) { + nat = n; + } else { + nat = new NameAbstractionTable(); + } + + SyntaxElementCursor c1 = rpe1.getCursor(), c2 = rpe2.getCursor(); + SyntaxElement next1, next2; + boolean hasNext1, hasNext2; // Check at the end if both cursors have reached the end + + do { + // First nodes can never be null as cursor is initialized with 'this' + next1 = c1.getCurrentNode(); + next2 = c2.getCurrentNode(); + // Handle special cases of prior equalsModRenaming implementation + if (next1 instanceof LetStatement ls) { + if (!handleLetStatement(ls, next2, nat)) { + return false; + } + } else if (next1 instanceof ProgramVariable || next1 instanceof Name) { + if (!handleProgramVariableOrElementName(next1, next2, nat)) { + return false; + } + } else if (next1.getChildCount() > 0) { + if (!handleRustyNonTerminalProgramElement(next1, + next2)) { + return false; + } + } else { + if (!handleStandard(next1, next2)) { + return false; + } + } + // walk to the next nodes in the tree + } while ((hasNext1 = c1.goToNext()) & (hasNext2 = c2.goToNext())); + + 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(RustyProgramElement RustyProgramElement) { + /* + * Currently, the best approach seems to be to walk through the RustyProgramElement with a + * SyntaxElementCursor and sum up hash codes. + */ + + NameAbstractionMap absMap = new NameAbstractionMap(); + + int hashCode = 1; + SyntaxElementCursor c = RustyProgramElement.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 LetStatement ls) { + hashCode = 31 * hashCode + ls.getChildCount(); + hashCode = + 31 * hashCode + 17 * ((ls.getType() == null) ? 0 : ls.getType().hashCode()); + absMap.add(ls); + } else if (next instanceof ProgramVariable || next instanceof Name) { + hashCode = 31 * hashCode + absMap.getAbstractName((RustyProgramElement) next); + } else if (next.getChildCount() > 0) { + hashCode = 31 * hashCode + next.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 in equalsModThisProperty --------------*/ + /** + * Handles the standard case of comparing two {@link SyntaxElement}s modulo renaming. + * + * @param se1 the first {@link SyntaxElement} to be compared + * @param se2 the second {@link SyntaxElement} to be compared + * @return {@code true} iff the two source elements are equal under the standard {@code equals} + * method + */ + private boolean handleStandard(SyntaxElement se1, SyntaxElement se2) { + /* + * As the prior implementations of equalsModRenaming for RustyProgramElements were mostly the same + * as their normal equals methods, we decided to move equalsModRenaming completely into the + * equals method and handle the special cases separately while walking through the tree that + * is a RustyProgramElement. + */ + return se1.equals(se2); + } + + /** + * Handles the special case of comparing a {@link } to a + * {@link SyntaxElement}. + * + * @param rnte the rusty program element with children to be compared + * @param se the {@link SyntaxElement} to be compared + * @return {@code true} iff {@code se} is of the same class and has the same number of children + * as {@code jnte} + */ + private boolean handleRustyNonTerminalProgramElement(SyntaxElement rnte, + SyntaxElement se) { + /* + * A JavaNonTerminalProgramElement is a special case of a RustyProgramElement, as we must not + * traverse the children recursively through the normal equals method. This is the case + * as we might have to add some entries of children nodes to a NameAbstractionTable so + * that they can be compared later on by the TreeWalker. + */ + if (se == rnte) { + return true; + } + if (se.getClass() != rnte.getClass()) { + return false; + } + return rnte.getChildCount() == se.getChildCount(); + } + + /** + * Handles the special case of comparing a {@link LetStatement} to a + * {@link SyntaxElement}. + * + * @param ls the {@link LetStatement} to be compared + * @param se the {@link SyntaxElement} to be compared + * @param nat the {@link NameAbstractionTable} the variable of {@code vs} should be added to + * @return {@code true} iff {@code se} is of the same class as {@code vs} and has the same + * number of children, dimensions and type + */ + private boolean handleLetStatement(LetStatement ls, SyntaxElement se, + NameAbstractionTable nat) { + /* + * A VariableSpecification is a special case of a JavaNonTerminalProgramElement similar to + * LabeledStatement, but we also need to check the dimensions and type of the + * VariableSpecification. + */ + if (se == ls) { + return true; + } + if (se.getClass() != ls.getClass()) { + return false; + } + final LetStatement other = (LetStatement) se; + if (ls.getChildCount() != se.getChildCount()) { + return false; + } + if (ls.getType() != null) { + if (!ls.getType().equals(other.getType())) { + return false; + } + } else { + if (other.getType() != null) { + return false; + } + } + nat.add(ls.getPattern(), other.getPattern()); + return true; + } + + /** + * Handles the special case of comparing a {@link ProgramVariable} or a + * {@link Name} to a {@link SyntaxElement}. + * + * @param se1 the first {@link SyntaxElement} which is either a {@link ProgramVariable} or a + * {@link Name} + * @param se2 the second {@link SyntaxElement} to be compared + * @param nat the {@link NameAbstractionTable} that should be used to check whether {@code se1} + * and {@code se2} have the same abstract name + * @return {@code true} iff {@code se1} and {@code se2} have the same abstract name + */ + private boolean handleProgramVariableOrElementName(SyntaxElement se1, SyntaxElement se2, + NameAbstractionTable nat) { + /* + * A ProgramVariable or a ProgramElementName is a special case of a RustyProgramElement and one + * of the main reasons for equalsModRenaming. Equality here comes down to checking the + * abstract name of the elements in a NAT. + */ + if (se1.getClass() != se2.getClass()) { + return false; + } + // We can cast here as se1 is either a ProgramVariable or a ProgramElementName + // (this method is only called for these two classes in equalsModThisProperty) + // and se2 is of the same class as se1 + return nat.sameAbstractName((RustyProgramElement) se1, (RustyProgramElement) se2); + } + + + /* ---------- End of helper methods for special cases in equalsModThisProperty ---------- */ + + /** + * A helper class to map {@link RustyProgramElement}s to an abstract name. + *

+ * 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 RustyProgramElement}s with their abstract names. + */ + private final Map map = new HashMap<>(); + + /** + * Adds a {@link RustyProgramElement} to the map. + * + * @param element the {@link RustyProgramElement} to be added + */ + public void add(RustyProgramElement element) { + map.put(element, map.size()); + } + + /** + * Returns the abstract name of a {@link RustyProgramElement} or {@code -1} if the element is not + * in the map. + *

+ * 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 Name} {@code int}. + * + * @param element the {@link RustyProgramElement} whose abstract name should be returned + * @return the abstract name of the {@link RustyProgramElement} or {@code -1} if the element is + * not in the map + */ + public int getAbstractName(RustyProgramElement element) { + final Integer result = map.get(element); + return result != null ? result : -1; + } + } +} diff --git a/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/equality/RenamingTermProperty.java b/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/equality/RenamingTermProperty.java new file mode 100644 index 00000000000..c5d131da478 --- /dev/null +++ b/keyext.rusty_while/src/main/java/org/key_project/rusty/logic/equality/RenamingTermProperty.java @@ -0,0 +1,383 @@ +package org.key_project.rusty.logic.equality; + +import org.key_project.logic.Term; +import org.key_project.logic.op.Operator; +import org.key_project.logic.op.QuantifiableVariable; +import org.key_project.rusty.ast.RustyProgramElement; +import org.key_project.rusty.logic.NameAbstractionTable; +import org.key_project.rusty.logic.RustyBlock; +import org.key_project.rusty.logic.op.Modality; +import org.key_project.rusty.logic.op.ProgramVariable; +import org.key_project.rusty.logic.op.sv.SchemaVariable; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.ImmutableSLList; + +import static org.key_project.rusty.logic.equality.RenamingProgramElementProperty.RENAMING_PROGRAM_ELEMENT_PROPERTY; + +public class RenamingTermProperty implements Property { + /** + * The single instance of this property. + */ + public static final RenamingTermProperty RENAMING_TERM_PROPERTY = new RenamingTermProperty(); + + /** + * This constructor is private as a single instance of this class should be shared. The instance + * can be accessed through {@link RenamingTermProperty#RENAMING_TERM_PROPERTY} and is used as a + * parameter for {@link EqualsModProperty#equalsModProperty(Object, Property, Object[])}. + */ + private RenamingTermProperty() {} + + /** + * Checks if {@code term2} is a term syntactically equal to {@code term1} modulo bound renaming. + * + * @param term1 a term + * @param term2 the term compared to {@code term1} + * @param v should not be used for this equality check + * @return {@code true} iff {@code term2} has the same values in operator, sort, arity, + * varsBoundHere and RustyBlock as {@code term1} modulo bound renaming + * @param is not needed for this equality check + */ + @Override + public boolean equalsModThisProperty(Term term1, Term term2, V... v) { + if (term2 == term1) { + return true; + } + return unifyHelp(term1, term2, ImmutableSLList.nil(), + 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) { + // Labels can be completely ignored + return hashTermHelper(term, ImmutableSLList.nil(), 1); + } + + // equals modulo renaming logic + + /** + * Compare two quantifiable variables if they are equal modulo renaming. + * + * @param ownVar first QuantifiableVariable to be compared + * @param cmpVar second QuantifiableVariable to be compared + * @param ownBoundVars variables bound above the current position + * @param cmpBoundVars variables bound above the current position + */ + private static boolean compareBoundVariables(QuantifiableVariable ownVar, + QuantifiableVariable cmpVar, ImmutableList ownBoundVars, + ImmutableList cmpBoundVars) { + + final int ownNum = indexOf(ownVar, ownBoundVars); + final int cmpNum = indexOf(cmpVar, cmpBoundVars); + + if (ownNum == -1 && cmpNum == -1) { + // if both variables are not bound the variables have to be the + // same object + return ownVar == cmpVar; + } + + // otherwise the variables have to be bound at the same point (and both + // be bound) + return ownNum == cmpNum; + } + + /** + * @return the index of the first occurrence of var in list, or + * -1 if the variable is not an element of the list + */ + private static int indexOf(QuantifiableVariable var, ImmutableList list) { + int res = 0; + while (!list.isEmpty()) { + if (list.head() == var) { + return res; + } + ++res; + list = list.tail(); + } + return -1; + } + + /** + * Compares two terms modulo bound renaming. + * + * @param t0 the first term + * @param t1 the second term + * @param ownBoundVars variables bound above the current position + * @param cmpBoundVars variables bound above the current position + * @return true is returned iff the terms are equal modulo bound renaming + */ + private boolean unifyHelp(Term t0, Term t1, ImmutableList ownBoundVars, + ImmutableList cmpBoundVars, NameAbstractionTable nat) { + + if (t0 == t1 && ownBoundVars.equals(cmpBoundVars)) { + return true; + } + + if (t0.sort() != t1.sort() || t0.arity() != t1.arity()) { + return false; + } + + final Operator op0 = t0.op(); + + if (op0 instanceof QuantifiableVariable) { + return handleQuantifiableVariable(t0, t1, ownBoundVars, cmpBoundVars); + } + + final Operator op1 = t1.op(); + + if (op0 instanceof Modality mod0 && op1 instanceof Modality mod1) { + if (mod0.kind() != mod1.kind()) { + return false; + } + nat = handleRusty(mod0.program(), mod1.program(), nat); + if (nat == FAILED) { + return false; + } + } else if (!(op0 instanceof ProgramVariable) && op0 != op1) { + return false; + } + + if (!(op0 instanceof SchemaVariable) && op0 instanceof ProgramVariable pv0) { + if (op1 instanceof ProgramVariable pv1) { + nat = checkNat(nat); + if (!RENAMING_PROGRAM_ELEMENT_PROPERTY.equalsModThisProperty(pv0, pv1, nat)) { + return false; + } + } else { + return false; + } + } + + 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 true iff the quantifiable variables are equal modulo renaming + */ + private boolean handleQuantifiableVariable(Term t0, Term t1, + ImmutableList ownBoundVars, + ImmutableList cmpBoundVars) { + return (t1.op() instanceof QuantifiableVariable) + && compareBoundVariables((QuantifiableVariable) t0.op(), + (QuantifiableVariable) t1.op(), ownBoundVars, cmpBoundVars); + } + + /** + * used to encode that handleJava results in an unsatisfiable constraint (faster than + * using exceptions) + */ + private static final NameAbstractionTable FAILED = new NameAbstractionTable(); + + /** + * Checks whether the given {@link RustyBlock}s are equal modulo renaming and returns the updated + * {@link NameAbstractionTable} or {@link #FAILED} if the {@link RustyBlock}s are not equal. + * + * @param jb0 the first {@link RustyBlock} to compare + * @param jb1 the second {@link RustyBlock} to compare + * @param nat the {@link NameAbstractionTable} used for the comparison + * @return the updated {@link NameAbstractionTable} if the {@link RustyBlock}s are equal modulo + * renaming or {@link #FAILED} if they are not + */ + private static NameAbstractionTable handleRusty(RustyBlock jb0, RustyBlock jb1, + NameAbstractionTable nat) { + if (!jb0.isEmpty() || !jb1.isEmpty()) { + nat = checkNat(nat); + if (RustyBlocksNotEqualModRenaming(jb0, jb1, nat)) { + return FAILED; + } + } + return nat; + } + + /** + * Returns true if the given {@link RustyBlock}s are not equal modulo renaming. + * + * @param rb1 the first {@link RustyBlock} + * @param rb2 the second {@link RustyBlock} + * @param nat the {@link NameAbstractionTable} used for the comparison + * @return true if the given {@link RustyBlock}s are NOT equal modulo renaming + */ + public static boolean RustyBlocksNotEqualModRenaming(RustyBlock rb1, RustyBlock rb2, + NameAbstractionTable nat) { + RustyProgramElement pe1 = rb1.program(); + RustyProgramElement pe2 = rb2.program(); + if (pe1 == null && pe2 == null) { + return false; + } else if (pe1 != null && pe2 != null) { + return !RENAMING_PROGRAM_ELEMENT_PROPERTY.equalsModThisProperty(pe1, pe2, nat); + } + 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 true iff the subterms are equal modulo renaming + */ + private boolean descendRecursively(Term t0, Term t1, + ImmutableList ownBoundVars, + ImmutableList cmpBoundVars, NameAbstractionTable nat) { + + for (int i = 0; i < t0.arity(); i++) { + ImmutableList subOwnBoundVars = ownBoundVars; + ImmutableList subCmpBoundVars = cmpBoundVars; + + if (t0.varsBoundHere(i).size() != t1.varsBoundHere(i).size()) { + return false; + } + for (int j = 0; j < t0.varsBoundHere(i).size(); j++) { + final QuantifiableVariable ownVar = t0.varsBoundHere(i).get(j); + final QuantifiableVariable cmpVar = t1.varsBoundHere(i).get(j); + if (ownVar.sort() != cmpVar.sort()) { + return false; + } + + subOwnBoundVars = subOwnBoundVars.prepend(ownVar); + subCmpBoundVars = subCmpBoundVars.prepend(cmpVar); + } + + boolean newConstraint = + unifyHelp(t0.sub(i), t1.sub(i), subOwnBoundVars, subCmpBoundVars, nat); + + if (!newConstraint) { + return false; + } + } + + 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(); + } + return nat; + } + // end of equals modulo renaming logic + + + /* -------- Helper methods for hashCodeModThisProperty --------- */ + + /** + * Helps to compute the hash code of a term modulo bound renaming. + *

+ * 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 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 + hashRustyBlock(mod); + } else if (op instanceof ProgramVariable pv) { + hashCode = 17 * hashCode + RENAMING_PROGRAM_ELEMENT_PROPERTY.hashCodeModThisProperty(pv); + } + + return recursiveHelper(term, nameAbstractionList, hashCode); + } + + /** + * Computes the hash code of a quantifiable variable modulo bound renaming. + *

+ * 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 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. + *

+ * 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 hashRustyBlock(Modality mod) { + final RustyBlock rb = mod.program(); + if (!rb.isEmpty()) { + final RustyProgramElement rpe = rb.program(); + return rpe != null ? RENAMING_PROGRAM_ELEMENT_PROPERTY.hashCodeModThisProperty(rpe) : 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. + *

+ * 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 nameAbstractionList, + int hashCode) { + for (int i = 0; i < term.arity(); i++) { + ImmutableList 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 ----- */ +}