001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.strategy.feature;
012:
013: import de.uka.ilkd.key.logic.PosInOccurrence;
014: import de.uka.ilkd.key.proof.Goal;
015: import de.uka.ilkd.key.rule.RuleApp;
016: import de.uka.ilkd.key.strategy.LongRuleAppCost;
017: import de.uka.ilkd.key.strategy.RuleAppCost;
018:
019: /**
020: * A conditional feature, in which the condition itself is a (binary) feature.
021: * The general notion is a term <code>c ? f1 : f2</code>, whereby the
022: * condition <code>c</code> determines whether the value of the whole
023: * expression is <code>f1</code> (if <code>c</code> returns zero, or more
024: * general if <code>c</code> returns a distinguished value
025: * <code>trueCost</code>) or <code>f2</code>
026: */
027: public class ShannonFeature implements Feature {
028:
029: /**
030: * The filter that decides which sub-feature is to be evaluated
031: */
032: private final Feature cond;
033:
034: /**
035: * If the result of <code>cond</code> is this cost, then the condition
036: * is assumed to hold
037: */
038: private final RuleAppCost trueCost;
039:
040: /**
041: * The feature for positive results of <code>filter</code>
042: */
043: private final Feature thenFeature;
044:
045: /**
046: * The feature for negative results of <code>filter</code>
047: */
048: private final Feature elseFeature;
049:
050: private ShannonFeature(Feature p_cond, RuleAppCost p_trueCost,
051: Feature p_thenFeature, Feature p_elseFeature) {
052: cond = p_cond;
053: trueCost = p_trueCost;
054: thenFeature = p_thenFeature;
055: elseFeature = p_elseFeature;
056: }
057:
058: public RuleAppCost compute(RuleApp app, PosInOccurrence pos,
059: Goal goal) {
060: if (cond.compute(app, pos, goal).equals(trueCost))
061: return thenFeature.compute(app, pos, goal);
062: else
063: return elseFeature.compute(app, pos, goal);
064: }
065:
066: /**
067: * @param cond
068: * the feature that decides which value is to be returned
069: * @param trueCost
070: * the value of <code>cond</code> that is regarded as
071: * true-value
072: * @param thenValue
073: * the value of the feature, if <code>cond</code> returns
074: * <code>trueCost</code>
075: * @return <code>thenValue</code> if <code>cond</code> returns
076: * <code>trueCost</code>, zero otherwise
077: */
078: public static Feature createConditional(Feature cond,
079: RuleAppCost trueCost, RuleAppCost thenValue) {
080: return createConditional(cond, trueCost, ConstFeature
081: .createConst(thenValue));
082: }
083:
084: /**
085: * @param cond
086: * the feature that decides which value is to be returned
087: * @param trueCost
088: * the value of <code>cond</code> that is regarded as
089: * true-value
090: * @param thenValue
091: * the value of the feature if <code>cond</code> returns
092: * <code>trueCost</code>
093: * @param elseValue
094: * the value of the feature if <code>cond</code> does not
095: * return <code>trueCost</code>
096: * @return <code>thenValue</code> if <code>cond</code> returns
097: * <code>trueCost</code>, <code>elseValue</code> otherwise
098: */
099: public static Feature createConditional(Feature cond,
100: RuleAppCost trueCost, RuleAppCost thenValue,
101: RuleAppCost elseValue) {
102: return createConditional(cond, trueCost, ConstFeature
103: .createConst(thenValue), ConstFeature
104: .createConst(elseValue));
105: }
106:
107: /**
108: * @param cond
109: * the feature that decides which value is to be returned
110: * @param trueCost
111: * the value of <code>cond</code> that is regarded as
112: * true-value
113: * @param thenFeature
114: * the value of the feature if <code>cond</code> returns
115: * <code>trueCost</code>
116: * @return the value of <code>thenFeature</code> if <code>cond</code>
117: * returns <code>trueCost</code>, zero otherwise
118: */
119: public static Feature createConditional(Feature cond,
120: RuleAppCost trueCost, Feature thenFeature) {
121: return createConditional(cond, trueCost, thenFeature,
122: LongRuleAppCost.ZERO_COST);
123: }
124:
125: /**
126: * @param cond
127: * the feature that decides which value is to be returned
128: * @param trueCost
129: * the value of <code>cond</code> that is regarded as
130: * true-value
131: * @param thenFeature
132: * the value of the feature if <code>cond</code> returns
133: * <code>trueCost</code>
134: * @param elseValue
135: * the value of the feature if <code>cond</code> does not
136: * return <code>trueCost</code>
137: * @return the value of <code>thenFeature</code> if <code>cond</code>
138: * returns <code>trueCost</code>, <code>elseValue</code>
139: * otherwise
140: */
141: public static Feature createConditional(Feature cond,
142: RuleAppCost trueCost, Feature thenFeature,
143: RuleAppCost elseValue) {
144: return createConditional(cond, trueCost, thenFeature,
145: ConstFeature.createConst(elseValue));
146: }
147:
148: /**
149: * @param cond
150: * the feature that decides which value is to be returned
151: * @param trueCost
152: * the value of <code>cond</code> that is regarded as
153: * true-value
154: * @param thenFeature
155: * the value of the feature if <code>cond</code> returns
156: * <code>trueCost</code>
157: * @param elseFeature
158: * the value of the feature if <code>cond</code> does not
159: * return <code>trueCost</code>
160: * @return the value of <code>thenFeature</code> if <code>cond</code>
161: * returns <code>trueCost</code>, the value of
162: * <code>elseFeature</code> otherwise
163: */
164: public static Feature createConditional(Feature cond,
165: RuleAppCost trueCost, Feature thenFeature,
166: Feature elseFeature) {
167: return new ShannonFeature(cond, trueCost, thenFeature,
168: elseFeature);
169: }
170:
171: /**
172: * @param cond
173: * the feature that decides which value is to be returned
174: * @param thenValue
175: * the value of the feature if <code>cond</code> returns zero
176: * @return the value of <code>thenFeature</code> if <code>cond</code>
177: * returns zero, zero otherwise
178: */
179: public static Feature createConditionalBinary(Feature cond,
180: RuleAppCost thenValue) {
181: return createConditionalBinary(cond, ConstFeature
182: .createConst(thenValue));
183: }
184:
185: /**
186: * @param cond
187: * the feature that decides which value is to be returned
188: * @param thenValue
189: * the value of the feature if <code>cond</code> returns zero
190: * @param elseValue
191: * the value of the feature if <code>cond</code> does not
192: * return zero
193: * @return <code>thenValue</code> if <code>cond</code> returns zero,
194: * <code>elseValue</code> otherwise
195: */
196: public static Feature createConditionalBinary(Feature cond,
197: RuleAppCost thenValue, RuleAppCost elseValue) {
198: return createConditionalBinary(cond, ConstFeature
199: .createConst(thenValue), ConstFeature
200: .createConst(elseValue));
201: }
202:
203: /**
204: * @param cond
205: * the feature that decides which value is to be returned
206: * @param thenFeature
207: * the value of the feature if <code>cond</code> returns zero
208: * @param elseValue
209: * the value of the feature if <code>cond</code> does not
210: * return zero
211: * @return the value of <code>thenFeature</code> if <code>cond</code>
212: * returns zero, <code>elseValue</code> otherwise
213: */
214: public static Feature createConditionalBinary(Feature cond,
215: Feature thenFeature, RuleAppCost elseValue) {
216: return createConditionalBinary(cond, thenFeature, ConstFeature
217: .createConst(elseValue));
218: }
219:
220: /**
221: * @param cond
222: * the feature that decides which value is to be returned
223: * @param thenFeature
224: * the value of the feature if <code>cond</code> returns zero
225: * @param elseFeature
226: * the value of the feature if <code>cond</code> does not
227: * return zero
228: * @return the value of <code>thenFeature</code> if <code>cond</code>
229: * returns zero, the value of <code>elseFeature</code> otherwise
230: */
231: public static Feature createConditionalBinary(Feature cond,
232: Feature thenFeature, Feature elseFeature) {
233: return createConditional(cond, BinaryFeature.ZERO_COST,
234: thenFeature, elseFeature);
235: }
236:
237: /**
238: * @param cond
239: * the feature that decides which value is to be returned
240: * @param thenFeature
241: * the value of the feature if <code>cond</code> returns zero
242: * @return the value of <code>thenFeature</code> if <code>cond</code>
243: * returns zero, zero otherwise
244: */
245: public static Feature createConditionalBinary(Feature cond,
246: Feature thenFeature) {
247: return createConditional(cond, BinaryFeature.ZERO_COST,
248: thenFeature, LongRuleAppCost.ZERO_COST);
249: }
250:
251: }
|