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: package de.uka.ilkd.key.rule.updatesimplifier;
010:
011: import java.util.HashMap;
012: import java.util.HashSet;
013:
014: import de.uka.ilkd.key.logic.Name;
015: import de.uka.ilkd.key.logic.Term;
016: import de.uka.ilkd.key.logic.op.*;
017: import de.uka.ilkd.key.logic.sort.AbstractSort;
018: import de.uka.ilkd.key.logic.sort.SetAsListOfSort;
019: import de.uka.ilkd.key.logic.sort.SetOfSort;
020: import de.uka.ilkd.key.logic.sort.Sort;
021: import de.uka.ilkd.key.util.Debug;
022:
023: /**
024: * represents an update and is used as basis data structure for the
025: * updatesimplifier. Currently this is only a naive default implementation.
026: */
027: public abstract class Update {
028:
029: // just for unique handling of anonymous updates
030: // it as to be taken care that this sort does not escape
031: private static final Sort SPECIAL_SORT = new AbstractSort(new Name(
032: "special_sort")) {
033: public SetOfSort extendsSorts() {
034: return SetAsListOfSort.EMPTY_SET;
035: }
036: };
037:
038: /**
039: * @author bubel
040: */
041: public static class UpdateInParts extends Update {
042:
043: private final HashMap loc2assignmentPairs;
044:
045: private final HashSet locationCache;
046:
047: private final ArrayOfAssignmentPair pairs;
048:
049: private SetOfQuantifiableVariable freeVars = null;
050:
051: /**
052: * @param pairs
053: */
054: public UpdateInParts(final ArrayOfAssignmentPair pairs) {
055: this .pairs = pairs;
056: loc2assignmentPairs = new HashMap();
057: this .locationCache = new HashSet();
058:
059: for (int i = 0; i < pairs.size(); i++) {
060: locationCache
061: .add(pairs.getAssignmentPair(i).location());
062: }
063:
064: }
065:
066: /*
067: * (non-Javadoc)
068: *
069: * @see de.uka.ilkd.key.rule.updatesimplifier.Update#getAllAssignmentPairs()
070: */
071: public ArrayOfAssignmentPair getAllAssignmentPairs() {
072: return pairs;
073: }
074:
075: /*
076: * (non-Javadoc)
077: *
078: * @see de.uka.ilkd.key.rule.updatesimplifier.Update#getAssignmentPairs(de.uka.ilkd.key.logic.op.Operator)
079: */
080: public ArrayOfAssignmentPair getAssignmentPairs(Location loc) {
081: if (!loc2assignmentPairs.containsKey(loc)) {
082: ListOfAssignmentPair result = SLListOfAssignmentPair.EMPTY_LIST;
083: for (int i = pairs.size() - 1; i >= 0; i--) {
084: AssignmentPair assignmentPair = pairs
085: .getAssignmentPair(i);
086: final Location op = assignmentPair.location();
087: if (loc.mayBeAliasedBy(op)) {
088: result = result.prepend(assignmentPair);
089: }
090: }
091:
092: loc2assignmentPairs.put(loc, new ArrayOfAssignmentPair(
093: result.toArray()));
094: }
095: return (ArrayOfAssignmentPair) loc2assignmentPairs.get(loc);
096: }
097:
098: /*
099: * (non-Javadoc)
100: *
101: * @see de.uka.ilkd.key.rule.updatesimplifier.Update#hasLocation(de.uka.ilkd.key.logic.op.Operator)
102: */
103: public boolean hasLocation(Location loc) {
104: return locationCache.contains(loc);
105: }
106:
107: /*
108: * (non-Javadoc)
109: *
110: * @see de.uka.ilkd.key.rule.updatesimplifier.Update#location(int)
111: */
112: public Location location(int n) {
113: return pairs.getAssignmentPair(n).location();
114: }
115:
116: /*
117: * (non-Javadoc)
118: *
119: * @see de.uka.ilkd.key.rule.updatesimplifier.Update#locationCount()
120: */
121: public int locationCount() {
122: return pairs.size();
123: }
124:
125: /* (non-Javadoc)
126: * @see de.uka.ilkd.key.rule.updatesimplifier.Update#freeVars()
127: */
128: public SetOfQuantifiableVariable freeVars() {
129: if (freeVars == null) {
130: freeVars = SetAsListOfQuantifiableVariable.EMPTY_SET;
131: for (int i = 0; i != pairs.size(); ++i)
132: freeVars = freeVars.union(pairs
133: .getAssignmentPair(i).freeVars());
134: }
135: return freeVars;
136: }
137:
138: /* (non-Javadoc)
139: * @see de.uka.ilkd.key.rule.updatesimplifier.Update#getAssignmentPair(int)
140: */
141: public AssignmentPair getAssignmentPair(int locPos) {
142: return pairs.getAssignmentPair(locPos);
143: }
144: }
145:
146: private static class UpdateWithUpdateTerm extends Update {
147:
148: private final HashMap loc2assignmentPairs;
149:
150: private HashSet locationCache;
151:
152: private final Term update;
153:
154: private final IUpdateOperator updateOp;
155:
156: private SetOfQuantifiableVariable freeVars = null;
157:
158: public UpdateWithUpdateTerm(Term update) {
159: this .update = update;
160: this .updateOp = (IUpdateOperator) update.op();
161: this .loc2assignmentPairs = new HashMap();
162:
163: for (int i = 0; i < updateOp.locationCount(); i++) {
164: if (updateOp.location(i) == StarLocation.ALL)
165: Debug
166: .fail("Anonymous update shall not be created using this "
167: + "class. (at least as long no generalized terms are "
168: + "supported)");
169: }
170: }
171:
172: /**
173: * @return
174: */
175: public ArrayOfAssignmentPair getAllAssignmentPairs() {
176: final AssignmentPair[] result = new AssignmentPair[locationCount()];
177: for (int i = 0; i < locationCount(); i++) {
178: result[i] = getAssignmentPair(i);
179: }
180: return new ArrayOfAssignmentPair(result);
181: }
182:
183: public AssignmentPair getAssignmentPair(int locPos) {
184: if (updateOp instanceof AnonymousUpdate)
185: return new AssignmentPairLazy(update, locPos);
186: else if (updateOp instanceof QuanUpdateOperator)
187: return new QuanAssignmentPairLazy(update, locPos);
188: else
189: Debug.fail("Unknown update operator");
190: return null; // unreachable
191: }
192:
193: /**
194: * determines and returns all assignment pairs whose location part may
195: * be an alias of <code>loc</code>
196: */
197: public ArrayOfAssignmentPair getAssignmentPairs(Location loc) {
198: if (!loc2assignmentPairs.containsKey(loc)) {
199: ListOfAssignmentPair result = SLListOfAssignmentPair.EMPTY_LIST;
200: for (int i = updateOp.locationCount() - 1; i >= 0; i--) {
201: if (loc.mayBeAliasedBy(updateOp.location(i)))
202: result = result.prepend(getAssignmentPair(i));
203: }
204:
205: loc2assignmentPairs.put(loc, new ArrayOfAssignmentPair(
206: result.toArray()));
207: }
208: return (ArrayOfAssignmentPair) loc2assignmentPairs.get(loc);
209: }
210:
211: public boolean hasLocation(Location loc) {
212: if (locationCache == null) {
213: this .locationCache = new HashSet();
214:
215: for (int i = 0; i < updateOp.locationCount(); i++) {
216: locationCache.add(updateOp.location(i));
217: }
218: }
219: return locationCache.contains(loc);
220: }
221:
222: public Location location(int n) {
223: return updateOp.location(n);
224: }
225:
226: /**
227: * returns the number of locations
228: *
229: * @return the number of locations as int
230: */
231: public int locationCount() {
232: return updateOp.locationCount();
233: }
234:
235: /* (non-Javadoc)
236: * @see de.uka.ilkd.key.rule.updatesimplifier.Update#freeVars()
237: */
238: public SetOfQuantifiableVariable freeVars() {
239: if (freeVars == null) {
240: if (update.sub(update.arity() - 1).freeVars().size() == 0) {
241: freeVars = update.freeVars();
242: } else {
243: freeVars = SetAsListOfQuantifiableVariable.EMPTY_SET;
244: for (int i = 0; i != locationCount(); ++i)
245: freeVars = freeVars.union(getAssignmentPair(i)
246: .freeVars());
247: }
248: }
249: return freeVars;
250: }
251: }
252:
253: /**
254: * creates an update representation out of the top level operator of the
255: * given update term
256: */
257: public static Update createUpdate(AssignmentPair[] pairs) {
258: return new UpdateInParts(new ArrayOfAssignmentPair(pairs));
259: }
260:
261: /**
262: * creates an update representation out of the top level operator of the
263: * given update term. If it is no update term an update with zero assignment
264: * pairs is returned (only for temporarly representations)
265: */
266: public static Update createUpdate(Term t) {
267: if (t.op() instanceof AnonymousUpdate) {
268: Term valueTerm = UpdateSimplifierTermFactory.DEFAULT
269: .getBasicTermFactory().createFunctionTerm(
270: new RigidFunction(t.op().name(),
271: SPECIAL_SORT, new Sort[0]));
272: AssignmentPair pair = new AssignmentPairImpl(
273: StarLocation.ALL, new Term[0], valueTerm);
274: return createUpdate(new AssignmentPair[] { pair });
275: } else if (!(t.op() instanceof IUpdateOperator)) {
276: return createUpdate(new AssignmentPair[0]);
277: }
278: return new UpdateWithUpdateTerm(t);
279: }
280:
281: /**
282: * @return
283: */
284: public abstract ArrayOfAssignmentPair getAllAssignmentPairs();
285:
286: /**
287: * determines and returns all assignment pairs whose location part has the
288: * same top level operator as the given one
289: */
290: public abstract ArrayOfAssignmentPair getAssignmentPairs(
291: Location loc);
292:
293: /**
294: * returns true if the given location is updated by this update
295: *
296: * @param location
297: * the Operator specifying the location which is updated
298: * @return true if location occurs on the left side of an assignment pair in
299: * this update
300: */
301: public abstract boolean hasLocation(Location loc);
302:
303: /**
304: * returns the n-th location operator
305: *
306: * @param n
307: * an int specifying the position of the location operator to be
308: * retrieved
309: * @return the n-tl location operator
310: */
311: public abstract Location location(int n);
312:
313: /**
314: * returns the number of locations
315: *
316: * @return the number of locations as int
317: */
318: public abstract int locationCount();
319:
320: /**
321: * returns true if this update object describes an anonymous update
322: */
323: public boolean isAnonymousUpdate() {
324: return hasLocation(StarLocation.ALL);
325: }
326:
327: /**
328: * @return the set of quantifiable variables that turn up free in this
329: * update (when applying the update, it might happen that such
330: * variables have to be renaming to avoid collisions)
331: */
332: public abstract SetOfQuantifiableVariable freeVars();
333:
334: public String toString() {
335: StringBuffer result = new StringBuffer("{");
336: ArrayOfAssignmentPair pairs = getAllAssignmentPairs();
337: for (int i = 0; i < pairs.size(); i++) {
338: result.append(pairs.getAssignmentPair(i).toString());
339: if (i < pairs.size() - 1)
340: result.append(" || ");
341: }
342: result.append("}");
343: return result.toString();
344: }
345:
346: // these classes are used to unify treatment of anonymous and
347: // normal updates. May become obsolete with generalized terms
348: public static class StarLocation extends NonRigidFunction implements
349: Location {
350:
351: // important "name" must be initialized before ALL!
352: private final static Name name = new Name("*");
353:
354: public final static StarLocation ALL = new StarLocation();
355:
356: private StarLocation() {
357: super (name, SPECIAL_SORT, new Sort[0]);
358: }
359:
360: /* (non-Javadoc)
361: * @see de.uka.ilkd.key.logic.op.Location#mayBeAliasedBy(de.uka.ilkd.key.logic.op.Location)
362: */
363: public boolean mayBeAliasedBy(Location loc) {
364: return false;
365: }
366:
367: /* (non-Javadoc)
368: * @see de.uka.ilkd.key.logic.op.Operator#name()
369: */
370: public Name name() {
371: return name;
372: }
373:
374: /* (non-Javadoc)
375: * @see de.uka.ilkd.key.logic.op.Operator#validTopLevel(de.uka.ilkd.key.logic.Term)
376: */
377: public boolean validTopLevel(Term term) {
378: return term.arity() == 0 && term.sort() != Sort.FORMULA;
379: }
380:
381: /* (non-Javadoc)
382: * @see de.uka.ilkd.key.logic.op.Operator#sort(de.uka.ilkd.key.logic.Term[])
383: */
384: public Sort sort(Term[] term) {
385: return SPECIAL_SORT;
386: }
387:
388: /* (non-Javadoc)
389: * @see de.uka.ilkd.key.logic.op.Operator#arity()
390: */
391: public int arity() {
392: return 0;
393: }
394:
395: /* (non-Javadoc)
396: * @see de.uka.ilkd.key.logic.op.Operator#isRigid(de.uka.ilkd.key.logic.Term)
397: */
398: public boolean isRigid(Term term) {
399: return true;
400: }
401:
402: }
403:
404: public abstract AssignmentPair getAssignmentPair(int locPos);
405: }
|