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.proof;
012:
013: import de.uka.ilkd.key.logic.*;
014: import de.uka.ilkd.key.rule.*;
015:
016: public class BuiltInRuleAppIndex implements java.io.Serializable {
017:
018: private BuiltInRuleIndex index;
019:
020: private NewRuleListener newRuleListener = NullNewRuleListener.INSTANCE;
021:
022: private SimplifyIntegerRule simplify = null;
023:
024: public BuiltInRuleAppIndex(BuiltInRuleIndex index) {
025: this .index = index;
026: }
027:
028: public BuiltInRuleAppIndex(BuiltInRuleIndex index,
029: NewRuleListener p_newRuleListener) {
030: this .index = index;
031: this .newRuleListener = p_newRuleListener;
032: }
033:
034: /**
035: * returns a list of built-in rules application applicable
036: * for the given goal and position
037: */
038: public ListOfRuleApp getBuiltInRule(Goal goal, PosInOccurrence pos,
039: Constraint userConstraint) {
040:
041: ListOfRuleApp result = SLListOfRuleApp.EMPTY_LIST;
042: IteratorOfBuiltInRule it = index.rules().iterator();
043:
044: while (it.hasNext()) {
045: BuiltInRule bir = it.next();
046: if (bir.isApplicable(goal, pos, userConstraint)) {
047: RuleApp app = new BuiltInRuleApp(bir, pos,
048: userConstraint);
049: if (goal.proof().mgt().ruleApplicable(app, goal)) {
050: result = result.prepend(app);
051: }
052: }
053: }
054:
055: return result;
056: }
057:
058: /**
059: * returns a copy of this index
060: */
061: public BuiltInRuleAppIndex copy() {
062: return new BuiltInRuleAppIndex(index.copy());
063: }
064:
065: public void setNewRuleListener(NewRuleListener p_newRuleListener) {
066: newRuleListener = p_newRuleListener;
067: }
068:
069: public BuiltInRuleIndex builtInRuleIndex() {
070: return index;
071: }
072:
073: private NewRuleListener getNewRulePropagator() {
074: return newRuleListener;
075: }
076:
077: public void scanApplicableRules(Goal goal, Constraint userConstraint) {
078: scanSimplificationRule(goal, userConstraint,
079: getNewRulePropagator());
080: // scanDecProcRule(goal, userConstraint, getNewRulePropagator () );
081: }
082:
083: private void scanDecProcRule(Goal goal, Constraint userConstraint,
084: NewRuleListener listener) {
085: BuiltInRule bir = findDecProcRule();
086: BuiltInRuleApp app = new BuiltInRuleApp(bir, null,
087: userConstraint);
088: listener.ruleAdded(app, null);
089: }
090:
091: private SimplifyIntegerRule findDecProcRule() {
092: if (simplify != null)
093: return simplify;
094: IteratorOfBuiltInRule it = index.rules().iterator();
095: while (it.hasNext()) {
096: BuiltInRule bir = it.next();
097: if (bir instanceof SimplifyIntegerRule) {
098: simplify = (SimplifyIntegerRule) bir;
099: }
100: }
101: return simplify;
102: }
103:
104: private void scanSimplificationRule(Goal goal,
105: Constraint userConstraint, NewRuleListener listener) {
106: final IteratorOfBuiltInRule ruleIt = index.rules().iterator();
107: while (ruleIt.hasNext()) {
108: final BuiltInRule bir = ruleIt.next();
109: scanSimplificationRule(bir, goal, false, userConstraint,
110: listener);
111: scanSimplificationRule(bir, goal, true, userConstraint,
112: listener);
113: }
114: }
115:
116: private void scanSimplificationRule(BuiltInRule rule, Goal goal,
117: boolean antec, Constraint userConstraint,
118: NewRuleListener listener) {
119: final Node node = goal.node();
120: final Sequent seq = node.sequent();
121:
122: IteratorOfConstrainedFormula it = (antec ? seq.antecedent()
123: : seq.succedent()).iterator();
124:
125: while (it.hasNext()) {
126: final ConstrainedFormula cfma = it.next();
127: scanSimplificationRule(rule, goal, antec, userConstraint,
128: cfma, listener);
129: }
130: }
131:
132: private void scanSimplificationRule(BuiltInRule rule, Goal goal,
133: boolean antec, Constraint userConstraint,
134: ConstrainedFormula cfma, NewRuleListener listener) {
135: final PosInOccurrence pos = new PosInOccurrence(cfma,
136: PosInTerm.TOP_LEVEL, antec);
137: if (rule.isApplicable(goal, pos, userConstraint)) {
138: BuiltInRuleApp app = new BuiltInRuleApp(rule, pos,
139: userConstraint);
140: if (goal.proof().mgt().ruleApplicable(app, goal)) {
141: listener.ruleAdded(app, pos);
142: }
143: }
144: }
145:
146: public void reportRuleApps(NewRuleListener l, Goal goal,
147: Constraint userConstraint) {
148: scanSimplificationRule(goal, userConstraint, l);
149: // scanDecProcRule( goal, userConstraint, l );
150: }
151:
152: /**
153: * called if a formula has been replaced
154: * @param sci SequentChangeInfo describing the change of the sequent
155: */
156: public void sequentChanged(Goal goal, SequentChangeInfo sci) {
157: final Proof proof = goal.proof();
158: final Constraint userConstraint = proof.getUserConstraint()
159: .getConstraint();
160:
161: scanAddedFormulas(goal, true, sci, userConstraint);
162: scanAddedFormulas(goal, false, sci, userConstraint);
163:
164: scanModifiedFormulas(goal, true, sci, userConstraint);
165: scanModifiedFormulas(goal, false, sci, userConstraint);
166: }
167:
168: private void scanAddedFormulas(Goal goal, boolean antec,
169: SequentChangeInfo sci, final Constraint userConstraint) {
170: final IteratorOfBuiltInRule ruleIt = index.rules().iterator();
171: ListOfConstrainedFormula cfmas = sci.addedFormulas(antec);
172: final NewRuleListener listener = getNewRulePropagator();
173: while (!cfmas.isEmpty()) {
174: final ConstrainedFormula cfma = cfmas.head();
175: while (ruleIt.hasNext()) {
176: final BuiltInRule rule = ruleIt.next();
177: scanSimplificationRule(rule, goal, antec,
178: userConstraint, cfma, listener);
179: }
180: cfmas = cfmas.tail();
181: }
182: }
183:
184: private void scanModifiedFormulas(Goal goal, boolean antec,
185: SequentChangeInfo sci, final Constraint userConstraint) {
186: final IteratorOfBuiltInRule ruleIt = index.rules().iterator();
187:
188: final NewRuleListener listener = getNewRulePropagator();
189: ListOfFormulaChangeInfo fcis = sci.modifiedFormulas(antec);
190:
191: while (!fcis.isEmpty()) {
192: final FormulaChangeInfo fci = fcis.head();
193: final ConstrainedFormula cfma = fci.getNewFormula();
194: while (ruleIt.hasNext()) {
195: final BuiltInRule rule = ruleIt.next();
196: scanSimplificationRule(rule, goal, antec,
197: userConstraint, cfma, listener);
198: }
199: fcis = fcis.tail();
200: }
201: }
202:
203: }
|