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:
17: /**
18: * A conditional feature, in which the condition itself is a (binary) feature.
19: * The general notion is a term <code>c ? f1 : f2</code>, whereby the
20: * condition <code>c</code> determines whether the value of the whole
21: * expression is <code>f1</code> (if <code>c</code> returns zero, or more
22: * general if <code>c</code> returns a distinguished value
23: * <code>trueCost</code>) or <code>f2</code>
24: */
25: public class ShannonTermFeature implements TermFeature {
26:
27: /**
28: * The filter that decides which sub-feature is to be evaluated
29: */
30: private final TermFeature cond;
31:
32: /**
33: * If the result of <code>cond</code> is this cost, then the condition is
34: * assumed to hold
35: */
36: private final RuleAppCost trueCost;
37:
38: /**
39: * The feature for positive results of <code>filter</code>
40: */
41: private final TermFeature thenFeature;
42:
43: /**
44: * The feature for negative results of <code>filter</code>
45: */
46: private final TermFeature elseFeature;
47:
48: private ShannonTermFeature(TermFeature p_cond,
49: RuleAppCost p_trueCost, TermFeature p_thenFeature,
50: TermFeature p_elseFeature) {
51: cond = p_cond;
52: trueCost = p_trueCost;
53: thenFeature = p_thenFeature;
54: elseFeature = p_elseFeature;
55: }
56:
57: public RuleAppCost compute(Term term) {
58: if (cond.compute(term).equals(trueCost))
59: return thenFeature.compute(term);
60: else
61: return elseFeature.compute(term);
62: }
63:
64: /**
65: * @param cond
66: * the feature that decides which value is to be returned
67: * @param thenFeature
68: * the value of the feature if <code>cond</code> returns zero
69: * @param elseFeature
70: * the value of the feature if <code>cond</code> does not
71: * return zero
72: * @return the value of <code>thenFeature</code> if <code>cond</code>
73: * returns zero, the value of <code>elseFeature</code> otherwise
74: */
75: public static TermFeature createConditionalBinary(TermFeature cond,
76: TermFeature thenFeature, TermFeature elseFeature) {
77: return new ShannonTermFeature(cond,
78: BinaryTermFeature.ZERO_COST, thenFeature, elseFeature);
79: }
80:
81: /**
82: * @param cond
83: * the feature that decides which value is to be returned
84: * @param thenFeature
85: * the value of the feature if <code>cond</code> returns zero
86: * @return the value of <code>thenFeature</code> if <code>cond</code>
87: * returns zero, zero otherwise
88: */
89: public static TermFeature createConditionalBinary(TermFeature cond,
90: TermFeature thenFeature) {
91: return createConditionalBinary(cond, thenFeature,
92: ConstTermFeature.createConst(LongRuleAppCost.ZERO_COST));
93: }
94:
95: }
|