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.PosInOccurrence;
14: import de.uka.ilkd.key.proof.Goal;
15: import de.uka.ilkd.key.rule.BuiltInRuleApp;
16: import de.uka.ilkd.key.rule.NoPosTacletApp;
17: import de.uka.ilkd.key.rule.RuleApp;
18: import de.uka.ilkd.key.util.Debug;
19:
20: /**
21: * Container for RuleApp instances with cost as determined by
22: * a given Strategy.
23: * Instances of this class are immutable
24: */
25: public abstract class RuleAppContainer implements Comparable {
26:
27: /**
28: * The stored rule app
29: */
30: private final RuleApp ruleApp;
31:
32: /**
33: * The costs of the stored rule app
34: */
35: private final RuleAppCost cost;
36:
37: protected RuleAppContainer(RuleApp p_app, RuleAppCost p_cost) {
38: ruleApp = p_app;
39: cost = p_cost;
40: }
41:
42: public int compareTo(Object o) {
43: // deliberately raise a <code>ClassCastException</code> for unsuitable
44: // arguments
45: return cost.compareTo(((RuleAppContainer) o).cost);
46: }
47:
48: /**
49: * Create a list of new RuleAppContainers that are to be
50: * considered for application.
51: */
52: public abstract ListOfRuleAppContainer createFurtherApps(
53: Goal p_goal, Strategy strategy);
54:
55: /**
56: * Create a <code>RuleApp</code> that is suitable to be applied
57: * or <code>null</code>.
58: */
59: public abstract RuleApp completeRuleApp(Goal p_goal,
60: Strategy strategy);
61:
62: protected RuleApp getRuleApp() {
63: return ruleApp;
64: }
65:
66: public RuleAppCost getCost() {
67: return cost;
68: }
69:
70: /**
71: * Create containers for RuleApps.
72: * @return list of containers for currently applicable RuleApps, the cost
73: * may be an instance of <code>TopRuleAppCost</code>.
74: */
75: public static ListOfRuleAppContainer createAppContainers(
76: RuleApp p_app, PosInOccurrence p_pio, Goal p_goal,
77: Strategy p_strategy) {
78:
79: if (p_app instanceof NoPosTacletApp)
80: return TacletAppContainer.createAppContainers(
81: (NoPosTacletApp) p_app, p_pio, p_goal, p_strategy);
82:
83: if (p_app instanceof BuiltInRuleApp)
84: return BuiltInRuleAppContainer.createAppContainers(
85: (BuiltInRuleApp) p_app, p_pio, p_goal, p_strategy);
86:
87: Debug.fail("Unexpected kind of rule.");
88:
89: return null;
90: }
91:
92: }
|