001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.rule;
012:
013: import de.uka.ilkd.key.logic.BoundVariableTools;
014: import de.uka.ilkd.key.logic.Term;
015: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
016: import de.uka.ilkd.key.logic.op.IUpdateOperator;
017: import de.uka.ilkd.key.util.Debug;
018:
019: /**
020: * Represents a pair of an update operator and the term
021: * that is used to update the variable(attribute) of update operator.
022: *
023: * The equals method implements equals mod renaming but with a strict sort
024: * restriction.
025: */
026: public class UpdatePair {
027:
028: /** the update terms */
029: private final Term update;
030:
031: public UpdatePair(Term update) {
032: // super(update.op(), Sort.FORMULA);
033: Debug.assertTrue(update.op() instanceof IUpdateOperator,
034: "updatepair:: simultaneous update expected");
035: this .update = update;
036: }
037:
038: public int arity() {
039: return update.arity() - 1;
040: }
041:
042: public Term sub(int n) {
043: if (n >= arity()) {
044: throw new IndexOutOfBoundsException();
045: }
046: return update.sub(n);
047: }
048:
049: public ArrayOfQuantifiableVariable varsBoundHere(int n) {
050: if (n >= arity())
051: throw new IndexOutOfBoundsException();
052: return update.varsBoundHere(n);
053: }
054:
055: public IUpdateOperator updateOperator() {
056: return (IUpdateOperator) update.op();
057: }
058:
059: /**
060: * equals modulo renaming of bound variables
061: */
062: public boolean equals(Object o) {
063: if (!(o instanceof UpdatePair)) {
064: return false;
065: }
066: final UpdatePair cmp = (UpdatePair) o;
067:
068: if (cmp.updateOperator() != updateOperator()) {
069: return false;
070: }
071:
072: for (int i = 0, ar = arity(); i < ar; i++) {
073: final ArrayOfQuantifiableVariable qVars = varsBoundHere(i);
074: final ArrayOfQuantifiableVariable cmpQVars = cmp
075: .varsBoundHere(i);
076: if (qVars.size() != cmpQVars.size()) {
077: return false;
078: } else if (qVars.size() == 0) {
079: if (!sub(i).equals(cmp.sub(i))) {
080: return false;
081: }
082: } else {
083: if (!BoundVariableTools.DEFAULT.equalsModRenaming(
084: qVars, sub(i), cmpQVars, cmp.sub(i))) {
085: return false;
086: }
087: }
088: }
089: return true;
090: }
091:
092: public int hashCode() {
093: int result = 17;
094: result = 37 * result;
095: return result;
096: }
097:
098: public String toString() {
099: return "{pair:" + update.toString() + "}";
100: }
101:
102: }
|