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.PIOPathIterator;
11: import de.uka.ilkd.key.logic.PosInOccurrence;
12: import de.uka.ilkd.key.logic.op.IUpdateOperator;
13: import de.uka.ilkd.key.logic.op.Modality;
14: import de.uka.ilkd.key.logic.op.Operator;
15: import de.uka.ilkd.key.proof.Goal;
16: import de.uka.ilkd.key.rule.RuleApp;
17: import de.uka.ilkd.key.util.Debug;
18:
19: /**
20: * Returns zero iff the position of a rule application is not in the scope of a
21: * modal operator (a program block or an update). Note that terms and formulas
22: * within (but not behind) updates are not in the scope of the update
23: */
24: public class NotInScopeOfModalityFeature extends BinaryFeature {
25:
26: public static final Feature INSTANCE = new NotInScopeOfModalityFeature();
27:
28: private NotInScopeOfModalityFeature() {
29: }
30:
31: protected 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 !inScopeOfModality(pos);
36: }
37:
38: private boolean inScopeOfModality(PosInOccurrence pos) {
39: final PIOPathIterator it = pos.iterator();
40:
41: while (it.next() != -1) {
42: final Operator op = it.getSubTerm().op();
43:
44: if (op instanceof Modality)
45: return true;
46: if (op instanceof IUpdateOperator) {
47: final IUpdateOperator updOp = (IUpdateOperator) op;
48: if (it.getChild() == updOp.targetPos())
49: return true;
50: }
51: }
52:
53: return false;
54: }
55:
56: }
|