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.termfeature;
12:
13: import de.uka.ilkd.key.logic.Term;
14: import de.uka.ilkd.key.strategy.RuleAppCost;
15: import de.uka.ilkd.key.strategy.TopRuleAppCost;
16:
17: /**
18: * A feature that computes the sum of two given features (faster than the more
19: * general class <code>SumFeature</code>)
20: */
21: public class BinarySumTermFeature implements TermFeature {
22:
23: public RuleAppCost compute(Term term) {
24: RuleAppCost f0Cost = f0.compute(term);
25: if (f0Cost instanceof TopRuleAppCost)
26: return f0Cost;
27: return f0Cost.add(f1.compute(term));
28: }
29:
30: private BinarySumTermFeature(TermFeature f0, TermFeature f1) {
31: this .f0 = f0;
32: this .f1 = f1;
33: }
34:
35: public static TermFeature createSum(TermFeature f0, TermFeature f1) {
36: return new BinarySumTermFeature(f0, f1);
37: }
38:
39: private final TermFeature f0, f1;
40: }
|