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.feature;
12:
13: import java.util.HashMap;
14: import java.util.Map;
15:
16: import de.uka.ilkd.key.logic.PosInOccurrence;
17: import de.uka.ilkd.key.proof.Goal;
18: import de.uka.ilkd.key.rule.IteratorOfRuleSet;
19: import de.uka.ilkd.key.rule.RuleApp;
20: import de.uka.ilkd.key.rule.RuleSet;
21: import de.uka.ilkd.key.rule.TacletApp;
22: import de.uka.ilkd.key.strategy.LongRuleAppCost;
23: import de.uka.ilkd.key.strategy.RuleAppCost;
24: import de.uka.ilkd.key.strategy.TopRuleAppCost;
25:
26: /**
27: * Feature for relating rule sets with feature terms. Given a taclet
28: * application, this feature will iterate over the rule sets that the taclet
29: * belongs to, and for each rule set the corresponding feature term (if
30: * existing) is evaluated. The result of the feature is the sum of the results
31: * of the different rule set features.
32: */
33: public class RuleSetDispatchFeature implements Feature {
34:
35: private final Map rulesetToFeature = new HashMap();
36:
37: private RuleSetDispatchFeature() {
38: }
39:
40: public static RuleSetDispatchFeature create() {
41: return new RuleSetDispatchFeature();
42: }
43:
44: public RuleAppCost compute(RuleApp app, PosInOccurrence pos,
45: Goal goal) {
46: if (!(app instanceof TacletApp))
47: return LongRuleAppCost.ZERO_COST;
48:
49: RuleAppCost res = LongRuleAppCost.ZERO_COST;
50: final IteratorOfRuleSet it = ((TacletApp) app).taclet()
51: .ruleSets();
52: while (!(res instanceof TopRuleAppCost) && it.hasNext()) {
53: final Feature partialF = (Feature) rulesetToFeature.get(it
54: .next());
55: if (partialF != null)
56: res = res.add(partialF.compute(app, pos, goal));
57: }
58:
59: return res;
60: }
61:
62: /**
63: * Bind feature <code>f</code> to the rule set <code>ruleSet</code>. If
64: * this method is called more than once for the same rule set, the given
65: * features are added to each other.
66: */
67: public void add(RuleSet ruleSet, Feature f) {
68: Feature combinedF = (Feature) rulesetToFeature.get(ruleSet);
69: if (combinedF == null)
70: combinedF = f;
71: else
72: combinedF = BinarySumFeature.createSum(combinedF, f);
73:
74: rulesetToFeature.put(ruleSet, combinedF);
75: }
76:
77: /**
78: * Remove all features that have been related to <code>ruleSet</code>.
79: */
80: public void clear(RuleSet ruleSet) {
81: rulesetToFeature.remove(ruleSet);
82: }
83: }
|