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.Name;
14: import de.uka.ilkd.key.logic.PosInOccurrence;
15: import de.uka.ilkd.key.proof.Goal;
16: import de.uka.ilkd.key.proof.Proof;
17: import de.uka.ilkd.key.rule.RuleApp;
18:
19: /**
20: * Trivial implementation of the Strategy interface
21: * that uses only the goal time to determine the cost
22: * of a RuleApp.
23: */
24: public class FIFOStrategy implements Strategy {
25:
26: private static final Name NAME = new Name("FIFO");
27:
28: private FIFOStrategy() {
29: }
30:
31: /**
32: * Evaluate the cost of a <code>RuleApp</code>.
33: * @return the cost of the rule application expressed as
34: * a <code>RuleAppCost</code> object.
35: * <code>TopRuleAppCost.INSTANCE</code> indicates
36: * that the rule shall not be applied at all
37: * (it is discarded by the strategy).
38: */
39: public RuleAppCost computeCost(RuleApp app, PosInOccurrence pio,
40: Goal goal) {
41: return LongRuleAppCost.create(goal.getTime());
42: }
43:
44: /**
45: * Re-Evaluate a <code>RuleApp</code>. This method is
46: * called immediately before a rule is really applied
47: * @return true iff the rule should be applied, false otherwise
48: */
49: public boolean isApprovedApp(RuleApp app, PosInOccurrence pio,
50: Goal goal) {
51: return true;
52: }
53:
54: public void instantiateApp(RuleApp app, PosInOccurrence pio,
55: Goal goal, RuleAppCostCollector collector) {
56: }
57:
58: public Name name() {
59: return NAME;
60: }
61:
62: public static Strategy INSTANCE = new FIFOStrategy();
63:
64: public static class Factory extends StrategyFactory {
65: public Name name() {
66: return NAME;
67: }
68:
69: public Strategy create(Proof proof,
70: StrategyProperties properties) {
71: return INSTANCE;
72: }
73: }
74:
75: }
|