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.RuleFilter;
17: import de.uka.ilkd.key.proof.TacletFilter;
18: import de.uka.ilkd.key.rule.RuleApp;
19: import de.uka.ilkd.key.rule.TacletApp;
20: import de.uka.ilkd.key.strategy.feature.NonDuplicateAppFeature;
21:
22: /**
23: * Trivial implementation of the Strategy interface
24: * that uses only the goal time to determine the cost
25: * of a RuleApp. A TacletFilter is used to filter out
26: * RuleApps.
27: */
28: public class SimpleFilteredStrategy implements Strategy {
29:
30: private static final Name NAME = new Name("Simple ruleset");
31:
32: private RuleFilter ruleFilter;
33:
34: private static final long IF_NOT_MATCHED_MALUS = 0; // this should be a feature
35:
36: public SimpleFilteredStrategy() {
37: this (TacletFilter.TRUE);
38: }
39:
40: public SimpleFilteredStrategy(RuleFilter p_ruleFilter) {
41: ruleFilter = p_ruleFilter;
42: }
43:
44: public Name name() {
45: return NAME;
46: }
47:
48: /**
49: * Evaluate the cost of a <code>RuleApp</code>.
50: * @return the cost of the rule application expressed as
51: * a <code>RuleAppCost</code> object.
52: * <code>TopRuleAppCost.INSTANCE</code> indicates
53: * that the rule shall not be applied at all
54: * (it is discarded by the strategy).
55: */
56: public RuleAppCost computeCost(RuleApp app, PosInOccurrence pio,
57: Goal goal) {
58: if (app instanceof TacletApp && !ruleFilter.filter(app.rule()))
59: return TopRuleAppCost.INSTANCE;
60:
61: RuleAppCost res = NonDuplicateAppFeature.INSTANCE.compute(app,
62: pio, goal);
63: if (res == TopRuleAppCost.INSTANCE)
64: return res;
65:
66: long cost = goal.getTime();
67: if (app instanceof TacletApp
68: && !((TacletApp) app).ifInstsComplete())
69: cost += IF_NOT_MATCHED_MALUS;
70:
71: return LongRuleAppCost.create(cost);
72: }
73:
74: /**
75: * Re-Evaluate a <code>RuleApp</code>. This method is
76: * called immediately before a rule is really applied
77: * @return true iff the rule should be applied, false otherwise
78: */
79: public boolean isApprovedApp(RuleApp app, PosInOccurrence pio,
80: Goal goal) {
81: // do not apply a rule twice
82: if (app instanceof TacletApp
83: && NonDuplicateAppFeature.INSTANCE.compute(app, pio,
84: goal) == TopRuleAppCost.INSTANCE)
85: return false;
86:
87: return true;
88: }
89:
90: public void instantiateApp(RuleApp app, PosInOccurrence pio,
91: Goal goal, RuleAppCostCollector collector) {
92: }
93: }
|