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.logic.Named;
14: import de.uka.ilkd.key.logic.PosInOccurrence;
15: import de.uka.ilkd.key.proof.Goal;
16: import de.uka.ilkd.key.rule.RuleApp;
17:
18: /**
19: * Generic interface for evaluating the cost of
20: * a RuleApp with regard to a specific strategy
21: */
22: public interface Strategy extends Named {
23:
24: /**
25: * Evaluate the cost of a <code>RuleApp</code>.
26: * @return the cost of the rule application expressed as
27: * a <code>RuleAppCost</code> object.
28: * <code>TopRuleAppCost.INSTANCE</code> indicates
29: * that the rule shall not be applied at all
30: * (it is discarded by the strategy).
31: */
32: RuleAppCost computeCost(RuleApp app, PosInOccurrence pio, Goal goal);
33:
34: /**
35: * Re-Evaluate a <code>RuleApp</code>. This method is
36: * called immediately before a rule is really applied
37: * @return true iff the rule should be applied, false otherwise
38: */
39: boolean isApprovedApp(RuleApp app, PosInOccurrence pio, Goal goal);
40:
41: /**
42: * Instantiate an incomplete <code>RuleApp</code>. This method is
43: * called when the <code>AutomatedRuleApplicationManager</code>
44: * comes across a rule application in which some schema variables
45: * are not yet instantiated, or which is in some other way
46: * incomplete. The strategy then has the opportunity to
47: * return/provide a list of (more) complete rule applications by
48: * feeding them into the provided
49: * <code>RuleAppCostCollector</code>.
50: */
51: void instantiateApp(RuleApp app, PosInOccurrence pio, Goal goal,
52: RuleAppCostCollector collector);
53: }
|