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: package de.uka.ilkd.key.strategy.feature;
11:
12: import de.uka.ilkd.key.logic.op.Operator;
13:
14: /**
15: * This feature returns zero if and only if the focus of the given rule
16: * application exists, is not top-level and the symbol immediately above the
17: * focus is <code>badSymbol</code>. Optionally, one can also specify that
18: * zero should only be returned if the symbol immediately above the
19: * focus is <code>badSymbol</code> and the focus has a certain subterm index.
20: *
21: * TODO: eliminate this class and use term features instead
22: */
23: public class DirectlyBelowSymbolFeature extends DirectlyBelowFeature {
24:
25: private DirectlyBelowSymbolFeature(Operator badSymbol, int index) {
26: super (badSymbol, index);
27: }
28:
29: public static Feature create(Operator badSymbol) {
30: return new DirectlyBelowSymbolFeature(badSymbol, -1);
31: }
32:
33: public static Feature create(Operator badSymbol, int index) {
34: return new DirectlyBelowSymbolFeature(badSymbol, index);
35: }
36:
37: protected boolean isBadSymbol(Operator op) {
38: return badSymbol == op;
39: }
40:
41: }
|