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.java.Services;
014: import de.uka.ilkd.key.logic.Constraint;
015: import de.uka.ilkd.key.logic.ConstraintContainer;
016: import de.uka.ilkd.key.logic.IntersectionConstraint;
017: import de.uka.ilkd.key.logic.op.Metavariable;
018:
019: /**
020: * Class for merging two constraint streams
021: */
022: public class BinaryMerger implements Merger {
023:
024: private MergerSink leftSink = new MergerSink();
025: private MergerSink rightSink = new MergerSink();
026:
027: /**
028: * Parent sink within the tree of sinks
029: */
030: private Sink parent;
031:
032: /**
033: * Services eg. if necessary additional sorts are added
034: * (this can happen during unification)
035: */
036: private Services services;
037:
038: /**
039: * Initial value of the buffers will be the parent's value
040: */
041: public BinaryMerger(Sink p_parent, Services p_services) {
042: parent = p_parent;
043:
044: leftSink.otherSink = rightSink;
045: rightSink.otherSink = leftSink;
046:
047: leftSink.buffer = parent.getResetConstraint();
048: rightSink.buffer = parent.getResetConstraint();
049:
050: services = p_services;
051: }
052:
053: /**
054: * Inputs offered by this merger
055: */
056: public IteratorOfSink getSinks() {
057: return SLListOfSink.EMPTY_LIST.prepend(rightSink).prepend(
058: leftSink).iterator();
059: }
060:
061: /**
062: * Reparent this merger; an implementing class should make
063: * appropriate "reset"-calls to the new parent
064: */
065: public void setParent(Sink p_parent) {
066: parent = p_parent;
067: parent.reset(leftSink.buffer.join(rightSink.buffer, services));
068: }
069:
070: /**
071: * @return true iff the whole subtree of sinks below this merger
072: * has seen consistent constraints
073: */
074: public boolean isSatisfiable() {
075: return leftSink.buffer.join(rightSink.buffer, services)
076: .isSatisfiable();
077: }
078:
079: private class MergerSink implements Sink {
080:
081: public MergerSink otherSink;
082:
083: public Constraint buffer;
084:
085: /**
086: * Add a constraint for which something (a goal or a subtree of
087: * the proof) can be closed
088: * @return a constraint representing the intersection of all
089: * constraints that have been pushed until now (including "p_c")
090: */
091: public void put(Constraint p_c) {
092: if (p_c.isSatisfiable()) {
093: ConstraintContainer cc = new ConstraintContainer();
094: buffer = IntersectionConstraint.intersect(buffer, p_c,
095: cc);
096: p_c = cc.val().join(otherSink.buffer, services);
097:
098: if (p_c.isSatisfiable())
099: parent.put(p_c);
100: }
101: }
102:
103: /**
104: * Tell the first restricter (possibly this sink) to remove "p_mv"
105: * from any passing constraint
106: *
107: * Restrictions should not leave its branches
108: */
109: public void addRestriction(Metavariable p_mv) {
110: }
111:
112: /**
113: * @return a constraint that restores the current state of this
114: * sink and its parents if used with "reset"
115: */
116: public Constraint getResetConstraint() {
117: return buffer;
118: }
119:
120: /**
121: * Remove all constraints that have been inserted with "put" until
122: * now, replacing them with the only constraint "p_c"
123: */
124: public void reset(Constraint p_c) {
125: buffer = p_c;
126: parent.reset(buffer.join(otherSink.buffer, services));
127: }
128:
129: }
130:
131: }
|