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: package de.uka.ilkd.key.strategy.feature;
09:
10: import de.uka.ilkd.key.logic.PosInOccurrence;
11: import de.uka.ilkd.key.logic.op.Operator;
12: import de.uka.ilkd.key.proof.Goal;
13: import de.uka.ilkd.key.rule.RuleApp;
14:
15: /**
16: * This feature returns zero if and only if the focus of the given rule
17: * application exists, is not top-level and the symbol immediately above the
18: * focus is <code>badSymbol</code>. Optionally, one can also specify that
19: * zero should only be returned if the symbol immediately above the
20: * focus is <code>badSymbol</code> and the focus has a certain subterm index.
21: *
22: * TODO: eliminate this class and use term features instead
23: */
24: public abstract class DirectlyBelowFeature extends BinaryFeature {
25:
26: protected final Object badSymbol;
27: private final int index;
28:
29: protected DirectlyBelowFeature(Object badSymbol, int index) {
30: this .badSymbol = badSymbol;
31: this .index = index;
32: }
33:
34: protected boolean filter(RuleApp app, PosInOccurrence pos, Goal goal) {
35: if (pos == null)
36: return false;
37: if (pos.isTopLevel())
38: return false;
39: if (!isBadSymbol(pos.up().subTerm().op()))
40: return false;
41: return index == -1 || index == pos.getIndex();
42: }
43:
44: protected abstract boolean isBadSymbol(Operator op);
45:
46: }
|