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: * Created on 26.11.2004
011: */
012: package de.uka.ilkd.key.rule.updatesimplifier;
013:
014: import de.uka.ilkd.key.logic.JavaBlock;
015: import de.uka.ilkd.key.logic.Term;
016: import de.uka.ilkd.key.logic.TermFactory;
017: import de.uka.ilkd.key.logic.op.*;
018: import de.uka.ilkd.key.logic.sort.AbstractSort;
019: import de.uka.ilkd.key.util.Debug;
020:
021: /**
022: * The default implementation of an assignment pair.
023: * There exists a lazy one to which may spare resources
024: * @see de.uka.ilkd.key.rule.updatesimplifier.AsssignmentPairLazy
025: * @author bubel
026: */
027: public class AssignmentPairImpl implements AssignmentPair {
028:
029: private final Location accessOp;
030: private final Term[] locSubs;
031: private final Term value;
032:
033: /**
034: * caches the value part of the assignment pair
035: * (avoids repeated creation of casts)
036: */
037: private Term safeValueCache = null;
038:
039: private int cachedLocationHashCode;
040: private final Term guard;
041: private final ArrayOfQuantifiableVariable boundVars;
042: private SetOfQuantifiableVariable freeVars = null;
043:
044: public AssignmentPairImpl(
045: final ArrayOfQuantifiableVariable boundVars,
046: final Term guard, final Location accessOp,
047: final Term[] locSubs, final Term value) {
048: this .boundVars = boundVars;
049: this .guard = guard;
050: this .accessOp = accessOp;
051: this .locSubs = locSubs;
052: this .value = value;
053: }
054:
055: /**
056: * creates the assignment <code>accessOp(locSubs):=value</code>
057: * @param accessOp the Location descriptor
058: * @param locSubs the subterms of the location
059: * @param value the value the location is updated to
060: */
061: public AssignmentPairImpl(final Location accessOp,
062: final Term[] locSubs, final Term value) {
063: this (new ArrayOfQuantifiableVariable(),
064: UpdateSimplifierTermFactory.DEFAULT.getValidGuard(),
065: accessOp, locSubs, value);
066: }
067:
068: /**
069: *
070: * returns the left side of the assignment pair as a term
071: *
072: * @see de.uka.ilkd.key.rule.updatesimplifier.AssignmentPair#locationAsTerm()
073: */
074: public Term locationAsTerm() {
075: return TermFactory.DEFAULT.createTerm(accessOp, locSubs,
076: new ArrayOfQuantifiableVariable(),
077: JavaBlock.EMPTY_JAVABLOCK);
078: }
079:
080: /**
081: * returns the location descriptor
082: * @see de.uka.ilkd.key.rule.updatesimplifier.AssignmentPair#location()
083: */
084: public Location location() {
085: return accessOp;
086: }
087:
088: /**
089: * returns the sub terms of the location
090: * @see de.uka.ilkd.key.rule.updatesimplifier.AssignmentPair#locationSubs()
091: */
092: public Term[] locationSubs() {
093: return locSubs;
094: }
095:
096: /**
097: * returns the value the location is updated to
098: * @see de.uka.ilkd.key.rule.updatesimplifier.AssignmentPair#value()
099: */
100: public Term valueUnsafe() {
101: return value;
102: }
103:
104: /**
105: * returns the value that is assigned to the location and adds
106: * if necessary (i.e. the static type <code>T</code> of the location as term is not a
107: * supersort) a type cast <code> (T) </code> in front.
108: * @return the right side of the assignment
109: */
110: public Term value() {
111: if (safeValueCache == null) {
112: safeValueCache = valueUnsafe();
113: final AbstractSort s = (AbstractSort) locationAsTerm()
114: .sort();
115: if (!(safeValueCache.sort().extendsTrans(s))) {
116: safeValueCache = TermFactory.DEFAULT
117: .createFunctionTerm(s.getCastSymbol(),
118: safeValueCache);
119: }
120: }
121: return safeValueCache;
122: }
123:
124: /* (non-Javadoc)
125: * @see de.uka.ilkd.key.rule.updatesimplifier.AssignmentPair#boundVars()
126: */
127: public ArrayOfQuantifiableVariable boundVars() {
128: return boundVars;
129: }
130:
131: /* (non-Javadoc)
132: * @see de.uka.ilkd.key.rule.updatesimplifier.AssignmentPair#freeVars()
133: */
134: public SetOfQuantifiableVariable freeVars() {
135: if (freeVars == null) {
136: freeVars = guard().freeVars().union(value().freeVars());
137: for (int i = 0; i != locationSubs().length; ++i)
138: freeVars = freeVars.union(locationSubs()[i].freeVars());
139:
140: for (int i = 0; i != boundVars().size(); ++i)
141: freeVars = freeVars.remove(boundVars()
142: .getQuantifiableVariable(i));
143: }
144:
145: return freeVars;
146: }
147:
148: /*
149: * (non-Javadoc)
150: *
151: * @see de.uka.ilkd.key.rule.updatesimplifier.AssignmentPair#guard()
152: */
153: public Term guard() {
154: return guard;
155: }
156:
157: /* (non-Javadoc)
158: * @see de.uka.ilkd.key.rule.updatesimplifier.AssignmentPair#nontrivialGuard()
159: */
160: public boolean nontrivialGuard() {
161: return guard().op() != Op.TRUE;
162: }
163:
164: /**
165: * true if the locations of both assignment pairs are equal
166: *
167: * @see de.uka.ilkd.key.rule.updatesimplifier.AssignmentPair#equalLocations(de.uka.ilkd.key.rule.updatesimplifier.AssignmentPair)
168: */
169: public boolean equalLocations(AssignmentPair p) {
170: if (p.location() != accessOp) {
171: return false;
172: }
173: Term[] cmpLocSubs = p.locationSubs();
174: Debug.assertTrue(locSubs.length == cmpLocSubs.length);
175: for (int i = 0; i < locSubs.length; i++) {
176: if (!locSubs[i].equals(cmpLocSubs[i])) {
177: return false;
178: }
179: }
180: return true;
181: }
182:
183: /**
184: * hashcode implementation
185: * @see de.uka.ilkd.key.rule.updatesimplifier.AssignmentPair#locationHashCode()
186: */
187: public int locationHashCode() {
188: if (cachedLocationHashCode == 0) {
189: cachedLocationHashCode = accessOp.hashCode();
190: for (int i = 0; i < locSubs.length; i++) {
191: cachedLocationHashCode += 17 * locSubs[i].hashCode();
192: }
193: if (cachedLocationHashCode == 0) {
194: cachedLocationHashCode = 1;
195: }
196: }
197: return cachedLocationHashCode;
198: }
199:
200: /**
201: * the hashCode of this assignment pair
202: */
203: public int hashCode() {
204: return locationHashCode() + 17 * valueUnsafe().hashCode() + 23
205: * guard().hashCode() + 31 * boundVars().hashCode();
206: }
207:
208: /**
209: * returns true if the given object equals this one
210: */
211: public boolean equals(Object o) {
212: if (!(o instanceof AssignmentPair))
213: return false;
214:
215: final AssignmentPair p = (AssignmentPair) o;
216:
217: return equalLocations(p)
218: && p.valueUnsafe().equals(valueUnsafe())
219: && p.guard().equals(guard())
220: && boundVars().equals(boundVars());
221: }
222:
223: private String printBoundVars() {
224: StringBuffer sb = new StringBuffer();
225: QuantifiableVariable qvar = null;
226: if (boundVars().size() == 1) {
227: qvar = boundVars().getQuantifiableVariable(0);
228: if (qvar instanceof LogicVariable) {
229: sb.append(((LogicVariable) qvar).sort() + " "
230: + ((LogicVariable) qvar).name());
231: } else {
232: sb.append(qvar);
233: }
234: sb.append("; ");
235: } else {
236: sb.append("(");
237: for (int i = 0; i < boundVars().size(); i++) {
238: qvar = boundVars().getQuantifiableVariable(i);
239: if (qvar instanceof LogicVariable) {
240: sb.append(((LogicVariable) qvar).sort() + " "
241: + ((LogicVariable) qvar).name());
242: } else {
243: sb.append(qvar);
244: }
245: if (i < boundVars().size() - 1) {
246: sb.append("; ");
247: }
248: }
249: sb.append(")");
250: }
251: return sb.toString();
252: }
253:
254: public String toString() {
255: return ""
256: + (boundVars().size() > 0 ? "\\for " + printBoundVars()
257: + " " : "")
258: + (nontrivialGuard() ? "\\if (" + guard() + ") " : "")
259: + locationAsTerm() + ":=" + valueUnsafe();
260: }
261:
262: }
|