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.PIOPathIterator;
14: import de.uka.ilkd.key.logic.PosInOccurrence;
15: import de.uka.ilkd.key.logic.Term;
16: import de.uka.ilkd.key.proof.Goal;
17: import de.uka.ilkd.key.rule.RuleApp;
18: import de.uka.ilkd.key.util.Debug;
19:
20: /**
21: * Returns zero iff the position of a rule application is not below any
22: * operators that bind variables
23: */
24: public class NotBelowBinderFeature extends BinaryFeature {
25:
26: public static final Feature INSTANCE = new NotBelowBinderFeature();
27:
28: private NotBelowBinderFeature() {
29: }
30:
31: public boolean filter(RuleApp app, PosInOccurrence pos, Goal goal) {
32: Debug.assertFalse(pos == null,
33: "Feature is only applicable to rules with find");
34:
35: return !belowBinder(pos);
36: }
37:
38: private boolean belowBinder(PosInOccurrence pos) {
39: final PIOPathIterator it = pos.iterator();
40:
41: while (it.next() != -1) {
42: final Term t = it.getSubTerm();
43:
44: if (t.varsBoundHere(it.getChild()).size() > 0)
45: return true;
46: }
47:
48: return false;
49: }
50:
51: }
|