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.PIOPathIterator;
014: import de.uka.ilkd.key.logic.PosInOccurrence;
015: import de.uka.ilkd.key.proof.FormulaTag;
016: import de.uka.ilkd.key.proof.Goal;
017: import de.uka.ilkd.key.rule.RuleApp;
018:
019: /**
020: * A rule app manager that ensures that rules are only applied to a certain
021: * subterm within the proof (within a goal). The real work is delegated to a
022: * second manager (delegate pattern), this class only filters rule applications
023: */
024: public class FocussedRuleApplicationManager implements
025: AutomatedRuleApplicationManager {
026:
027: private final AutomatedRuleApplicationManager delegate;
028:
029: private final FormulaTag focussedFormula;
030: private final PosInOccurrence focussedSubterm;
031:
032: private Goal goal;
033:
034: // Until <code>next</code> was called for the first time only rule
035: // applications for the focussed formula are accepted, after that also
036: // applications for other formulas. The idea is that then the rule index
037: // caches are filled and further reported rules involve modified or new
038: // formulas (this works at least for delegate
039: // <code>QueueRuleApplicationManager</code>)
040: private boolean onlyModifyFocussedFormula;
041:
042: private FocussedRuleApplicationManager(
043: AutomatedRuleApplicationManager delegate, Goal goal,
044: FormulaTag focussedFormula,
045: PosInOccurrence focussedSubterm,
046: boolean onlyModifyFocussedFormula) {
047: this .delegate = delegate;
048: this .focussedFormula = focussedFormula;
049: this .focussedSubterm = focussedSubterm;
050: this .goal = goal;
051: this .onlyModifyFocussedFormula = onlyModifyFocussedFormula;
052: }
053:
054: public FocussedRuleApplicationManager(
055: AutomatedRuleApplicationManager delegate, Goal goal,
056: PosInOccurrence focussedSubterm) {
057: this (delegate, goal, goal.getFormulaTagManager().getTagForPos(
058: focussedSubterm.topLevel()), focussedSubterm, true);
059:
060: clearCache();
061: }
062:
063: public void clearCache() {
064: delegate.clearCache();
065: }
066:
067: public AutomatedRuleApplicationManager copy() {
068: return (AutomatedRuleApplicationManager) clone();
069: }
070:
071: public Object clone() {
072: return new FocussedRuleApplicationManager(delegate.copy(),
073: null, focussedFormula, focussedSubterm,
074: onlyModifyFocussedFormula);
075: }
076:
077: public RuleApp peekNext() {
078: return delegate.peekNext();
079: }
080:
081: public RuleApp next() {
082: final RuleApp app = delegate.next();
083: onlyModifyFocussedFormula = false;
084: return app;
085: }
086:
087: public void setGoal(Goal p_goal) {
088: goal = p_goal;
089: delegate.setGoal(p_goal);
090: }
091:
092: public void ruleAdded(RuleApp rule, PosInOccurrence pos) {
093: // filter the rule applications, only allow applications within the
094: // focussed subterm or to other formulas that have been added after creation
095: // of the manager (we rely on the fact that the caching rule indexes only
096: // report rules for modified/added formulas anyway)
097:
098: final PosInOccurrence focFormula = getPIOForFocussedSubterm();
099:
100: if (focFormula != null && pos != null) {
101: if (isSameFormula(pos, focFormula)) {
102: if (!isBelow(focFormula, pos))
103: // rule app within the focussed formula, but not within the
104: // focussed subterm
105: return;
106: } else {
107: if (onlyModifyFocussedFormula)
108: return;
109: }
110: } else if (onlyModifyFocussedFormula) {
111: return;
112: }
113:
114: delegate.ruleAdded(rule, pos);
115: }
116:
117: private boolean isSameFormula(PosInOccurrence pio1,
118: PosInOccurrence pio2) {
119: return pio2.isInAntec() == pio1.isInAntec()
120: && pio2.constrainedFormula().equals(
121: pio1.constrainedFormula());
122: }
123:
124: private PosInOccurrence getPIOForFocussedSubterm() {
125: final PosInOccurrence formula = goal.getFormulaTagManager()
126: .getPosForTag(focussedFormula);
127:
128: if (formula == null)
129: return null;
130:
131: return focussedSubterm.replaceConstrainedFormula(formula
132: .constrainedFormula());
133: }
134:
135: private boolean isBelow(PosInOccurrence over, PosInOccurrence under) {
136: final PIOPathIterator overIt = over.iterator();
137: final PIOPathIterator underIt = under.iterator();
138:
139: while (true) {
140: final int overChild = overIt.next();
141: final int underChild = underIt.next();
142: if (overChild == -1)
143: return true;
144: if (overChild != underChild)
145: return false;
146: }
147: }
148:
149: public AutomatedRuleApplicationManager getDelegate() {
150: return delegate;
151: }
152: }
|