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.util.Debug;
015:
016: /**
017: * Class for merging an arbitrary number of constraint streams
018: */
019: public class MultiMerger implements Merger {
020:
021: /**
022: * BinaryMerger are arranged as a balanced binary tree with
023: * rootMerger being the root and leafSinks a list of the leafs'
024: * sinks
025: */
026: private BinaryMerger rootMerger;
027: private ListOfSink leafSinks = SLListOfSink.EMPTY_LIST;
028:
029: private int arity = 0;
030:
031: /**
032: * Parent sink within the tree of sinks
033: */
034: private Sink parent;
035:
036: /**
037: * Services eg. if necessary additional sorts are added
038: * (this can happen during unification)
039: */
040: private Services services;
041:
042: /**
043: * Initial value of the buffers will be the parent's value
044: */
045: public MultiMerger(Sink p_parent, int p_arity, Services p_services) {
046: Debug.assertTrue(p_arity >= 2,
047: "Tried to create MultiMerger with less than 2 sinks");
048:
049: parent = p_parent;
050: services = p_services;
051: expand(p_arity);
052: }
053:
054: /**
055: * Expand the merger, possibly adding new sinks. The old sinks
056: * will remain valid and will be the first elements in the new
057: * list of all sinks. It is much more efficient to create all
058: * needed sinks by a single call than by successive calls.
059: */
060: public void expand(int p_arity) {
061: if (p_arity == arity)
062: return;
063:
064: Debug
065: .assertTrue(p_arity > arity,
066: "Tried to shrink MultiMerger");
067:
068: BinaryMerger r = new BinaryMerger(parent, services);
069: ListOfSink sinkList = SLListOfSink.EMPTY_LIST;
070: ListOfSink newList = SLListOfSink.EMPTY_LIST;
071: IteratorOfSink it;
072: int i;
073:
074: it = r.getSinks();
075: sinkList = sinkList.append(it.next()).append(it.next());
076:
077: if (arity == 0)
078: i = p_arity - 2;
079: else {
080: i = p_arity - arity - 1;
081: rootMerger.setParent(sinkList.head());
082: sinkList = sinkList.tail();
083: }
084:
085: rootMerger = r;
086: arity = p_arity;
087:
088: while (i-- != 0) {
089: if (sinkList == SLListOfSink.EMPTY_LIST) {
090: /** Increase the depth of the tree by one */
091: while (newList != SLListOfSink.EMPTY_LIST) {
092: sinkList = sinkList.prepend(newList.head());
093: newList = newList.tail();
094: }
095: }
096:
097: it = new BinaryMerger(sinkList.head(), services).getSinks();
098: newList = newList.prepend(it.next()).prepend(it.next());
099: sinkList = sinkList.tail();
100: }
101:
102: while (newList != SLListOfSink.EMPTY_LIST) {
103: sinkList = sinkList.prepend(newList.head());
104: newList = newList.tail();
105: }
106:
107: while (sinkList != SLListOfSink.EMPTY_LIST) {
108: leafSinks = leafSinks.append(sinkList.head());
109: sinkList = sinkList.tail();
110: }
111: }
112:
113: public int getArity() {
114: return arity;
115: }
116:
117: /**
118: * Inputs offered by this merger
119: */
120: public IteratorOfSink getSinks() {
121: return leafSinks.iterator();
122: }
123:
124: /**
125: * @return true iff the whole subtree of sinks below this merger
126: * has seen consistent constraints
127: */
128: public boolean isSatisfiable() {
129: return rootMerger.isSatisfiable();
130: }
131:
132: /**
133: * Reparent this merger; an implementing class should make
134: * appropriate "reset"-calls to the new parent
135: */
136: public void setParent(Sink p_parent) {
137: parent = p_parent;
138: rootMerger.setParent(parent);
139: }
140:
141: }
|