001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.proof.incclosure;
012:
013: import de.uka.ilkd.key.logic.Constraint;
014: import de.uka.ilkd.key.logic.ConstraintContainer;
015: import de.uka.ilkd.key.logic.IntersectionConstraint;
016: import de.uka.ilkd.key.proof.IteratorOfNode;
017: import de.uka.ilkd.key.proof.Node;
018: import de.uka.ilkd.key.util.Debug;
019:
020: /**
021: * Sink removing given metavariables from passing constraints, thus
022: * making variables local
023: *
024: * This derivative does also detect subtrees which are completely
025: * closed
026: */
027: public class BranchRestricter extends Restricter {
028:
029: Node node = null;
030:
031: /**
032: * Constraint holding the intersection of all branch constraints
033: * (constraints held by the branch sinks) above and at this
034: * restricter's node
035: * this is undefined if node == null
036: */
037: Constraint pathConstraint = Constraint.TOP;
038:
039: /**
040: * PRECONDITION: p_parent != null
041: */
042: public BranchRestricter(Sink p_parent) {
043: super (p_parent);
044: }
045:
046: /*
047: * @param p_node the root of the branch (subtree) this restricter
048: * belongs to
049: */
050: public void setNode(Node p_node) {
051: node = p_node;
052:
053: resetPathConstraint();
054: }
055:
056: /**
057: * Add a constraint for which something (a goal or a subtree of
058: * the proof) can be closed
059: */
060: public void put(Constraint p_c) {
061: super .put(p_c);
062:
063: if (node != null) {
064: if (getParent().getResetConstraint().isBottom())
065: node.subtreeCompletelyClosed();
066:
067: putPathConstraint(getParent().getResetConstraint());
068: }
069: }
070:
071: /**
072: * Remove all constraints that have been inserted with "put" until
073: * now, replacing them with the only constraint "p_c"
074: */
075: public void reset(Constraint p_c) {
076: pathConstraint = null;
077:
078: super .reset(p_c);
079:
080: if (pathConstraint == null)
081: // otherwise the constraint was already reset by a recursive call
082: resetPathConstraint();
083: }
084:
085: /**
086: * Set the "pathConstraint"-attribute to the intersection of all
087: * branch constraints (constraints held by the branch sinks) above
088: * and at this restricter's node, propagate this change downwards
089: *
090: * PRECONDITION: the "pathConstraint"-attributes above this node
091: * are up to date
092: */
093: protected void resetPathConstraint() {
094: Debug.assertTrue(node != null,
095: "Branch restricter doesn't know its branch");
096:
097: pathConstraint = Constraint.TOP;
098:
099: // go upwards to the next BranchRestricter, take its
100: // pathConstraint
101: Node n = node;
102: while (n.getBranchSink() == this && !n.root())
103: n = n.parent();
104:
105: if (n.getBranchSink() != this ) {
106: Sink sink = n.getBranchSink();
107: if (sink instanceof BranchRestricter)
108: pathConstraint = ((BranchRestricter) sink)
109: .getPathConstraint();
110: }
111:
112: resetPathConstraint(pathConstraint);
113: }
114:
115: /**
116: * Set the "pathConstraint"-attribute to the intersection of p_c
117: * with the local branch constraint, propagate this change
118: * downwards
119: */
120: protected void resetPathConstraint(Constraint p_c) {
121: pathConstraint = IntersectionConstraint.intersect(getParent()
122: .getResetConstraint(), p_c);
123:
124: IteratorOfNode it = nextNodesBelow();
125: Sink sink;
126:
127: while (it.hasNext()) {
128: sink = it.next().getBranchSink();
129: if (sink instanceof BranchRestricter)
130: ((BranchRestricter) sink)
131: .resetPathConstraint(pathConstraint);
132: }
133: }
134:
135: /**
136: * Intersect the "pathConstraint"-attribute with p_c, propagate
137: * this change downwards
138: */
139: protected void putPathConstraint(Constraint p_c) {
140: ConstraintContainer cc = new ConstraintContainer();
141:
142: pathConstraint = IntersectionConstraint.intersect(
143: pathConstraint, p_c, cc);
144:
145: if (cc.val().isSatisfiable()) {
146: IteratorOfNode it = nextNodesBelow();
147: Sink sink;
148:
149: while (it.hasNext()) {
150: sink = it.next().getBranchSink();
151: if (sink instanceof BranchRestricter)
152: ((BranchRestricter) sink).putPathConstraint(cc
153: .val());
154: }
155: }
156: }
157:
158: /**
159: * @return Constraint holding the intersection of all branch
160: * constraints (constraints held by the branch sinks) above and at
161: * this restricter's node
162: */
163: public Constraint getPathConstraint() {
164: return pathConstraint;
165: }
166:
167: /**
168: * From "node" go downwards within the proof tree to the next node
169: * with more than one child, return an iterator of the children
170: */
171: private IteratorOfNode nextNodesBelow() {
172: Node n;
173:
174: Debug.assertTrue(node != null,
175: "Branch restricter doesn't know its branch");
176:
177: n = node;
178: while (n.childrenCount() == 1)
179: n = n.child(0);
180:
181: return n.childrenIterator();
182: }
183:
184: }
|