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.termgenerator;
12:
13: import java.util.Stack;
14:
15: import de.uka.ilkd.key.logic.IteratorOfTerm;
16: import de.uka.ilkd.key.logic.PosInOccurrence;
17: import de.uka.ilkd.key.logic.Term;
18: import de.uka.ilkd.key.logic.op.Op;
19: import de.uka.ilkd.key.logic.op.Operator;
20: import de.uka.ilkd.key.proof.Goal;
21: import de.uka.ilkd.key.rule.RuleApp;
22:
23: /**
24: * Enumerate potential subformulas of a formula that could be used for a cut
25: * (taclet cut_direct). This term-generator does not descend below quantifiers,
26: * only below propositional junctors
27: */
28: public class AllowedCutPositionsGenerator implements TermGenerator {
29:
30: private AllowedCutPositionsGenerator() {
31: }
32:
33: public final static TermGenerator INSTANCE = new AllowedCutPositionsGenerator();
34:
35: public IteratorOfTerm generate(RuleApp app, PosInOccurrence pos,
36: Goal goal) {
37: return new Iterator(pos.constrainedFormula().formula(), pos
38: .isInAntec());
39: }
40:
41: private class Iterator implements IteratorOfTerm {
42: private final Stack termStack = new Stack();
43:
44: public Iterator(Term t, boolean negated) {
45: push(t, negated);
46: }
47:
48: private void push(Term t, boolean negated) {
49: termStack.push(t);
50: termStack.push(Boolean.valueOf(negated));
51: }
52:
53: public boolean hasNext() {
54: return !termStack.isEmpty();
55: }
56:
57: public Term next() {
58: final boolean negated = ((Boolean) termStack.pop())
59: .booleanValue();
60: final Term res = (Term) termStack.pop();
61: final Operator op = res.op();
62:
63: if (op == Op.NOT) {
64: push(res.sub(0), !negated);
65: } else if (op == (negated ? Op.OR : Op.AND)) {
66: push(res.sub(0), negated);
67: push(res.sub(1), negated);
68: } else if (negated && op == Op.IMP) {
69: push(res.sub(0), !negated);
70: push(res.sub(1), negated);
71: }
72:
73: return res;
74: }
75: }
76: }
|