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 three given features (faster than the more
21: * general class <code>SumFeature</code>)
22: */
23: public class TernarySumFeature implements Feature {
24:
25: public RuleAppCost compute(RuleApp app, PosInOccurrence pos,
26: Goal goal) {
27: RuleAppCost res = f0.compute(app, pos, goal);
28: if (res instanceof TopRuleAppCost)
29: return res;
30: res = res.add(f1.compute(app, pos, goal));
31: if (res instanceof TopRuleAppCost)
32: return res;
33: return res.add(f2.compute(app, pos, goal));
34: }
35:
36: private TernarySumFeature(Feature f0, Feature f1, Feature f2) {
37: this .f0 = f0;
38: this .f1 = f1;
39: this .f2 = f2;
40: }
41:
42: public static Feature createSum(Feature f0, Feature f1, Feature f2) {
43: return new TernarySumFeature(f0, f1, f2);
44: }
45:
46: private final Feature f0, f1, f2;
47:
48: }
|