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 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.RuleAppCost;
17: import de.uka.ilkd.key.strategy.TopRuleAppCost;
18:
19: /**
20: * A feature that computes the sum of two given features (faster than the more
21: * general class <code>SumFeature</code>)
22: */
23: public class BinarySumFeature implements Feature {
24:
25: public RuleAppCost compute(RuleApp app, PosInOccurrence pos,
26: Goal goal) {
27: RuleAppCost f0Cost = f0.compute(app, pos, goal);
28: if (f0Cost instanceof TopRuleAppCost)
29: return f0Cost;
30: return f0Cost.add(f1.compute(app, pos, goal));
31: }
32:
33: private BinarySumFeature(Feature f0, Feature f1) {
34: this .f0 = f0;
35: this .f1 = f1;
36: }
37:
38: public static Feature createSum(Feature f0, Feature f1) {
39: return new BinarySumFeature(f0, f1);
40: }
41:
42: private final Feature f0, f1;
43: }
|