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.op.Equality;
16: import de.uka.ilkd.key.logic.op.IUpdateOperator;
17: import de.uka.ilkd.key.proof.Goal;
18: import de.uka.ilkd.key.rule.IfFormulaInstSeq;
19: import de.uka.ilkd.key.rule.IfFormulaInstantiation;
20: import de.uka.ilkd.key.rule.TacletApp;
21: import de.uka.ilkd.key.util.Debug;
22:
23: /**
24: * This feature checks that an equation is not applied to itself. This means
25: * that the focus of the rule application must not be one side of an equation
26: * that is the instantiation of the first if-formula. If the rule application is
27: * admissible, zero is returned.
28: */
29: public class CheckApplyEqFeature extends BinaryTacletAppFeature {
30:
31: public static final Feature INSTANCE = new CheckApplyEqFeature();
32:
33: private CheckApplyEqFeature() {
34: }
35:
36: protected boolean filter(TacletApp p_app, PosInOccurrence pos,
37: Goal goal) {
38: Debug.assertTrue(pos != null, "Need to know the position of "
39: + "the application of the taclet");
40:
41: IfFormulaInstantiation ifInst = p_app.ifFormulaInstantiations()
42: .head();
43:
44: Debug.assertTrue(ifInst != null,
45: "Need to know the equation the taclet"
46: + " is used with");
47:
48: return isNotSelfApplication(pos, ifInst)
49: // && equationIsDirected ( ifInst, p_app.constraint() )
50: ;
51: }
52:
53: private boolean isNotSelfApplication(PosInOccurrence pos,
54: IfFormulaInstantiation ifInst) {
55: if (!(ifInst instanceof IfFormulaInstSeq)
56: || ifInst.getConstrainedFormula() != pos
57: .constrainedFormula()
58: || ((IfFormulaInstSeq) ifInst).inAntec() != pos
59: .isInAntec())
60: return true;
61:
62: // Position may not be one of the terms compared in
63: // the equation
64:
65: final PIOPathIterator it = pos.iterator();
66:
67: it.next();
68:
69: // leading updates are not interesting
70: while (it.getSubTerm().op() instanceof IUpdateOperator) {
71: if (!it.hasNext())
72: return true;
73: it.next();
74: }
75:
76: if (!(it.getSubTerm().op() instanceof Equality)
77: || !it.hasNext())
78: return true;
79:
80: if (it.getChild() == 0)
81: // we don't allow rewriting in the left term of the equation
82: return false;
83:
84: return true;
85: }
86:
87: }
|