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.LongRuleAppCost;
15: import de.uka.ilkd.key.strategy.RuleAppCost;
16: import de.uka.ilkd.key.strategy.TopRuleAppCost;
17:
18: /**
19: * Feature for invoking a list of term features on the direct subterms of a
20: * given term. The result will be the sum of the individual results. If the
21: * arity of the term investigated does not coincide with the number of term
22: * features that are given as arguments, <code>arityMismatchCost</code> will
23: * be returned
24: */
25: public class SubTermFeature implements TermFeature {
26:
27: private SubTermFeature(TermFeature[] features,
28: RuleAppCost arityMismatchCost) {
29: this .features = features;
30: this .arityMismatchCost = arityMismatchCost;
31: }
32:
33: public static TermFeature create(TermFeature[] fs,
34: RuleAppCost arityMismatchCost) {
35: final TermFeature[] fsCopy = new TermFeature[fs.length];
36: System.arraycopy(fs, 0, fsCopy, 0, fs.length);
37: return new SubTermFeature(fsCopy, arityMismatchCost);
38: }
39:
40: public static TermFeature create(TermFeature[] fs) {
41: return create(fs, TopRuleAppCost.INSTANCE);
42: }
43:
44: private final TermFeature[] features;
45: private final RuleAppCost arityMismatchCost;
46:
47: public RuleAppCost compute(Term term) {
48: if (term.arity() != features.length)
49: return arityMismatchCost;
50:
51: RuleAppCost res = LongRuleAppCost.ZERO_COST;
52:
53: for (int i = 0; i < features.length
54: && !(res instanceof TopRuleAppCost); i++)
55: res = res.add(features[i].compute(term.sub(i)));
56:
57: return res;
58: }
59: }
|