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.rule.TacletApp;
17:
18: /**
19: * Abstract superclass for features of TacletApps that have either zero or top
20: * cost.
21: */
22: public abstract class BinaryTacletAppFeature extends BinaryFeature {
23:
24: private final boolean nonTacletValue;
25:
26: protected BinaryTacletAppFeature() {
27: nonTacletValue = true;
28: }
29:
30: /**
31: * @param p_nonTacletValue
32: * the value that is to be returned should the feature be applied
33: * to a rule that is not a taclet
34: */
35: protected BinaryTacletAppFeature(boolean p_nonTacletValue) {
36: nonTacletValue = p_nonTacletValue;
37: }
38:
39: final protected boolean filter(RuleApp app, PosInOccurrence pos,
40: Goal goal) {
41: if (app instanceof TacletApp)
42: return filter((TacletApp) app, pos, goal);
43: return nonTacletValue;
44: }
45:
46: /**
47: * Compute whether the result of the feature is zero (<code>true</code>)
48: * or infinity (<code>false</code>)
49: *
50: * @param app
51: * the TacletApp
52: * @param pos
53: * position where <code>app</code> is to be applied
54: * @param goal
55: * the goal on which <code>app</code> is to be applied
56: * @return true iff the the result of the feature is supposed to be zero.
57: */
58: protected abstract boolean filter(TacletApp app,
59: PosInOccurrence pos, Goal goal);
60: }
|