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.inst;
012:
013: import de.uka.ilkd.key.java.ArrayOfProgramElement;
014: import de.uka.ilkd.key.java.ProgramElement;
015: import de.uka.ilkd.key.java.Services;
016: import de.uka.ilkd.key.java.reference.ExecutionContext;
017: import de.uka.ilkd.key.logic.Name;
018: import de.uka.ilkd.key.logic.PosInProgram;
019: import de.uka.ilkd.key.logic.ProgramElementName;
020: import de.uka.ilkd.key.logic.Term;
021: import de.uka.ilkd.key.logic.op.*;
022: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
023: import de.uka.ilkd.key.rule.ListOfUpdatePair;
024: import de.uka.ilkd.key.rule.SLListOfObject;
025: import de.uka.ilkd.key.rule.SLListOfUpdatePair;
026: import de.uka.ilkd.key.rule.UpdatePair;
027: import de.uka.ilkd.key.util.Debug;
028:
029: /**
030: * This class wraps a MapFromSchemaVariableToInstantiationEntry and is used to
031: * store instantiations of schemavariables. The class is immutable, this means
032: * changing its content will result in creating a new object.
033: */
034: public class SVInstantiations {
035: /** the empty instantiation */
036: public static final SVInstantiations EMPTY_SVINSTANTIATIONS = new SVInstantiations();
037:
038: /**
039: * the context itself is not realised as a schemavariable, therefore we need
040: * here a dummy SV for a more unified handling (key in map)
041: */
042: private static final SchemaVariable CONTEXTSV = SchemaVariableFactory
043: .createProgramSV(
044: new ProgramElementName("Context"),
045: new ProgramSVSort(new Name("ContextStatementBlock")) {
046: public boolean canStandFor(ProgramElement pe,
047: Services services) {
048: return true;
049: }
050: }, false); // just a dummy SV for context
051:
052: /** the map with the instantiations to logic terms */
053: private final MapFromSchemaVariableToInstantiationEntry map;
054:
055: /**
056: * just a list of "interesting" instantiations: these instantiations are not
057: * 100% predetermined and worth saving in a proof
058: */
059: private final MapFromSchemaVariableToInstantiationEntry interesting;
060:
061: /**
062: * updates may be ignored when matching, therefore they need to be added
063: * after the application around the added/replaced parts. These are stored
064: * in this list
065: */
066: private final ListOfUpdatePair updateContext;
067:
068: /** instantiations of generic sorts */
069: private GenericSortInstantiations genericSortInstantiations = GenericSortInstantiations.EMPTY_INSTANTIATIONS;
070:
071: /** additional conditions for the generic sorts */
072: private final ListOfGenericSortCondition genericSortConditions;
073:
074: /** integer to cache the hashcode */
075: private int hashcode = 0;
076:
077: /** creates a new SVInstantions object with an empty map */
078: private SVInstantiations() {
079: genericSortConditions = SLListOfGenericSortCondition.EMPTY_LIST;
080: updateContext = SLListOfUpdatePair.EMPTY_LIST;
081: map = MapAsListFromSchemaVariableToInstantiationEntry.EMPTY_MAP;
082: interesting = MapAsListFromSchemaVariableToInstantiationEntry.EMPTY_MAP;
083: }
084:
085: /**
086: * creates a new SVInstantions object using the given map
087: *
088: * @param map
089: * the MapFromSchemaVariableToInstantiationEntry with the
090: * instantiations
091: */
092: private SVInstantiations(
093: MapFromSchemaVariableToInstantiationEntry map,
094: MapFromSchemaVariableToInstantiationEntry interesting,
095: ListOfUpdatePair updateContext,
096: ListOfGenericSortCondition genericSortConditions) {
097: this (map, interesting, updateContext,
098: GenericSortInstantiations.EMPTY_INSTANTIATIONS,
099: genericSortConditions);
100: }
101:
102: private SVInstantiations(
103: MapFromSchemaVariableToInstantiationEntry map,
104: MapFromSchemaVariableToInstantiationEntry interesting,
105: ListOfUpdatePair updateContext,
106: GenericSortInstantiations genericSortInstantiations,
107: ListOfGenericSortCondition genericSortConditions) {
108: this .map = map;
109: this .interesting = interesting;
110: this .updateContext = updateContext;
111: this .genericSortInstantiations = genericSortInstantiations;
112: this .genericSortConditions = genericSortConditions;
113: }
114:
115: public GenericSortInstantiations getGenericSortInstantiations() {
116: return genericSortInstantiations;
117: }
118:
119: public ListOfGenericSortCondition getGenericSortConditions() {
120: return genericSortConditions;
121: }
122:
123: /**
124: * adds the given pair to the instantiations. If the given SchemaVariable
125: * has been instantiated already, the new pair is taken without a warning.
126: *
127: * @param sv
128: * the SchemaVariable to be instantiated
129: * @param subst
130: * the Term the SchemaVariable is instantiated with
131: * @return SVInstantiations the new SVInstantiations containing the given
132: * pair
133: */
134: public SVInstantiations add(SchemaVariable sv, Term subst) {
135: return add(sv, new TermInstantiation(sv, subst));
136: }
137:
138: public SVInstantiations add(OperatorSV sv,
139: de.uka.ilkd.key.logic.op.Operator op) {
140: return add(sv, new OperatorInstantiation(sv, op));
141: }
142:
143: public SVInstantiations addInteresting(SchemaVariable sv, Term subst) {
144: return addInteresting(sv, new TermInstantiation(sv, subst));
145: }
146:
147: public SVInstantiations add(SchemaVariable sv, ProgramElement pe,
148: int instantiationType) {
149: return add(sv, new ProgramSkolemInstantiation(sv, pe,
150: instantiationType));
151: }
152:
153: public SVInstantiations addInteresting(SchemaVariable sv, Name name) {
154: return addInteresting(sv, new NameInstantiationEntry(sv, name));
155: }
156:
157: public SVInstantiations add(SchemaVariable sv, ProgramList pes) {
158: return add(sv, new ProgramListInstantiation(sv, pes.getList()));
159: }
160:
161: public SVInstantiations addList(SchemaVariable sv, Object[] list) {
162: return add(sv, new ListInstantiation(sv,
163: SLListOfObject.EMPTY_LIST.prepend(list)));
164: }
165:
166: /** adds the given pair to the instantiations. If the given
167: * SchemaVariable has been instantiated already, the new pair is
168: * taken without a warning.
169: * @param sv the SchemaVariable to be instantiated
170: * @param pe the ProgramElement the SchemaVariable is instantiated with
171: * @return SVInstantiations the new SVInstantiations containing
172: * the given pair
173: */
174: public SVInstantiations add(SchemaVariable sv, ProgramElement pe) {
175: return add(sv, new ProgramInstantiation(sv, pe));
176: }
177:
178: public SVInstantiations addInteresting(SchemaVariable sv,
179: ProgramElement pe) {
180: return addInteresting(sv, new ProgramInstantiation(sv, pe));
181: }
182:
183: public SVInstantiations addInterestingList(SchemaVariable sv,
184: Object[] list) {
185: return addInteresting(sv, new ListInstantiation(sv,
186: SLListOfObject.EMPTY_LIST.prepend(list)));
187: }
188:
189: /**
190: * adds the given pair to the instantiations for the context.If the context
191: * has been instantiated already, the new pair is taken without a warning.
192: *
193: * @param prefix
194: * the PosInProgram describing the prefix
195: * @param postfix
196: * the PosInProgram describing the postfix
197: * @param activeStatementContext
198: * the ExecutionContext of the first active statement
199: * @param pe
200: * the ProgramElement the context positions are related to
201: * @return SVInstantiations the new SVInstantiations containing the given
202: * pair
203: */
204: public SVInstantiations add(PosInProgram prefix,
205: PosInProgram postfix,
206: ExecutionContext activeStatementContext, ProgramElement pe) {
207: return add(CONTEXTSV, new ContextInstantiationEntry(CONTEXTSV,
208: prefix, postfix, activeStatementContext, pe));
209: }
210:
211: // the following two exceptions are created statically for performance
212: private static final SortException INCOMPATIBLE_INSTANTIATION_EXCEPTION = new SortException(
213: "Sort of SV " + "is not compatible with its "
214: + "instantiation's sort\n"
215: + "(This exception object is static)");
216:
217: private static final IllegalInstantiationException CONVERT_INSTANTIATION_EXCEPTION = new SortException(
218: "Instantiation of SV " + "cannot be converted to logic\n"
219: + "(This exception object is static)");
220:
221: private static final SortException UNSOLVABLE_SORT_CONDITIONS_EXCEPTION = new SortException(
222: "Conditions for sorts" + " cannot be satisfied\n"
223: + "(This exception object is static)");
224:
225: private SVInstantiations checkSorts(InstantiationEntry p_entry,
226: boolean p_forceRebuild) {
227: Boolean b = getGenericSortInstantiations().checkSorts(p_entry);
228:
229: if (b == null)
230: return rebuildSorts();
231: else if (!b.booleanValue())
232: throw INCOMPATIBLE_INSTANTIATION_EXCEPTION;
233: if (p_forceRebuild)
234: return rebuildSorts();
235: return this ;
236: }
237:
238: private SVInstantiations checkCondition(GenericSortCondition p_c,
239: boolean p_forceRebuild) {
240: Boolean b = getGenericSortInstantiations().checkCondition(p_c);
241:
242: if (b == null)
243: return rebuildSorts();
244: else if (!b.booleanValue())
245: throw UNSOLVABLE_SORT_CONDITIONS_EXCEPTION;
246: if (p_forceRebuild)
247: return rebuildSorts();
248: return this ;
249: }
250:
251: private SVInstantiations rebuildSorts() {
252: genericSortInstantiations = GenericSortInstantiations.create(
253: map.entryIterator(), getGenericSortConditions());
254: return this ;
255: }
256:
257: /**
258: * adds the given pair to the instantiations. If the given SchemaVariable
259: * has been instantiated already, the new pair is taken without a warning.
260: *
261: * @param sv
262: * the SchemaVariable to be instantiated
263: * @param entry
264: * the InstantiationEntry
265: * @return SVInstantiations the new SVInstantiations containing the given
266: * pair
267: */
268: public SVInstantiations add(SchemaVariable sv,
269: InstantiationEntry entry) {
270: return new SVInstantiations(map.put(sv, entry), interesting(),
271: getUpdateContext(), getGenericSortInstantiations(),
272: getGenericSortConditions()).checkSorts(entry, false);
273: }
274:
275: public SVInstantiations addInteresting(SchemaVariable sv,
276: InstantiationEntry entry) {
277: return new SVInstantiations(map.put(sv, entry), interesting()
278: .put(sv, entry), getUpdateContext(),
279: getGenericSortInstantiations(),
280: getGenericSortConditions()).checkSorts(entry, false);
281: }
282:
283: /**
284: * replaces the given pair in the instantiations. If the given
285: * SchemaVariable has been instantiated already, the new pair is taken
286: * without a warning.
287: *
288: * @param sv
289: * the SchemaVariable to be instantiated
290: * @param entry
291: * the InstantiationEntry the SchemaVariable is instantiated with
292: */
293: public SVInstantiations replace(SchemaVariable sv,
294: InstantiationEntry entry) {
295: return new SVInstantiations(map.remove(sv).put(sv, entry),
296: interesting(), getUpdateContext(),
297: getGenericSortConditions()).checkSorts(entry, true);
298: }
299:
300: /**
301: * adds the schemvariable to the set of interesting ones
302: * @throws IllegalInstantiationException, if sv has not yet been instantiated
303: */
304: public SVInstantiations makeInteresting(SchemaVariable sv) {
305: final InstantiationEntry entry = getInstantiationEntry(sv);
306:
307: if (entry == null) {
308: throw new IllegalInstantiationException(
309: sv
310: + " cannot be made interesting. As it is not yet in the map.");
311: }
312:
313: return new SVInstantiations(map, interesting().put(sv, entry),
314: getUpdateContext(), getGenericSortConditions())
315: .checkSorts(entry, true);
316:
317: }
318:
319: /**
320: * replaces the given pair in the instantiations. If the given
321: * SchemaVariable has been instantiated already, the new pair is taken
322: * without a warning.
323: *
324: * @param sv
325: * the SchemaVariable to be instantiated
326: * @param term
327: * the Term the SchemaVariable is instantiated with
328: */
329: public SVInstantiations replace(SchemaVariable sv, Term term) {
330: return replace(sv, new TermInstantiation(sv, term));
331: }
332:
333: /**
334: * replaces the given pair in the instantiations. If the given
335: * SchemaVariable has been instantiated already, the new pair is taken
336: * without a warning.
337: *
338: * @param sv
339: * the SchemaVariable to be instantiated
340: * @param pe
341: * the ProgramElement the SchemaVariable is instantiated with
342: */
343: public SVInstantiations replace(SchemaVariable sv, ProgramElement pe) {
344: return replace(sv, new ProgramInstantiation(sv, pe));
345: }
346:
347: /**
348: * replaces the given pair in the instantiations. If the given
349: * SchemaVariable has been instantiated already, the new pair is taken
350: * without a warning.
351: *
352: * @param sv
353: * the SchemaVariable to be instantiated
354: * @param pes
355: * the ArrayOfProgramElement the SchemaVariable is instantiated
356: * with
357: */
358: public SVInstantiations replace(SchemaVariable sv,
359: ArrayOfProgramElement pes) {
360: return replace(sv, new ProgramListInstantiation(sv, pes));
361: }
362:
363: /**
364: * replaces the given pair in the instantiations. If the context has been
365: * instantiated already, the new pair is taken without a warning.
366: *
367: * @param prefix
368: * the PosInProgram describing the position of the first
369: * statement after the prefix
370: * @param postfix
371: * the PosInProgram describing the position of the statement just
372: * before the postfix
373: * @param activeStatementContext
374: * the ExecutionContext of the first active statement
375: * @param pe
376: * the ProgramElement the context positions are related to
377: */
378: public SVInstantiations replace(PosInProgram prefix,
379: PosInProgram postfix,
380: ExecutionContext activeStatementContext, ProgramElement pe) {
381: return replace(CONTEXTSV, new ContextInstantiationEntry(
382: CONTEXTSV, prefix, postfix, activeStatementContext, pe));
383: }
384:
385: /**
386: * returns true iff the sv has been instantiated already
387: *
388: * @return true iff the sv has been instantiated already
389: */
390: public boolean isInstantiated(SchemaVariable sv) {
391: return map.containsKey(sv);
392: }
393:
394: /**
395: * returns the instantiation of the given SchemaVariable
396: *
397: * @return the InstantiationEntry the SchemaVariable will be instantiated
398: * with, null if no instantiation is stored
399: */
400: public InstantiationEntry getInstantiationEntry(SchemaVariable sv) {
401: return map.get(sv);
402: }
403:
404: /**
405: * returns the instantiation of the given SchemaVariable
406: *
407: * @return the Object the SchemaVariable will be instantiated with, null if
408: * no instantiation is stored
409: */
410: public Object getInstantiation(SchemaVariable sv) {
411: final InstantiationEntry entry = getInstantiationEntry(sv);
412: return entry == null ? null : entry.getInstantiation();
413: }
414:
415: /**
416: * returns the instantiation of the given SchemaVariable as Term. If the
417: * instantiation is a program element it is tried to convert it to a term
418: * otherwise an exception is thrown
419: *
420: * @return the Object the SchemaVariable will be instantiated with, null if
421: * no instantiation is stored
422: */
423: public Term getTermInstantiation(SchemaVariable sv,
424: ExecutionContext ec, Services services) {
425: final Object inst = getInstantiation(sv);
426: if (inst == null) {
427: return null;
428: } else if (inst instanceof Term) {
429: return (Term) inst;
430: } else if (inst instanceof ProgramElement) {
431: return services.getTypeConverter().convertToLogicElement(
432: (ProgramElement) inst, ec);
433: } else {
434: throw CONVERT_INSTANTIATION_EXCEPTION;
435: }
436: }
437:
438: /** adds an update to the update context */
439: public SVInstantiations addUpdate(Term update) {
440: return new SVInstantiations(map, interesting(), updateContext
441: .append(new UpdatePair(update)),
442: getGenericSortInstantiations(),
443: getGenericSortConditions());
444: }
445:
446: public SVInstantiations addUpdateList(ListOfUpdatePair updates) {
447: return new SVInstantiations(map, interesting(), updates,
448: getGenericSortInstantiations(),
449: getGenericSortConditions());
450: }
451:
452: public SVInstantiations clearUpdateContext() {
453: return new SVInstantiations(map, interesting(),
454: SLListOfUpdatePair.EMPTY_LIST,
455: getGenericSortInstantiations(),
456: getGenericSortConditions());
457: }
458:
459: /**
460: * returns the instantiation entry for the context "schema variable" or null
461: * if non such exists
462: */
463: public ContextInstantiationEntry getContextInstantiation() {
464: final InstantiationEntry entry = getInstantiationEntry(CONTEXTSV);
465: return (ContextInstantiationEntry) entry;
466: }
467:
468: /**
469: * returns iterator of the SchemaVariables that have an instantiation
470: *
471: * @return the IteratorOfSchemaVariable
472: */
473: public IteratorOfSchemaVariable svIterator() {
474: return map.keyIterator();
475: }
476:
477: /**
478: * returns iterator of the mapped pair (SchemaVariables, InstantiationEntry)
479: *
480: * @return the IteratorOfEntryOfSchemaVariableAndInstantiationEntry
481: */
482: public IteratorOfEntryOfSchemaVariableAndInstantiationEntry pairIterator() {
483: return map.entryIterator();
484: }
485:
486: /**
487: * returns the number of SchemaVariables of which an instantiation is known
488: *
489: * @return int that is the number of SchemaVariables of which an
490: * instantiation is known
491: */
492: public int size() {
493: return map.size();
494: }
495:
496: /**
497: * returns the update context
498: *
499: * @return the update context
500: */
501: public ListOfUpdatePair getUpdateContext() {
502: return updateContext;
503: }
504:
505: /**
506: * returns true if the given object and this one have the same mappings
507: *
508: * @return true if the given object and this one have the same mappings
509: */
510: public boolean equals(Object obj) {
511: final SVInstantiations cmp;
512: if (!(obj instanceof SVInstantiations)) {
513: return false;
514: } else {
515: cmp = (SVInstantiations) obj;
516: }
517: if (size() != cmp.size()
518: || !getUpdateContext().equals(cmp.getUpdateContext())) {
519: return false;
520: }
521:
522: final IteratorOfEntryOfSchemaVariableAndInstantiationEntry it = pairIterator();
523: while (it.hasNext()) {
524: final EntryOfSchemaVariableAndInstantiationEntry e = it
525: .next();
526: final Object inst = e.value().getInstantiation();
527: assert inst != null : "Illegal null instantiation.";
528: if (!inst.equals(cmp.getInstantiation(e.key()))) {
529: return false;
530: }
531: }
532: return true;
533:
534: }
535:
536: public int hashCode() {
537: if (hashcode == 0) {
538: int result = 37 * getUpdateContext().hashCode() + size();
539: final IteratorOfEntryOfSchemaVariableAndInstantiationEntry it = pairIterator();
540: while (it.hasNext()) {
541: final EntryOfSchemaVariableAndInstantiationEntry e = it
542: .next();
543: result = 37 * result
544: + e.value().getInstantiation().hashCode()
545: + e.key().hashCode();
546: }
547: hashcode = result == 0 ? 1 : result;
548: }
549: return hashcode;
550: }
551:
552: public SVInstantiations union(SVInstantiations other) {
553: MapFromSchemaVariableToInstantiationEntry result = map;
554:
555: final IteratorOfEntryOfSchemaVariableAndInstantiationEntry it = other.map
556: .entryIterator();
557:
558: while (it.hasNext()) {
559: final EntryOfSchemaVariableAndInstantiationEntry entry = it
560: .next();
561: result = result.put(entry.key(), entry.value());
562: }
563:
564: ListOfUpdatePair updates = SLListOfUpdatePair.EMPTY_LIST;
565:
566: if (other.getUpdateContext() == SLListOfUpdatePair.EMPTY_LIST) {
567: updates = getUpdateContext();
568: } else if (getUpdateContext() == SLListOfUpdatePair.EMPTY_LIST) {
569: updates = other.getUpdateContext();
570: } else if (!getUpdateContext().equals(other.getUpdateContext())) {
571: Debug.fail("The update context of one of"
572: + " the instantiations has to be empty or equal.");
573: } else {
574: updates = other.getUpdateContext();
575: }
576: return new SVInstantiations(result, interesting(), updates,
577: getGenericSortConditions()).rebuildSorts();
578: }
579:
580: public MapFromSchemaVariableToInstantiationEntry interesting() {
581: return interesting;
582: }
583:
584: /** toString */
585: public String toString() {
586: StringBuffer result = new StringBuffer("SV Instantiations: ");
587: return (result.append(map.toString())).toString();
588: }
589:
590: /**
591: * Add the given additional condition for the generic sort instantiations
592: */
593: public SVInstantiations add(GenericSortCondition p_c)
594: throws SortException {
595: return new SVInstantiations(map, interesting(),
596: getUpdateContext(), getGenericSortInstantiations(),
597: getGenericSortConditions().prepend(p_c))
598: .checkCondition(p_c, false);
599: }
600:
601: public ExecutionContext getExecutionContext() {
602: final ContextInstantiationEntry cte = getContextInstantiation();
603: if (cte != null) {
604: return cte.activeStatementContext();
605: } else {
606: return null;
607: }
608: }
609:
610: public EntryOfSchemaVariableAndInstantiationEntry lookupEntryForSV(
611: Name name) {
612: final IteratorOfEntryOfSchemaVariableAndInstantiationEntry it = map
613: .entryIterator();
614: while (it.hasNext()) {
615: final EntryOfSchemaVariableAndInstantiationEntry e = it
616: .next();
617: if (e.key().name().equals(name))
618: return e;
619: }
620: return null; // handle this better!
621: }
622:
623: public SchemaVariable lookupVar(Name name) {
624: final EntryOfSchemaVariableAndInstantiationEntry e = lookupEntryForSV(name);
625: return e == null ? null : e.key(); // handle this better!
626: }
627:
628: public Object lookupValue(Name name) {
629: final EntryOfSchemaVariableAndInstantiationEntry e = lookupEntryForSV(name);
630: return e == null ? null : e.value().getInstantiation();
631: }
632:
633: }
|