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.proof.RuleFilter;
016: import de.uka.ilkd.key.rule.RuleApp;
017: import de.uka.ilkd.key.strategy.LongRuleAppCost;
018: import de.uka.ilkd.key.strategy.RuleAppCost;
019:
020: /**
021: * A feature that evaluates one of two given features, depending on the result
022: * of a <code>RuleFilter</code>
023: */
024: public class ConditionalFeature implements Feature {
025:
026: private ConditionalFeature(RuleFilter p_cond,
027: Feature p_thenFeature, Feature p_elseFeature) {
028: cond = p_cond;
029: thenFeature = p_thenFeature;
030: elseFeature = p_elseFeature;
031: }
032:
033: public RuleAppCost compute(RuleApp app, PosInOccurrence pos,
034: Goal goal) {
035: if (cond.filter(app.rule()))
036: return thenFeature.compute(app, pos, goal);
037: else
038: return elseFeature.compute(app, pos, goal);
039: }
040:
041: /**
042: * @param cond the filter that decides which value is to be returned
043: * @param thenValue the value of the feature, if <code>filter</code>
044: * returns true
045: */
046: public static Feature createConditional(RuleFilter cond,
047: RuleAppCost thenValue) {
048: return createConditional(cond, ConstFeature
049: .createConst(thenValue));
050: }
051:
052: /**
053: * @param cond the filter that decides which value is to be returned
054: * @param thenValue the value of the feature, if <code>filter</code>
055: * returns true
056: * @param elseValue the value of the feature, if <code>filter</code>
057: * returns false
058: */
059: public static Feature createConditional(RuleFilter cond,
060: RuleAppCost thenValue, RuleAppCost elseValue) {
061: return createConditional(cond, ConstFeature
062: .createConst(thenValue), ConstFeature
063: .createConst(elseValue));
064: }
065:
066: /**
067: * @param cond the filter that decides which value is to be returned
068: * @param thenFeature the feature that is evaluted, if <code>filter</code>
069: * returns true
070: * @param elseValue the value of the feature, if <code>filter</code>
071: * returns false
072: */
073: public static Feature createConditional(RuleFilter cond,
074: Feature thenFeature) {
075: return createConditional(cond, thenFeature,
076: LongRuleAppCost.ZERO_COST);
077: }
078:
079: /**
080: * @param cond the filter that decides which value is to be returned
081: * @param thenFeature the feature that is evaluted, if <code>filter</code>
082: * returns true
083: * @param elseValue the value of the feature, if <code>filter</code>
084: * returns false
085: */
086: public static Feature createConditional(RuleFilter cond,
087: Feature thenFeature, RuleAppCost elseValue) {
088: return createConditional(cond, thenFeature, ConstFeature
089: .createConst(elseValue));
090: }
091:
092: /**
093: * @param cond the filter that decides which value is to be returned
094: * @param thenFeature the feature that is evaluted, if <code>filter</code>
095: * returns true
096: * @param elseFeature the feature that is evaluted, if <code>filter</code>
097: * returns false
098: */
099: public static Feature createConditional(RuleFilter cond,
100: Feature thenFeature, Feature elseFeature) {
101: return new ConditionalFeature(cond, thenFeature, elseFeature);
102: }
103:
104: /**
105: * The filter that decides which sub-feature is to be evaluated
106: */
107: private final RuleFilter cond;
108:
109: /**
110: * The feature for positive results of <code>filter</code>
111: */
112: private final Feature thenFeature;
113:
114: /**
115: * The feature for negative results of <code>filter</code>
116: */
117: private final Feature elseFeature;
118: }
|