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.Sequent;
12: import de.uka.ilkd.key.logic.op.Operator;
13: import de.uka.ilkd.key.logic.op.QuanUpdateOperator;
14: import de.uka.ilkd.key.proof.Goal;
15: import de.uka.ilkd.key.rule.RuleApp;
16: import de.uka.ilkd.key.rule.Taclet;
17:
18: public class InUpdateFeature extends BinaryFeature {
19:
20: private final boolean inUpdateAndAssume;
21: private final boolean splittingRules;
22: private final boolean inInitPhase;
23:
24: private InUpdateFeature(boolean splittingRules,
25: boolean inUpdateAndAssume, boolean inInitPhase) {
26: this .inUpdateAndAssume = inUpdateAndAssume;
27: this .splittingRules = splittingRules;
28: this .inInitPhase = inInitPhase;
29: }
30:
31: //true wenn nicht erlaubt
32:
33: protected boolean filter(RuleApp app, PosInOccurrence pos, Goal goal) {
34: if (app.rule() instanceof Taclet) {
35: Taclet taclet = (Taclet) app.rule();
36: if (taclet.goalTemplates().size() > 1
37: && (!splittingRules || inInitPhase)) {
38: return true;
39: }
40:
41: if (taclet.ifSequent() == Sequent.EMPTY_SEQUENT) {
42: return false;
43: }
44: }
45: return inUpdate(pos) && !inUpdateAndAssume;
46: }
47:
48: public boolean inUpdate(PosInOccurrence pio2) {
49: if (pio2 == null) {
50: return false;
51: }
52: PosInOccurrence pio = pio2;
53: while (!pio.isTopLevel()) {
54: Operator op = pio.up().subTerm().op();
55: if (op instanceof QuanUpdateOperator
56: || op.toString().equals("STATE")) {
57: if (pio.posInTerm().getIndex() < pio.up().subTerm()
58: .arity() - 1) {
59: return true;
60: }
61:
62: }
63: pio = pio.up();
64: }
65: return false;
66: }
67:
68: public boolean inState(PosInOccurrence pio2) {
69: PosInOccurrence pio = pio2;
70: if (pio2 == null) {
71: return false;
72: }
73: while (!pio.isTopLevel()) {
74: Operator op = pio.up().subTerm().op();
75: if (op.toString().equals("STATE")) {
76: return true;
77: }
78: pio = pio.up();
79: }
80:
81: return false;
82: }
83:
84: public static Feature create(boolean isSplittingAllowed,
85: boolean inUpdateAndAssumes, boolean inInitPhase) {
86: return new InUpdateFeature(isSplittingAllowed,
87: inUpdateAndAssumes, inInitPhase);
88: }
89:
90: }
|