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.updatesimplifier;
012:
013: import de.uka.ilkd.key.logic.Term;
014: import de.uka.ilkd.key.logic.TermFactory;
015: import de.uka.ilkd.key.logic.op.IUpdateOperator;
016: import de.uka.ilkd.key.logic.op.Location;
017: import de.uka.ilkd.key.logic.op.SetOfQuantifiableVariable;
018: import de.uka.ilkd.key.logic.sort.AbstractSort;
019:
020: /**
021: *
022: */
023: abstract class AbstractAssignmentPairLazy implements AssignmentPair {
024:
025: /**
026: * term with the update operator as top level operator to which the modeled assignment pair belongs
027: */
028: private final Term update;
029: private SetOfQuantifiableVariable freeVars = null;
030:
031: /**
032: * stores the location hash code
033: */
034: private int locationHash = 0;
035:
036: /**
037: * caches the value part of the assignment pair
038: * (avoids repeated creation of casts)
039: */
040: private Term safeValueCache = null;
041:
042: /**
043: * caches created terms denoting the locations
044: */
045: private Term[] locationSubsCache = null;
046: private int subtermsBeginCache = -1;
047: private int subtermsEndCache = -1;
048:
049: protected AbstractAssignmentPairLazy(final Term update,
050: int locationPos) {
051: this .update = update;
052: this .locationPos = locationPos;
053: }
054:
055: protected Term getUpdateTerm() {
056: return update;
057: }
058:
059: protected IUpdateOperator getUpdateOp() {
060: return (IUpdateOperator) getUpdateTerm().op();
061: }
062:
063: /**
064: * the position <code> i </code> of the location in the update operator
065: */
066: private final int locationPos;
067:
068: protected int getLocationPos() {
069: return locationPos;
070: }
071:
072: /**
073: * returns the location
074: * @return the left side of the assignment
075: */
076: public Term locationAsTerm() {
077: return getUpdateOp()
078: .location(getUpdateTerm(), getLocationPos());
079: }
080:
081: /**
082: * returns the location operator
083: * @return the location specifying operator
084: */
085: public Location location() {
086: return getUpdateOp().location(getLocationPos());
087: }
088:
089: /**
090: * returns the locations sub terms
091: * @return the left side of the assignment
092: */
093: public Term[] locationSubs() {
094: if (locationSubsCache == null) {
095: locationSubsCache = new Term[location().arity()];
096: for (int i = 0, j = locationSubtermsBegin(); j != locationSubtermsEnd(); ++i, ++j)
097: locationSubsCache[i] = getUpdateTerm().sub(j);
098: }
099: return locationSubsCache;
100: }
101:
102: protected int locationSubtermsBegin() {
103: if (subtermsBeginCache == -1)
104: subtermsBeginCache = getUpdateOp().locationSubtermsBegin(
105: getLocationPos());
106: return subtermsBeginCache;
107: }
108:
109: protected int locationSubtermsEnd() {
110: if (subtermsEndCache == -1)
111: subtermsEndCache = getUpdateOp().locationSubtermsEnd(
112: getLocationPos());
113: return subtermsEndCache;
114: }
115:
116: /**
117: * returns an int fulfilling the usual hashcode properties but without
118: * consideration of the value part of the assignment pair
119: *
120: * @return an int as location hashcode
121: */
122: public int locationHashCode() {
123: if (locationHash == 0) {
124: locationHash = location().hashCode();
125: final Term[] locSubs = locationSubs();
126: for (int i = 0; i < locSubs.length; i++) {
127: locationHash += 17 * locSubs[i].hashCode();
128: }
129: if (locationHash == 0) {
130: locationHash = 1;
131: }
132: }
133: return locationHash;
134: }
135:
136: /**
137: * returns true if the location that is updated is equal to location of the
138: * given assignment pair
139: *
140: * @param p
141: * the AssignmentPair whose location is compared
142: * @return true if the location that is updated is equal to location of the
143: * given assignment pair
144: */
145: public boolean equalLocations(AssignmentPair p) {
146: if (p.location() != location())
147: return false;
148:
149: final Term[] pLocSubs = p.locationSubs();
150: final Term[] tLocSubs = this .locationSubs();
151:
152: if (pLocSubs.length != tLocSubs.length)
153: return false;
154:
155: for (int i = 0; i < pLocSubs.length; i++) {
156: if (!(pLocSubs[i].equals(tLocSubs[i])))
157: return false;
158: }
159: return true;
160: }
161:
162: /**
163: * returns the value that is assigned to the location and adds
164: * if necessary (i.e. the static type <code>T</code> of the location as term is not a
165: * supersort) a type cast <code> (T) </code> in front.
166: * @return the right side of the assignment
167: */
168: public Term value() {
169: if (safeValueCache == null) {
170: safeValueCache = valueUnsafe();
171: final AbstractSort s = (AbstractSort) locationAsTerm()
172: .sort();
173: if (!(safeValueCache.sort().extendsTrans(s))) {
174: safeValueCache = TermFactory.DEFAULT
175: .createFunctionTerm(s.getCastSymbol(),
176: safeValueCache);
177: }
178: }
179: return safeValueCache;
180: }
181:
182: /**
183: * returns the value that is assigned to the location
184: * (no implicit casts are added and therefore themethod is not type safe)
185: * You should be sure what you are doing if using this method, otherwise
186: * {@link AbstractAssignmentPairLazy#value}
187: * @return the right side of the assignment
188: */
189: public Term valueUnsafe() {
190: return getUpdateTerm().sub(valuePos());
191: }
192:
193: protected int valuePos() {
194: return getUpdateOp().valuePos(getLocationPos());
195: }
196:
197: /* (non-Javadoc)
198: * @see de.uka.ilkd.key.rule.updatesimplifier.AssignmentPair#freeVars()
199: */
200: public SetOfQuantifiableVariable freeVars() {
201: if (freeVars == null) {
202: freeVars = guard().freeVars().union(
203: valueUnsafe().freeVars());
204: for (int i = 0; i != locationSubs().length; ++i)
205: freeVars = freeVars.union(locationSubs()[i].freeVars());
206:
207: for (int i = 0; i != boundVars().size(); ++i)
208: freeVars = freeVars.remove(boundVars()
209: .getQuantifiableVariable(i));
210: }
211:
212: return freeVars;
213: }
214:
215: public String toString() {
216: return ""
217: + (boundVars().size() > 0 ? "\\for " + boundVars()
218: + " " : "")
219: + (nontrivialGuard() ? "\\if (" + guard() + ") " : "")
220: + locationAsTerm() + ":=" + valueUnsafe();
221: }
222:
223: /**
224: * returns true if the given object equals this one
225: */
226: public boolean equals(Object o) {
227: if (!(o instanceof AssignmentPair))
228: return false;
229:
230: final AssignmentPair p = (AssignmentPair) o;
231:
232: return equalLocations(p)
233: && p.valueUnsafe().equals(valueUnsafe())
234: && p.guard().equals(guard())
235: && boundVars().equals(boundVars());
236: }
237:
238: /**
239: * the hashCode of this assignment pair
240: */
241: public int hashCode() {
242: return locationHashCode() + 17 * value().hashCode() + 23
243: * guard().hashCode() + 31 * boundVars().hashCode();
244: }
245: }
|