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 de.uka.ilkd.key.logic.ConstrainedFormula;
014: import de.uka.ilkd.key.logic.FormulaChangeInfo;
015: import de.uka.ilkd.key.logic.ListOfFormulaChangeInfo;
016: import de.uka.ilkd.key.logic.PIOPathIterator;
017: import de.uka.ilkd.key.logic.PosInOccurrence;
018: import de.uka.ilkd.key.logic.Term;
019: import de.uka.ilkd.key.logic.op.IUpdateOperator;
020: import de.uka.ilkd.key.logic.op.Modality;
021: import de.uka.ilkd.key.logic.op.Operator;
022: import de.uka.ilkd.key.proof.FormulaTag;
023: import de.uka.ilkd.key.proof.Goal;
024: import de.uka.ilkd.key.rule.RuleApp;
025: import de.uka.ilkd.key.util.Debug;
026:
027: /**
028: * Instances of this class are immutable
029: */
030: public class FindTacletAppContainer extends TacletAppContainer {
031:
032: /**
033: * The position of the rule app in two different representations:
034: * <code>positionTag</code> denotes the concerned formula and survives
035: * modifications of the sequent and of parts of the formula, and
036: * <code>applicationPosition</code> is the original position for which the
037: * rule app was created
038: */
039: private final FormulaTag positionTag;
040: private final PosInOccurrence applicationPosition;
041:
042: FindTacletAppContainer(RuleApp p_app, PosInOccurrence p_pio,
043: RuleAppCost p_cost, Goal p_goal, long p_age) {
044: super (p_app, p_cost, p_age);
045: applicationPosition = p_pio;
046: positionTag = p_goal.getFormulaTagManager().getTagForPos(
047: p_pio.topLevel());
048:
049: if (positionTag == null)
050: // faster than <code>assertFalse</code>
051: Debug.fail("Formula " + p_pio + " does not exist");
052: }
053:
054: /**
055: * @return true iff the stored rule app is applicable for the given sequent,
056: * i.e. if the find-position does still exist (if-formulas are not
057: * considered)
058: */
059: protected boolean isStillApplicable(Goal p_goal) {
060: final PosInOccurrence topPos = p_goal.getFormulaTagManager()
061: .getPosForTag(positionTag);
062: if (topPos == null)
063: // the formula does not exist anymore, bail out
064: return false;
065: if (!topPos.constrainedFormula().constraint().equals(
066: applicationPosition.constrainedFormula().constraint()))
067: // the constraint of the formula has changed, bail out
068: return false;
069: if (subformulaOrPreceedingUpdateHasChanged(p_goal))
070: return false;
071: if (!p_goal.proof().mgt().ruleApplicable(getRuleApp(), p_goal)) {
072: return false;
073: }
074: return true;
075: }
076:
077: /**
078: * @return true iff a subformula that contains the find position stored by
079: * this object has been altered since the creation of this object or if a
080: * preceeding update has changed
081: */
082: private boolean subformulaOrPreceedingUpdateHasChanged(Goal p_goal) {
083: ListOfFormulaChangeInfo infoList = p_goal
084: .getFormulaTagManager().getModifications(positionTag);
085:
086: while (!infoList.isEmpty()) {
087: final FormulaChangeInfo info = infoList.head();
088: infoList = infoList.tail();
089:
090: final ConstrainedFormula newFormula = info.getNewFormula();
091: if (newFormula == applicationPosition.constrainedFormula())
092: // then there were no relevant modifications since the creation
093: // of the rule app object
094: return false;
095:
096: if (!independentSubformulas(info
097: .getPositionOfModification(), newFormula))
098: return true;
099: }
100:
101: return false;
102: }
103:
104: /**
105: * checks if the modification path and the postition where this taclet application
106: * has been matched again denote independant subformulas. The modification affects
107: * a formula <code>F</code> if <code>F</code> is a subformula of the modified one
108: * or the modification took part inside an update which may occur in the update
109: * prefix instantiation of the taclet application
110: * @return true iff <code>applicationPosition</code> is in the scope of
111: * the position <code>p_pos</code> (the formulas are not compared, only the
112: * positions within the formulas) and no indirect relationship exists which
113: * is established by a modification that occurred inside an update
114: */
115: private boolean independentSubformulas(PosInOccurrence changePos,
116: ConstrainedFormula newFormula) {
117: final PIOPathIterator changePIO = changePos.iterator();
118: final PIOPathIterator appPIO = applicationPosition.iterator();
119:
120: while (true) {
121: final int changeIndex = changePIO.next();
122: final int appIndex = appPIO.next();
123:
124: if (appIndex == -1)
125: return false;
126:
127: if (changeIndex == -1) {
128: final Term beforeChangeTerm = changePIO.getSubTerm();
129: final Operator beforeChangeOp = beforeChangeTerm.op();
130:
131: // special case: a taclet application is not affected by changes
132: // to a preceding program, as long as the post-condition of the
133: // program does not change. this is a pretty common situation
134: // during symbolic program execution; also consider
135: // <code>TermTacletAppIndex.updateCompleteRebuild</code>
136: if (beforeChangeOp instanceof Modality) {
137: final PosInOccurrence afterChangePos = changePos
138: .replaceConstrainedFormula(newFormula);
139: final Term afterChangeTerm = afterChangePos
140: .subTerm();
141: return beforeChangeOp == afterChangeTerm.op()
142: && beforeChangeTerm.sub(0).equals(
143: afterChangeTerm.sub(0));
144: }
145:
146: return false;
147: }
148:
149: if (changeIndex != appIndex) {
150: // in case a change within an update occurred, also (some)
151: // taclets within the update target expression have to be
152: // invalidated
153: final Operator modOp = changePIO.getSubTerm().op();
154:
155: return !(modOp instanceof IUpdateOperator
156: && appIndex == ((IUpdateOperator) modOp)
157: .targetPos() && updateContextIsRecorded());
158: }
159: }
160: }
161:
162: /**
163: * @return <code>true</code> iff the update context (updates above the
164: * application position) is relevant and stored for this taclet app.
165: * In this case, the taclet app has to be discarded as soon as the
166: * update context changes
167: */
168: private boolean updateContextIsRecorded() {
169: return !getTacletApp().instantiations().getUpdateContext()
170: .isEmpty();
171: }
172:
173: /**
174: * @return non-null for FindTaclets
175: */
176: protected PosInOccurrence getPosInOccurrence(Goal p_goal) {
177: final PosInOccurrence topPos = p_goal.getFormulaTagManager()
178: .getPosForTag(positionTag);
179:
180: assert topPos != null;
181:
182: return applicationPosition.replaceConstrainedFormula(topPos
183: .constrainedFormula());
184: }
185:
186: }
|