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.quantifierHeuristics;
12:
13: import de.uka.ilkd.key.logic.PosInOccurrence;
14: import de.uka.ilkd.key.proof.Goal;
15: import de.uka.ilkd.key.rule.RuleApp;
16: import de.uka.ilkd.key.strategy.LongRuleAppCost;
17: import de.uka.ilkd.key.strategy.RuleAppCost;
18: import de.uka.ilkd.key.strategy.TopRuleAppCost;
19: import de.uka.ilkd.key.strategy.feature.Feature;
20:
21: public class InstantiationCostScalerFeature implements Feature {
22:
23: private final Feature costFeature;
24: private final Feature allowSplitting;
25:
26: private static final RuleAppCost ONE_COST = LongRuleAppCost
27: .create(1);
28: private static final RuleAppCost MINUS_3000_COST = LongRuleAppCost
29: .create(-3000);
30:
31: private InstantiationCostScalerFeature(Feature costFeature,
32: Feature allowSplitting) {
33: this .costFeature = costFeature;
34: this .allowSplitting = allowSplitting;
35: }
36:
37: public static Feature create(Feature costFeature,
38: Feature allowSplitting) {
39: return new InstantiationCostScalerFeature(costFeature,
40: allowSplitting);
41: }
42:
43: public RuleAppCost compute(RuleApp app, PosInOccurrence pos,
44: Goal goal) {
45:
46: final RuleAppCost cost = costFeature.compute(app, pos, goal);
47:
48: if (cost.equals(LongRuleAppCost.ZERO_COST))
49: return MINUS_3000_COST;
50: if (cost.equals(ONE_COST))
51: return LongRuleAppCost.ZERO_COST;
52:
53: final RuleAppCost as = allowSplitting.compute(app, pos, goal);
54: if (!as.equals(LongRuleAppCost.ZERO_COST))
55: return TopRuleAppCost.INSTANCE;
56:
57: assert cost instanceof LongRuleAppCost : "Can only handle LongRuleAppCost";
58:
59: final LongRuleAppCost longCost = (LongRuleAppCost) cost;
60: return LongRuleAppCost.create(longCost.getValue() + 200);
61: }
62:
63: }
|