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.feature;
12:
13: import de.uka.ilkd.key.logic.PosInOccurrence;
14: import de.uka.ilkd.key.proof.Goal;
15: import de.uka.ilkd.key.rule.RuleApp;
16: import de.uka.ilkd.key.strategy.LongRuleAppCost;
17: import de.uka.ilkd.key.strategy.RuleAppCost;
18: import de.uka.ilkd.key.strategy.TopRuleAppCost;
19:
20: /**
21: * Abstract superclass for features that have either zero cost or top cost.
22: */
23: public abstract class BinaryFeature implements Feature {
24:
25: protected BinaryFeature() {
26: }
27:
28: /** Constant that represents the boolean value true */
29: public static final RuleAppCost ZERO_COST = LongRuleAppCost.ZERO_COST;
30: /** Constant that represents the boolean value false */
31: public static final RuleAppCost TOP_COST = TopRuleAppCost.INSTANCE;
32:
33: public RuleAppCost compute(RuleApp app, PosInOccurrence pos,
34: Goal goal) {
35: return filter(app, pos, goal) ? ZERO_COST : TOP_COST;
36: }
37:
38: /**
39: * Compute whether the result of the feature is zero (<code>true</code>)
40: * or infinity (<code>false</code>)
41: *
42: * @param app
43: * the RuleApp
44: * @param pos
45: * position where <code>app</code> is to be applied
46: * @param goal
47: * the goal on which <code>app</code> is to be applied
48: * @return true iff the the result of the feature is supposed to be zero.
49: */
50: protected abstract boolean filter(RuleApp app, PosInOccurrence pos,
51: Goal goal);
52:
53: }
|