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 java.util.ArrayList;
014: import java.util.Collections;
015: import java.util.Iterator;
016: import java.util.List;
017:
018: import de.uka.ilkd.key.java.Services;
019: import de.uka.ilkd.key.logic.Constraint;
020: import de.uka.ilkd.key.logic.PosInOccurrence;
021: import de.uka.ilkd.key.logic.SequentChangeInfo;
022: import de.uka.ilkd.key.rule.*;
023:
024: /**
025: * manages the possible application of rules (RuleApps)
026: */
027: public class RuleAppIndex {
028:
029: private Goal goal;
030:
031: private TacletIndex tacletIndex;
032:
033: /**
034: * Two <code>TacletAppIndex</code> objects, one of which only contains rules
035: * that have to be applied interactively, and the other one for rules that
036: * can also be applied automatic. This is used as an optimization, as only
037: * the latter index has to be kept up to date while applying rules automated
038: */
039: private TacletAppIndex interactiveTacletAppIndex;
040: private TacletAppIndex automatedTacletAppIndex;
041:
042: private BuiltInRuleAppIndex builtInRuleAppIndex;
043:
044: private List listenerList = Collections
045: .synchronizedList(new ArrayList(10));
046:
047: /**
048: * The current mode of the index: For <code>autoMode==true</code>, the index
049: * <code>interactiveTacletAppIndex</code> is not updated
050: */
051: private boolean autoMode;
052:
053: public RuleAppIndex(TacletAppIndex p_tacletAppIndex,
054: BuiltInRuleAppIndex p_builtInRuleAppIndex) {
055: this (p_tacletAppIndex.tacletIndex(), p_builtInRuleAppIndex);
056: }
057:
058: public RuleAppIndex(TacletIndex p_tacletIndex,
059: BuiltInRuleAppIndex p_builtInRuleAppIndex) {
060: tacletIndex = p_tacletIndex;
061: automatedTacletAppIndex = new TacletAppIndex(tacletIndex);
062: interactiveTacletAppIndex = new TacletAppIndex(tacletIndex);
063: builtInRuleAppIndex = p_builtInRuleAppIndex;
064: // default to false to keep compatibility with old code
065: autoMode = false;
066:
067: automatedTacletAppIndex
068: .setRuleFilter(AnyRuleSetTacletFilter.INSTANCE);
069: interactiveTacletAppIndex.setRuleFilter(new NotRuleFilter(
070: AnyRuleSetTacletFilter.INSTANCE));
071:
072: setNewRuleListeners();
073: }
074:
075: private RuleAppIndex(TacletIndex tacletIndex,
076: TacletAppIndex interactiveTacletAppIndex,
077: TacletAppIndex automatedTacletAppIndex,
078: BuiltInRuleAppIndex builtInRuleAppIndex, boolean autoMode) {
079: this .tacletIndex = tacletIndex;
080: this .interactiveTacletAppIndex = interactiveTacletAppIndex;
081: this .automatedTacletAppIndex = automatedTacletAppIndex;
082: this .builtInRuleAppIndex = builtInRuleAppIndex;
083: this .autoMode = autoMode;
084:
085: setNewRuleListeners();
086: }
087:
088: private void setNewRuleListeners() {
089: NewRuleListener newRuleListener = new NewRuleListener() {
090: public void ruleAdded(RuleApp taclet, PosInOccurrence pos) {
091: informNewRuleListener(taclet, pos);
092: }
093: };
094: interactiveTacletAppIndex.setNewRuleListener(newRuleListener);
095: automatedTacletAppIndex.setNewRuleListener(newRuleListener);
096: builtInRuleAppIndex.setNewRuleListener(newRuleListener);
097: }
098:
099: public void setup(Goal p_goal) {
100: goal = p_goal;
101: interactiveTacletAppIndex.setup(p_goal);
102: automatedTacletAppIndex.setup(p_goal);
103: }
104:
105: /**
106: * Currently the rule app index can either operate in interactive mode (and
107: * contain applications of all existing taclets) or in automatic mode (and
108: * only contain a restricted set of taclets that can possibly be applied
109: * automated). This distinction could be replaced with a more general way to
110: * control the contents of the rule app index
111: */
112: public void autoModeStarted() {
113: autoMode = true;
114: }
115:
116: public void autoModeStopped() {
117: autoMode = false;
118: }
119:
120: /**
121: * returns the Taclet index for this ruleAppIndex.
122: */
123: public TacletIndex tacletIndex() {
124: return tacletIndex;
125: }
126:
127: /**
128: * returns the built-in rule application index for this
129: * ruleAppIndex.
130: */
131: public BuiltInRuleAppIndex builtInRuleAppIndex() {
132: return builtInRuleAppIndex;
133: }
134:
135: /**
136: * adds a change listener to the index
137: * @param l the AppIndexListener to add
138: */
139: public void addNewRuleListener(NewRuleListener l) {
140: listenerList.add(l);
141: }
142:
143: /**
144: * removes a change listener to the index
145: * @param l the AppIndexListener to remove
146: */
147: public void removeNewRuleListener(NewRuleListener l) {
148: listenerList.remove(l);
149: }
150:
151: /**returns the set of rule applications for
152: * the given heuristics
153: * at the given position of the given sequent.
154: * @param filter the TacletFiler filtering the taclets of interest
155: * @param pos the PosInOccurrence to focus
156: * @param services the Services object encapsulating information
157: * about the java datastructures like (static)types etc.
158: * @param userConstraint the Constraint with user defined instantiations
159: * of meta variables
160: */
161: public ListOfTacletApp getTacletAppAt(TacletFilter filter,
162: PosInOccurrence pos, Services services,
163: Constraint userConstraint) {
164: ListOfTacletApp result = SLListOfTacletApp.EMPTY_LIST;
165: if (!autoMode) {
166: result = result.prepend(interactiveTacletAppIndex
167: .getTacletAppAt(pos, filter, services,
168: userConstraint));
169: }
170: result = result.prepend(automatedTacletAppIndex.getTacletAppAt(
171: pos, filter, services, userConstraint));
172: return result;
173: }
174:
175: /**
176: * returns the rule applications at the given PosInOccurrence and at all
177: * Positions below this. The method calls getTacletAppAt for all the
178: * Positions below.
179: * @param filter the TacletFiler filtering the taclets of interest
180: * @param pos the position where to start from
181: * @param services the Services object encapsulating information
182: * about the java datastructures like (static)types etc.
183: * @param userConstraint the Constraint with user defined instantiations
184: * of meta variables
185: * @return the possible rule applications
186: */
187: public ListOfTacletApp getTacletAppAtAndBelow(TacletFilter filter,
188: PosInOccurrence pos, Services services,
189: Constraint userConstraint) {
190: ListOfTacletApp result = SLListOfTacletApp.EMPTY_LIST;
191: if (!autoMode) {
192: result = result.prepend(interactiveTacletAppIndex
193: .getTacletAppAtAndBelow(pos, filter, services,
194: userConstraint));
195: }
196: result = result.prepend(automatedTacletAppIndex
197: .getTacletAppAtAndBelow(pos, filter, services,
198: userConstraint));
199: return result;
200: }
201:
202: /**
203: * collects all FindTacletInstantiations for the given
204: * heuristics and position
205: * @param filter the TacletFiler filtering the taclets of interest
206: * @param pos the PosInOccurrence to focus
207: * @param services the Services object encapsulating information
208: * about the java datastructures like (static)types etc.
209: * @param userConstraint the Constraint with user defined instantiations
210: * of meta variables
211: * @return list of all possible instantiations
212: */
213: public ListOfNoPosTacletApp getFindTaclet(TacletFilter filter,
214: PosInOccurrence pos, Services services,
215: Constraint userConstraint) {
216: ListOfNoPosTacletApp result = SLListOfNoPosTacletApp.EMPTY_LIST;
217: if (!autoMode) {
218: result = result.prepend(interactiveTacletAppIndex
219: .getFindTaclet(pos, filter, services,
220: userConstraint));
221: }
222: result = result.prepend(automatedTacletAppIndex.getFindTaclet(
223: pos, filter, services, userConstraint));
224: return result;
225: }
226:
227: /**
228: * collects all NoFindTacletInstantiations for the given
229: * heuristics
230: * @param filter the TacletFiler filtering the taclets of interest
231: * @param services the Services object encapsulating information
232: * about the java datastructures like (static)types etc.
233: * @param userConstraint the Constraint with user defined instantiations
234: * of meta variables
235: * @return list of all possible instantiations
236: */
237: public ListOfNoPosTacletApp getNoFindTaclet(TacletFilter filter,
238: Services services, Constraint userConstraint) {
239: ListOfNoPosTacletApp result = SLListOfNoPosTacletApp.EMPTY_LIST;
240: if (!autoMode) {
241: result = result.prepend(interactiveTacletAppIndex
242: .getNoFindTaclet(filter, services, userConstraint));
243: }
244: result = result.prepend(automatedTacletAppIndex
245: .getNoFindTaclet(filter, services, userConstraint));
246: return result;
247: }
248:
249: /**
250: * collects all RewriteTacletInstantiations for the given
251: * heuristics in a subterm of the constraintformula described by a
252: * PosInOccurrence
253: * @param filter the TacletFiler filtering the taclets of interest
254: * @param pos the PosInOccurrence to focus
255: * @param services the Services object encapsulating information
256: * about the java datastructures like (static)types etc.
257: * @param userConstraint the Constraint with user defined instantiations
258: * of meta variables
259: * @return list of all possible instantiations
260: */
261: public ListOfNoPosTacletApp getRewriteTaclet(TacletFilter filter,
262: PosInOccurrence pos, Services services,
263: Constraint userConstraint) {
264: ListOfNoPosTacletApp result = SLListOfNoPosTacletApp.EMPTY_LIST;
265: if (!autoMode) {
266: result = result.prepend(interactiveTacletAppIndex
267: .getRewriteTaclet(pos, filter, services,
268: userConstraint));
269: }
270: result = result
271: .prepend(automatedTacletAppIndex.getRewriteTaclet(pos,
272: filter, services, userConstraint));
273: return result;
274: }
275:
276: /**
277: * returns a list of built-in rule applications applicable
278: * for the given goal, user defined constraint and position
279: */
280: public ListOfRuleApp getBuiltInRule(Goal goal, PosInOccurrence pos,
281: Constraint userConstraint) {
282:
283: return builtInRuleAppIndex().getBuiltInRule(goal, pos,
284: userConstraint);
285: }
286:
287: /**
288: * adds a new Taclet with instantiation information to the Taclet Index
289: * of this TacletAppIndex.
290: * @param tacletApp the NoPosTacletApp describing a partial instantiated Taclet to add
291: */
292: public void addNoPosTacletApp(NoPosTacletApp tacletApp) {
293: tacletIndex.add(tacletApp);
294:
295: if (autoMode)
296: interactiveTacletAppIndex.clearIndexes();
297:
298: interactiveTacletAppIndex.addedNoPosTacletApp(tacletApp);
299: automatedTacletAppIndex.addedNoPosTacletApp(tacletApp);
300: }
301:
302: /**
303: * remove a Taclet with instantiation information from the Taclet
304: * Index of this TacletAppIndex.
305: * @param tacletApp the NoPosTacletApp to remove
306: */
307: public void removeNoPosTacletApp(NoPosTacletApp tacletApp) {
308: tacletIndex.remove(tacletApp);
309:
310: if (autoMode)
311: interactiveTacletAppIndex.clearIndexes();
312:
313: interactiveTacletAppIndex.removedNoPosTacletApp(tacletApp);
314: automatedTacletAppIndex.removedNoPosTacletApp(tacletApp);
315: }
316:
317: /**
318: * called if a formula has been replaced
319: * @param goal the Goal which sequent has been changed
320: * @param sci SequentChangeInfo describing the change of the sequent
321: */
322: public void sequentChanged(Goal goal, SequentChangeInfo sci) {
323: if (!autoMode)
324: // the TacletAppIndex is able to detect modification of the
325: // sequent itself, it is not necessary to clear the index
326: interactiveTacletAppIndex.sequentChanged(goal, sci);
327: automatedTacletAppIndex.sequentChanged(goal, sci);
328: builtInRuleAppIndex().sequentChanged(goal, sci);
329: }
330:
331: /**
332: * Empties all caches
333: */
334: public void clearAndDetachCache() {
335: // Currently this only applies to the taclet index
336: interactiveTacletAppIndex.clearAndDetachCache();
337: automatedTacletAppIndex.clearAndDetachCache();
338: }
339:
340: /**
341: * Empties all caches
342: */
343: public void clearIndexes() {
344: // Currently this only applies to the taclet index
345: interactiveTacletAppIndex.clearIndexes();
346: automatedTacletAppIndex.clearIndexes();
347: }
348:
349: /**
350: * Ensures that all caches are fully up-to-date
351: */
352: public void fillCache() {
353: if (!autoMode)
354: interactiveTacletAppIndex.fillCache();
355: automatedTacletAppIndex.fillCache();
356: }
357:
358: /**
359: * Report all rule applications that are supposed to be applied
360: * automatically, and that are currently stored by the index
361: *
362: * @param l the NewRuleListener
363: * @param services the Services
364: * @param userConstraint the Constraint capturing user defined instantiations
365: * of meta variables
366: */
367: public void reportAutomatedRuleApps(NewRuleListener l,
368: Services services, Constraint userConstraint) {
369: automatedTacletAppIndex.reportRuleApps(l, services,
370: userConstraint);
371: builtInRuleAppIndex().reportRuleApps(l, goal, userConstraint);
372: }
373:
374: /**
375: * Report builtin rules to all registered NewRuleListener instances.
376: * @param p_goal the Goal which to scan
377: * @param p_userConstraint the Constraint capturing user defined instantiations
378: * of meta variables
379: */
380: public void scanBuiltInRules(Goal p_goal,
381: Constraint p_userConstraint) {
382: builtInRuleAppIndex().scanApplicableRules(p_goal,
383: p_userConstraint);
384: }
385:
386: /**
387: * informs all observers, if a formula has been added, changed or
388: * removed
389: */
390: private void informNewRuleListener(RuleApp p_app,
391: PosInOccurrence p_pos) {
392: Iterator it = listenerList.iterator();
393: while (it.hasNext())
394: ((NewRuleListener) it.next()).ruleAdded(p_app, p_pos);
395: }
396:
397: /**
398: * returns a new RuleAppIndex with a copied TacletIndex.
399: * Attention: the listener lists are not copied
400: */
401: public RuleAppIndex copy() {
402: TacletIndex copiedTacletIndex = tacletIndex.copy();
403: TacletAppIndex copiedInteractiveTacletAppIndex = interactiveTacletAppIndex
404: .copyWithTacletIndex(copiedTacletIndex);
405: TacletAppIndex copiedAutomatedTacletAppIndex = automatedTacletAppIndex
406: .copyWithTacletIndex(copiedTacletIndex);
407: return new RuleAppIndex(copiedTacletIndex,
408: copiedInteractiveTacletAppIndex,
409: copiedAutomatedTacletAppIndex, builtInRuleAppIndex()
410: .copy(), autoMode);
411: }
412:
413: public String toString() {
414: return "RuleAppIndex with indexing, getting Taclets from"
415: + " TacletAppIndex " + interactiveTacletAppIndex
416: + " and " + automatedTacletAppIndex;
417: }
418: }
|