01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.strategy;
12:
13: import de.uka.ilkd.key.proof.Goal;
14: import de.uka.ilkd.key.proof.NewRuleListener;
15: import de.uka.ilkd.key.rule.RuleApp;
16:
17: /**
18: *
19: */
20: public interface AutomatedRuleApplicationManager extends
21: NewRuleListener {
22:
23: /**
24: * Clear existing caches of applicable rules
25: */
26: void clearCache();
27:
28: /**
29: * @return the first applicable rule app, i.e. the least expensive element
30: * of the heap that is not obsolete and caches the result of this
31: * operation to save some time the next time the method
32: * nextAndCache() or next() is called. A call of next() empties the
33: * cache again.
34: */
35: RuleApp peekNext();
36:
37: /**
38: * @return the next rule that is supposed to be applied
39: */
40: RuleApp next();
41:
42: /**
43: * Set the goal <code>this</code> is the rule app manager for
44: */
45: void setGoal(Goal p_goal);
46:
47: AutomatedRuleApplicationManager copy();
48:
49: }
|