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: * Feature for invoking a term feature recursively on all subterms of a term.
19: * The result will be the sum of the individual results for subterms. The
20: * feature descends to subterms as long as <code>cond</code> returns zero.
21: */
22: public class RecSubTermFeature implements TermFeature {
23:
24: private final TermFeature cond, summand;
25:
26: private RecSubTermFeature(TermFeature cond, TermFeature summand) {
27: this .cond = cond;
28: this .summand = summand;
29: }
30:
31: public static TermFeature create(TermFeature cond,
32: TermFeature summand) {
33: return new RecSubTermFeature(cond, summand);
34: }
35:
36: public RuleAppCost compute(Term term) {
37: RuleAppCost res = summand.compute(term);
38:
39: if (res instanceof TopRuleAppCost
40: || cond.compute(term) instanceof TopRuleAppCost)
41: return res;
42:
43: for (int i = 0; i != term.arity()
44: && !(res instanceof TopRuleAppCost); ++i)
45: res = res.add(compute(term.sub(i)));
46:
47: return res;
48: }
49: }
|