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.strategy;
012:
013: import java.util.HashMap;
014:
015: import de.uka.ilkd.key.java.Services;
016: import de.uka.ilkd.key.logic.*;
017: import de.uka.ilkd.key.logic.op.IteratorOfSchemaVariable;
018: import de.uka.ilkd.key.logic.op.SchemaVariable;
019: import de.uka.ilkd.key.logic.op.SetOfSchemaVariable;
020: import de.uka.ilkd.key.proof.*;
021: import de.uka.ilkd.key.rule.*;
022: import de.uka.ilkd.key.util.Debug;
023:
024: /**
025: * Instances of this class are immutable
026: */
027: public abstract class TacletAppContainer extends RuleAppContainer {
028:
029: private final long age;
030:
031: protected TacletAppContainer(RuleApp p_app, RuleAppCost p_cost,
032: long p_age) {
033: super (p_app, p_cost);
034: age = p_age;
035: }
036:
037: protected NoPosTacletApp getTacletApp() {
038: return (NoPosTacletApp) getRuleApp();
039: }
040:
041: public long getAge() {
042: return age;
043: }
044:
045: private ListOfTacletApp incMatchIfFormulas(Goal p_goal) {
046: final IfInstantiator instantiator = new IfInstantiator(p_goal);
047: instantiator.findIfFormulaInstantiations();
048: return instantiator.getResults();
049: }
050:
051: protected static TacletAppContainer createContainer(RuleApp p_app,
052: PosInOccurrence p_pio, Goal p_goal, Strategy p_strategy,
053: boolean p_initial) {
054: return createContainer(p_app, p_pio, p_goal, p_strategy
055: .computeCost(p_app, p_pio, p_goal), p_initial);
056: }
057:
058: private static TacletAppContainer createContainer(RuleApp p_app,
059: PosInOccurrence p_pio, Goal p_goal, RuleAppCost p_cost,
060: boolean p_initial) {
061: // This relies on the fact that the method <code>Goal.getTime()</code>
062: // never returns a value less than zero
063: final long localage = p_initial ? -1 : p_goal.getTime();
064: if (p_pio == null)
065: return new NoFindTacletAppContainer(p_app, p_cost, localage);
066: else
067: return new FindTacletAppContainer(p_app, p_pio, p_cost,
068: p_goal, localage);
069: }
070:
071: /**
072: * Create a list of new RuleAppContainers that are to be
073: * considered for application.
074: */
075: public ListOfRuleAppContainer createFurtherApps(Goal p_goal,
076: Strategy p_strategy) {
077: if (!isStillApplicable(p_goal)
078: || getTacletApp().ifInstsComplete()
079: && !ifFormulasStillValid(p_goal))
080: return SLListOfRuleAppContainer.EMPTY_LIST;
081:
082: final TacletAppContainer newCont = createContainer(p_goal,
083: p_strategy);
084: if (newCont.getCost() instanceof TopRuleAppCost)
085: return SLListOfRuleAppContainer.EMPTY_LIST;
086:
087: ListOfRuleAppContainer res = SLListOfRuleAppContainer.EMPTY_LIST
088: .prepend(newCont);
089:
090: if (getTacletApp().ifInstsComplete()) {
091: res = addInstances(getTacletApp(), res, p_goal, p_strategy);
092: } else {
093: final IteratorOfTacletApp it = incMatchIfFormulas(p_goal)
094: .iterator();
095: while (it.hasNext()) {
096: final TacletApp app = it.next();
097: res = addContainer(app, res, p_goal, p_strategy);
098: res = addInstances(app, res, p_goal, p_strategy);
099: }
100: }
101:
102: return res;
103: }
104:
105: /**
106: * Add all instances of the given taclet app (that are possibly produced
107: * using method <code>instantiateApp</code> of the strategy) to
108: * <code>targetList</code>
109: */
110: private ListOfRuleAppContainer addInstances(TacletApp app,
111: ListOfRuleAppContainer targetList, Goal p_goal,
112: Strategy p_strategy) {
113: if (app.uninstantiatedVars().size() == 0)
114: return targetList;
115: return instantiateApp(app, targetList, p_goal, p_strategy);
116: }
117:
118: /**
119: * Use the method <code>instantiateApp</code> of the strategy for choosing
120: * the values of schema variables that have not been instantiated so far
121: */
122: private ListOfRuleAppContainer instantiateApp(TacletApp app,
123: ListOfRuleAppContainer targetList, final Goal p_goal,
124: Strategy p_strategy) {
125: // just for being able to modify the result-list in an
126: // anonymous class
127: final ListOfRuleAppContainer[] resA = new ListOfRuleAppContainer[] { targetList };
128:
129: final RuleAppCostCollector collector = new RuleAppCostCollector() {
130: public void collect(RuleApp newApp, RuleAppCost cost) {
131: if (cost instanceof TopRuleAppCost)
132: return;
133: resA[0] = addContainer((TacletApp) newApp, resA[0],
134: p_goal, cost);
135: }
136: };
137: p_strategy.instantiateApp(app, getPosInOccurrence(p_goal),
138: p_goal, collector);
139:
140: return resA[0];
141: }
142:
143: /**
144: * Create a container object for the given taclet app, provided that the app
145: * is <code>sufficientlyComplete</code>, and add the container to
146: * <code>targetList</code>
147: */
148: private ListOfRuleAppContainer addContainer(TacletApp app,
149: ListOfRuleAppContainer targetList, Goal p_goal,
150: Strategy p_strategy) {
151: return targetList.prepend(TacletAppContainer.createContainer(
152: app, getPosInOccurrence(p_goal), p_goal, p_strategy,
153: false));
154: }
155:
156: /**
157: * Create a container object for the given taclet app, provided that the app
158: * is <code>sufficientlyComplete</code>, and add the container to
159: * <code>targetList</code>
160: */
161: private ListOfRuleAppContainer addContainer(TacletApp app,
162: ListOfRuleAppContainer targetList, Goal p_goal,
163: RuleAppCost cost) {
164: if (!sufficientlyCompleteApp(app))
165: return targetList;
166: return targetList.prepend(TacletAppContainer.createContainer(
167: app, getPosInOccurrence(p_goal), p_goal, cost, false));
168: }
169:
170: private boolean sufficientlyCompleteApp(TacletApp app) {
171: final SetOfSchemaVariable needed = app
172: .neededUninstantiatedVars();
173: if (needed.size() == 0)
174: return true;
175: final IteratorOfSchemaVariable it = needed.iterator();
176: while (it.hasNext()) {
177: final SchemaVariable sv = it.next();
178: if (sv.isSkolemTermSV())
179: continue;
180: return false;
181: }
182: return true;
183: }
184:
185: private TacletAppContainer createContainer(Goal p_goal,
186: Strategy p_strategy) {
187: return createContainer(getTacletApp(),
188: getPosInOccurrence(p_goal), p_goal, p_strategy, false);
189: }
190:
191: /**
192: * Create containers for NoFindTaclets.
193: */
194: static ListOfRuleAppContainer createAppContainers(
195: NoPosTacletApp p_app, Goal p_goal, Strategy p_strategy) {
196: return createAppContainers(p_app, null, p_goal, p_strategy);
197: }
198:
199: /**
200: * Create containers for FindTaclets or NoFindTaclets.
201: * @param p_app if <code>p_pio</code> is null, <code>p_app</code> has to be
202: * a <code>TacletApp</code> for a <code>NoFindTaclet</code>,
203: * otherwise for a <code>FindTaclet</code>.
204: * @return list of containers for currently applicable TacletApps, the cost
205: * may be an instance of <code>TopRuleAppCost</code>.
206: */
207: static ListOfRuleAppContainer createAppContainers(
208: NoPosTacletApp p_app, PosInOccurrence p_pio, Goal p_goal,
209: Strategy p_strategy) {
210: if (!(p_pio == null ? p_app.taclet() instanceof NoFindTaclet
211: : p_app.taclet() instanceof FindTaclet))
212: // faster than <code>assertTrue</code>
213: Debug.fail("Wrong type of taclet " + p_app.taclet());
214:
215: // Create an initial container for the given taclet; the if-formulas of
216: // the taclet are only matched lazy (by <code>createFurtherApps()</code>
217: return SLListOfRuleAppContainer.EMPTY_LIST
218: .prepend(createContainer(p_app, p_pio, p_goal,
219: p_strategy, true));
220: }
221:
222: /**
223: * @return true iff instantiation of the if-formulas of the stored taclet
224: * app exist and are valid are still valid, i.e. the referenced formulas
225: * still exist
226: */
227: protected boolean ifFormulasStillValid(Goal p_goal) {
228: if (getTacletApp().taclet().ifSequent().isEmpty())
229: return true;
230: if (!getTacletApp().ifInstsComplete())
231: return false;
232:
233: final IteratorOfIfFormulaInstantiation it = getTacletApp()
234: .ifFormulaInstantiations().iterator();
235: final Sequent seq = p_goal.sequent();
236:
237: while (it.hasNext()) {
238: final IfFormulaInstantiation ifInst2 = it.next();
239: if (!(ifInst2 instanceof IfFormulaInstSeq))
240: // faster than assertTrue
241: Debug.fail("Don't know what to do with the "
242: + "if-instantiation " + ifInst2);
243: final IfFormulaInstSeq ifInst = (IfFormulaInstSeq) ifInst2;
244: if (!(ifInst.inAntec() ? seq.antecedent() : seq.succedent())
245: .contains(ifInst.getConstrainedFormula()))
246: return false;
247: }
248:
249: return true;
250: }
251:
252: /**
253: * @return true iff the stored rule app is applicable for the given sequent,
254: * i.e. if the find-position does still exist (if-formulas are not
255: * considered)
256: */
257: protected abstract boolean isStillApplicable(Goal p_goal);
258:
259: protected PosInOccurrence getPosInOccurrence(Goal p_goal) {
260: return null;
261: }
262:
263: /**
264: * Create a <code>RuleApp</code> that is suitable to be applied
265: * or <code>null</code>.
266: */
267: public RuleApp completeRuleApp(Goal p_goal, Strategy strategy) {
268: if (!isStillApplicable(p_goal))
269: return null;
270:
271: if (!ifFormulasStillValid(p_goal))
272: return null;
273:
274: TacletApp app = getTacletApp();
275:
276: final PosInOccurrence pio = getPosInOccurrence(p_goal);
277: if (!strategy.isApprovedApp(app, pio, p_goal))
278: return null;
279:
280: if (pio != null) {
281: app = app.setPosInOccurrence(pio);
282: if (app == null)
283: return null;
284: }
285:
286: if (!app.complete())
287: app = app.tryToInstantiate(p_goal, p_goal.proof()
288: .getServices());
289:
290: return app;
291: }
292:
293: /**
294: * This class implements custom instantiation of if-formulas.
295: */
296: private class IfInstantiator {
297: private final Goal goal;
298:
299: private ListOfIfFormulaInstantiation allAntecFormulas;
300: private ListOfIfFormulaInstantiation allSuccFormulas;
301:
302: private ListOfTacletApp results = SLListOfTacletApp.EMPTY_LIST;
303:
304: IfInstantiator(final Goal goal) {
305: this .goal = goal;
306: }
307:
308: private void addResult(TacletApp app) {
309: if (app == null)
310: return;
311: results = results.prepend(app);
312: /*
313: final RuleAppContainer cont =
314: TacletAppContainer.createContainer ( app,
315: getPosInOccurrence ( goal ),
316: goal,
317: strategy,
318: false );
319: results = results.prepend ( cont );
320: */
321: }
322:
323: /**
324: * Find all possible instantiations of the if sequent formulas
325: * within the sequent "p_seq".
326: * @return a list of tacletapps with the found if formula
327: * instantiations
328: */
329: public void findIfFormulaInstantiations() {
330: final Sequent p_seq = goal.sequent();
331:
332: Debug.assertTrue(
333: getTacletApp().ifFormulaInstantiations() == null,
334: "The if formulas have already been instantiated");
335:
336: if (getTaclet().ifSequent() == Sequent.EMPTY_SEQUENT)
337: addResult(getTacletApp());
338: else {
339: allAntecFormulas = IfFormulaInstSeq.createList(p_seq,
340: true);
341: allSuccFormulas = IfFormulaInstSeq.createList(p_seq,
342: false);
343: findIfFormulaInstantiationsHelp(
344: createSemisequentList(getTaclet().ifSequent() // Matching starting
345: .succedent()), // with the last formula
346: createSemisequentList(getTaclet().ifSequent()
347: .antecedent()),
348: SLListOfIfFormulaInstantiation.EMPTY_LIST,
349: getTacletApp().matchConditions(), false);
350: }
351: }
352:
353: private Taclet getTaclet() {
354: return getTacletApp().taclet();
355: }
356:
357: /**
358: * @param p_all
359: * if true then return all formulas of the particular
360: * semisequent, otherwise only the formulas returned by
361: * <code>selectNewFormulas</code>
362: * @return a list of potential if-formula instantiations (analogously to
363: * <code>IfFormulaInstSeq.createList</code>)
364: */
365: private ListOfIfFormulaInstantiation getSequentFormulas(
366: boolean p_antec, boolean p_all) {
367: if (p_all)
368: return getAllSequentFormulas(p_antec);
369:
370: final ListOfIfFormulaInstantiation cache = getNewSequentFormulasFromCache(p_antec);
371: if (cache != null)
372: return cache;
373:
374: final ListOfIfFormulaInstantiation newFormulas = selectNewFormulas(p_antec);
375:
376: addNewSequentFormulasToCache(newFormulas, p_antec);
377:
378: return newFormulas;
379: }
380:
381: /**
382: * @return a list of potential if-formula instantiations (analogously to
383: * <code>IfFormulaInstSeq.createList</code>), but consisting
384: * only of those formulas of the current goal for which the
385: * method <code>isNewFormula</code> returns <code>true</code>
386: */
387: private ListOfIfFormulaInstantiation selectNewFormulas(
388: boolean p_antec) {
389: final IteratorOfIfFormulaInstantiation it = getAllSequentFormulas(
390: p_antec).iterator();
391: ListOfIfFormulaInstantiation res = SLListOfIfFormulaInstantiation.EMPTY_LIST;
392:
393: while (it.hasNext()) {
394: final IfFormulaInstantiation ifInstantiation = it
395: .next();
396: if (isNewFormulaDirect(ifInstantiation))
397: res = res.prepend(ifInstantiation);
398: }
399:
400: return res;
401: }
402:
403: /**
404: * @return true iff the formula described by the argument has been
405: * modified (or introduced) since the latest point of time when
406: * the if-formulas of the enclosing taclet app (container) have
407: * been matched
408: */
409: private boolean isNewFormula(
410: IfFormulaInstantiation p_ifInstantiation) {
411: final boolean antec = ((IfFormulaInstSeq) p_ifInstantiation)
412: .inAntec();
413:
414: final ListOfIfFormulaInstantiation cache = getNewSequentFormulasFromCache(antec);
415:
416: if (cache != null)
417: return cache.contains(p_ifInstantiation);
418:
419: return isNewFormulaDirect(p_ifInstantiation);
420: }
421:
422: /**
423: * @return true iff the formula described by the argument has been
424: * modified (or introduced) since the latest point of time when
425: * the if-formulas of the enclosing taclet app (container) have
426: * been matched (this method does not use the cache)
427: */
428: private boolean isNewFormulaDirect(
429: IfFormulaInstantiation p_ifInstantiation) {
430: final boolean antec = ((IfFormulaInstSeq) p_ifInstantiation)
431: .inAntec();
432:
433: final ConstrainedFormula cfma = p_ifInstantiation
434: .getConstrainedFormula();
435: final PosInOccurrence pio = new PosInOccurrence(cfma,
436: PosInTerm.TOP_LEVEL, antec);
437:
438: final FormulaTagManager tagManager = goal
439: .getFormulaTagManager();
440:
441: final FormulaTag tag = tagManager.getTagForPos(pio);
442: final long formulaAge = tagManager.getAgeForTag(tag);
443:
444: // The strict relation can be used, because when applying a rule the
445: // age of a goal is increased before the actual modification of the
446: // goal take place
447: return getAge() < formulaAge;
448: }
449:
450: private ListOfIfFormulaInstantiation getNewSequentFormulasFromCache(
451: boolean p_antec) {
452: synchronized (ifInstCache) {
453: if (ifInstCache.cacheKey != goal.node())
454: return null;
455:
456: // the cache contains formula lists for the right semisequent
457: return (ListOfIfFormulaInstantiation) getCacheMap(
458: p_antec).get(getAgeObject());
459: }
460: }
461:
462: private void addNewSequentFormulasToCache(
463: ListOfIfFormulaInstantiation p_list, boolean p_antec) {
464: synchronized (ifInstCache) {
465: if (ifInstCache.cacheKey != goal.node()) {
466: ifInstCache.cacheKey = goal.node();
467: ifInstCache.antecCache.clear();
468: ifInstCache.succCache.clear();
469: }
470:
471: getCacheMap(p_antec).put(getAgeObject(), p_list);
472: }
473: }
474:
475: private HashMap getCacheMap(boolean p_antec) {
476: return p_antec ? ifInstCache.antecCache
477: : ifInstCache.succCache;
478: }
479:
480: private Long getAgeObject() {
481: return new Long(getAge());
482: }
483:
484: private ListOfIfFormulaInstantiation getAllSequentFormulas(
485: boolean p_antec) {
486: return p_antec ? allAntecFormulas : allSuccFormulas;
487: }
488:
489: /**
490: * Recursive function for matching the remaining tail of an if sequent
491: *
492: * @param p_ifSeqTail
493: * tail of the current semisequent as list
494: * @param p_ifSeqTail2nd
495: * the following semisequent (i.e. antecedent) or null
496: * @param p_matchCond
497: * match conditions until now, i.e. after matching the first
498: * formulas of the if sequent
499: * @param p_alreadyMatchedNewFor
500: * at least one new formula has already been matched, i.e. a
501: * formula that has been modified recently
502: * @param p_toMatch
503: * list of the formulas to match the current if semisequent
504: * formulas with
505: * @param p_toMatch2nd
506: * list of the formulas of the antecedent
507: */
508: private void findIfFormulaInstantiationsHelp(
509: ListOfConstrainedFormula p_ifSeqTail,
510: ListOfConstrainedFormula p_ifSeqTail2nd,
511: ListOfIfFormulaInstantiation p_alreadyMatched,
512: MatchConditions p_matchCond,
513: boolean p_alreadyMatchedNewFor) {
514:
515: while (p_ifSeqTail.isEmpty()) {
516: if (p_ifSeqTail2nd == null) {
517: // All formulas have been matched, collect the results
518: addResult(setAllInstantiations(p_matchCond,
519: p_alreadyMatched));
520: return;
521: } else {
522: // Change from succedent to antecedent
523: p_ifSeqTail = p_ifSeqTail2nd;
524: p_ifSeqTail2nd = null;
525: }
526: }
527:
528: // Match the current formula
529: final boolean antec = p_ifSeqTail2nd == null;
530: final boolean lastIfFormula = p_ifSeqTail.size() == 1
531: && (p_ifSeqTail2nd == null || p_ifSeqTail2nd
532: .isEmpty());
533: final ListOfIfFormulaInstantiation formulas = getSequentFormulas(
534: antec, !lastIfFormula || p_alreadyMatchedNewFor);
535: final IfMatchResult mr = getTaclet().matchIf(
536: formulas.iterator(), p_ifSeqTail.head().formula(),
537: p_matchCond, getServices(), getUserConstraint());
538:
539: // For each matching formula call the method again to match
540: // the remaining terms
541: IteratorOfIfFormulaInstantiation itCand = mr.getFormulas()
542: .iterator();
543: IteratorOfMatchConditions itMC = mr.getMatchConditions()
544: .iterator();
545: p_ifSeqTail = p_ifSeqTail.tail();
546: while (itCand.hasNext()) {
547: final IfFormulaInstantiation ifInstantiation = itCand
548: .next();
549: final boolean nextAlreadyMatchedNewFor = lastIfFormula
550: || p_alreadyMatchedNewFor
551: || isNewFormula(ifInstantiation);
552: findIfFormulaInstantiationsHelp(p_ifSeqTail,
553: p_ifSeqTail2nd, p_alreadyMatched
554: .prepend(ifInstantiation), itMC.next(),
555: nextAlreadyMatchedNewFor);
556: }
557: }
558:
559: private Constraint getUserConstraint() {
560: return getProof().getUserConstraint().getConstraint();
561: }
562:
563: private Proof getProof() {
564: return goal.proof();
565: }
566:
567: private Services getServices() {
568: return getProof().getServices();
569: }
570:
571: private NoPosTacletApp setAllInstantiations(
572: MatchConditions p_matchCond,
573: ListOfIfFormulaInstantiation p_alreadyMatched) {
574: return NoPosTacletApp.createNoPosTacletApp(getTaclet(),
575: p_matchCond.getInstantiations(), p_matchCond
576: .getConstraint(), p_matchCond
577: .getNewMetavariables(), p_alreadyMatched);
578: }
579:
580: private ListOfConstrainedFormula createSemisequentList(
581: Semisequent p_ss) {
582: ListOfConstrainedFormula res = SLListOfConstrainedFormula.EMPTY_LIST;
583:
584: IteratorOfConstrainedFormula it = p_ss.iterator();
585: while (it.hasNext())
586: res = res.prepend(it.next());
587:
588: return res;
589: }
590:
591: /**
592: * @return Returns the results.
593: */
594: public ListOfTacletApp getResults() {
595: return results;
596: }
597: }
598:
599: /**
600: * Direct-mapped cache of lists of formulas (potential instantiations of
601: * if-formulas of taclets) that were modified after a certain point of time
602: */
603:
604: /**
605: * Hashmaps of the particular lists of formulas; the keys of the maps
606: * is the point of time that separates old from new (modified) formulas
607: *
608: * Keys: Long Values: ListOfIfFormulaInstantiation
609: */
610: protected static final class IfInstCache {
611: public Node cacheKey = null;
612:
613: public final HashMap antecCache = new HashMap();
614: public final HashMap succCache = new HashMap();
615: }
616:
617: protected static final IfInstCache ifInstCache = new IfInstCache();
618: }
|