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.IntersectionConstraint;
015: import de.uka.ilkd.key.logic.op.Metavariable;
016:
017: /**
018: * Sink buffering all constraints that are pushed using "put",
019: * offering the possibility to reset the tree of sinks
020: */
021: public class BufferSink implements Sink {
022:
023: private Constraint buffer;
024:
025: /**
026: * Parent sink within the tree of sinks. For "parent == null" this
027: * is the root sink
028: */
029: private Sink parent;
030:
031: /**
032: * Initial value of the buffer will be the parent's value
033: */
034: public BufferSink(Sink p_parent) {
035: parent = p_parent;
036:
037: if (parent == null)
038: buffer = Constraint.TOP;
039: else
040: buffer = parent.getResetConstraint();
041: }
042:
043: /**
044: * @return the buffered constraint
045: */
046: public Constraint getConstraint() {
047: return buffer;
048: }
049:
050: public boolean isSatisfiable() {
051: return buffer.isSatisfiable();
052: }
053:
054: /**
055: * Add a constraint for which something (a goal or a subtree of
056: * the proof) can be closed
057: */
058: public void put(Constraint p_c) {
059: if (p_c.isSatisfiable()) {
060: if (parent == null)
061: buffer = IntersectionConstraint.intersect(buffer, p_c);
062: else {
063: parent.put(p_c);
064: buffer = parent.getResetConstraint();
065: }
066: }
067: }
068:
069: /**
070: * Tell the first restricter (possibly this sink) to remove "p_mv"
071: * from any passing constraint
072: */
073: public void addRestriction(Metavariable p_mv) {
074: if (parent != null)
075: parent.addRestriction(p_mv);
076: }
077:
078: /**
079: * @return a constraint that restores the current state of this
080: * sink and its parents if used with "reset"
081: */
082: public Constraint getResetConstraint() {
083: return buffer;
084: }
085:
086: /**
087: * Remove all constraints that have been inserted with "put" until
088: * now, replacing them with the only constraint "p_c"
089: */
090: public void reset(Constraint p_c) {
091: buffer = p_c;
092: if (parent != null)
093: parent.reset(p_c);
094: }
095:
096: public void reset() {
097: reset(buffer);
098: }
099:
100: }
|