--- /dev/null
+/********************* */
+/*! \file union_find.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Path-compressing, backtrackable union-find using an undo
+ ** stack
+ **
+ ** Path-compressing, backtrackable union-find using an undo stack
+ ** rather than storing items in a CDMap<>.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__UF__MORGAN__UNION_FIND_H
+#define __CVC4__THEORY__UF__MORGAN__UNION_FIND_H
+
+#include <utility>
+#include <vector>
+#include <ext/hash_map>
+
+#include "expr/node.h"
+#include "context/cdo.h"
+
+namespace CVC4 {
+
+namespace context {
+ class Context;
+}/* CVC4::context namespace */
+
+namespace theory {
+namespace uf {
+namespace morgan {
+
+// NodeType \in { Node, TNode }
+template <class NodeType, class NodeHash>
+class UnionFind : context::ContextNotifyObj {
+ /** Our underlying map type. */
+ typedef __gnu_cxx::hash_map<NodeType, NodeType, NodeHash> MapType;
+
+ /**
+ * Our map of Nodes to their canonical representatives.
+ * If a Node is not present in the map, it is its own
+ * representative.
+ */
+ MapType d_map;
+
+ /** Our undo stack for changes made to d_map. */
+ std::vector<std::pair<TNode, TNode> > d_trace;
+
+ /** Our current offset in the d_trace stack (context-dependent). */
+ context::CDO<size_t> d_offset;
+
+public:
+ UnionFind(context::Context* ctxt) :
+ context::ContextNotifyObj(ctxt),
+ d_offset(ctxt, 0) {
+ }
+
+ ~UnionFind() throw() { }
+
+ /**
+ * Return a Node's union-find representative, doing path compression.
+ */
+ inline TNode find(TNode n);
+
+ /**
+ * Return a Node's union-find representative, NOT doing path compression.
+ * This is useful for Assert() statements, debug checking, and similar
+ * things that you do NOT want to mutate the structure.
+ */
+ inline TNode debugFind(TNode n) const;
+
+ /**
+ * Set the canonical representative of n to newParent. They should BOTH
+ * be their own canonical representatives on entry to this funciton.
+ */
+ inline void setCanon(TNode n, TNode newParent);
+
+ /**
+ * Called by the Context when a pop occurs. Cancels everything to the
+ * current context level. Overrides ContextNotifyObj::notify().
+ */
+ void notify();
+
+};/* class UnionFind<> */
+
+template <class NodeType, class NodeHash>
+inline TNode UnionFind<NodeType, NodeHash>::debugFind(TNode n) const {
+ typename MapType::const_iterator i = d_map.find(n);
+ if(i == d_map.end()) {
+ return n;
+ } else {
+ return debugFind((*i).second);
+ }
+}
+
+template <class NodeType, class NodeHash>
+inline TNode UnionFind<NodeType, NodeHash>::find(TNode n) {
+ Trace("ufuf") << "UFUF find of " << n << endl;
+ typename MapType::iterator i = d_map.find(n);
+ if(i == d_map.end()) {
+ Trace("ufuf") << "UFUF it is rep" << endl;
+ return n;
+ } else {
+ Trace("ufuf") << "UFUF not rep: par is " << (*i).second << endl;
+ pair<TNode, TNode> pr = *i;
+ // our iterator is invalidated by the recursive call to find(),
+ // since it mutates the map
+ TNode p = find(pr.second);
+ if(p == pr.second) {
+ return p;
+ }
+ d_trace.push_back(make_pair(n, pr.second));
+ d_offset = d_trace.size();
+ Trace("ufuf") << "UFUF setting canon of " << n << " : " << p << " @ " << d_trace.size() << endl;
+ pr.second = p;
+ d_map.insert(pr);
+ return p;
+ }
+}
+
+template <class NodeType, class NodeHash>
+inline void UnionFind<NodeType, NodeHash>::setCanon(TNode n, TNode newParent) {
+ Assert(d_map.find(n) == d_map.end());
+ Assert(d_map.find(newParent) == d_map.end());
+ Trace("ufuf") << "UFUF setting canon of " << n << " : " << newParent << " @ " << d_trace.size() << endl;
+ d_map[n] = newParent;
+ d_trace.push_back(make_pair(n, TNode::null()));
+ d_offset = d_trace.size();
+}
+
+}/* CVC4::theory::uf::morgan namespace */
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /*__CVC4__THEORY__UF__MORGAN__UNION_FIND_H */
#include "context/cdset.h"
#include "context/cdlist_context_memory.h"
#include "util/exception.h"
+#include "theory/uf/morgan/stacking_map.h"
namespace CVC4 {
OutputChannel* d_out;
// typedef all of these so that iterators are easy to define
- typedef context::CDMap<Node, Node, NodeHashFunction> RepresentativeMap;
+ typedef theory::uf::morgan::StackingMap <Node, NodeHashFunction> RepresentativeMap;
typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > ClassList;
typedef context::CDMap<Node, ClassList*, NodeHashFunction> ClassLists;
typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > UseList;
typedef context::CDMap<Node, Node, NodeHashFunction> ProofMap;
typedef context::CDMap<Node, Node, NodeHashFunction> ProofLabel;
+ // Simple, NON-context-dependent pending list, union find and "seen
+ // set" types for constructing explanations and
+ // nearestCommonAncestor(); see explain().
+ typedef std::list<std::pair<Node, Node> > PendingProofList_t;
+ typedef __gnu_cxx::hash_map<TNode, TNode, TNodeHashFunction> UnionFind_t;
+ typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> SeenSet_t;
+
RepresentativeMap d_representative;
ClassLists d_classList;
UseLists d_useList;
}
}
- TNode proofRewrite(TNode pfStep) {
+ TNode proofRewrite(TNode pfStep) const {
ProofMap::const_iterator i = d_proofRewrite.find(pfStep);
if(i == d_proofRewrite.end()) {
return pfStep;
* Find the EC representative for a term t in the current context.
*/
inline TNode find(TNode t) const throw(AssertionException) {
- context::CDMap<Node, Node, NodeHashFunction>::iterator i =
- d_representative.find(t);
- return (i == d_representative.end()) ? t : TNode((*i).second);
+ TNode rep1 = d_representative.find(t);
+ return rep1.isNull() ? t : rep1;
}
- void explainAlongPath(TNode a, TNode c, std::list<std::pair<Node, Node> >& pending, __gnu_cxx::hash_map<Node, Node, NodeHashFunction>& unionFind, std::list<Node>& pf)
+ void explainAlongPath(TNode a, TNode c, PendingProofList_t& pending, UnionFind_t& unionFind, std::list<Node>& pf)
throw(AssertionException);
- Node highestNode(TNode a, __gnu_cxx::hash_map<Node, Node, NodeHashFunction>& unionFind)
+ Node highestNode(TNode a, UnionFind_t& unionFind) const
throw(AssertionException);
- Node nearestCommonAncestor(TNode a, TNode b)
+ Node nearestCommonAncestor(TNode a, TNode b, UnionFind_t& unionFind)
throw(AssertionException);
/**
* Internal lookup mapping from tuples to equalities.
*/
inline TNode lookup(TNode a) const {
- context::CDMap<Node, Node, NodeHashFunction>::iterator i = d_lookup.find(a);
+ LookupMap::iterator i = d_lookup.find(a);
if(i == d_lookup.end()) {
return TNode::null();
} else {
* Append equality "eq" to uselist of "of".
*/
inline void appendToUseList(TNode of, TNode eq) {
- Debug("cc") << "adding " << eq << " to use list of " << of << std::endl;
+ Trace("cc") << "adding " << eq << " to use list of " << of << std::endl;
Assert(eq.getKind() == kind::EQUAL ||
eq.getKind() == kind::IFF);
Assert(of == find(of));
void CongruenceClosure<OutputChannel>::addEq(TNode eq, TNode inputEq) {
d_proofRewrite[eq] = inputEq;
- if(Debug.isOn("cc")) {
- Debug("cc") << "CC addEq[" << d_context->getLevel() << "]: " << eq << std::endl;
+ if(Trace.isOn("cc")) {
+ Trace("cc") << "CC addEq[" << d_context->getLevel() << "]: " << eq << std::endl;
}
Assert(eq.getKind() == kind::EQUAL ||
eq.getKind() == kind::IFF);
Assert(eq[1].getKind() != kind::APPLY_UF);
if(areCongruent(eq[0], eq[1])) {
- Debug("cc") << "CC -- redundant, ignoring...\n";
+ Trace("cc") << "CC -- redundant, ignoring...\n";
return;
}
Assert(s != t);
- Debug("cc:detail") << "CC " << s << " == " << t << std::endl;
+ Trace("cc:detail") << "CC " << s << " == " << t << std::endl;
// change from paper: do this whether or not s, t are applications
- Debug("cc:detail") << "CC propagating the eq" << std::endl;
+ Trace("cc:detail") << "CC propagating the eq" << std::endl;
if(s.getKind() != kind::APPLY_UF) {
// s, t are constants
// s is an apply, t is a constant
Node ap = buildRepresentativesOfApply(s);
- Debug("cc:detail") << "CC rewrLHS " << "op_and_args_a == " << t << std::endl;
- Debug("cc") << "CC ap is " << ap << std::endl;
+ Trace("cc:detail") << "CC rewrLHS " << "op_and_args_a == " << t << std::endl;
+ Trace("cc") << "CC ap is " << ap << std::endl;
TNode l = lookup(ap);
- Debug("cc:detail") << "CC lookup(ap): " << l << std::endl;
+ Trace("cc:detail") << "CC lookup(ap): " << l << std::endl;
if(!l.isNull()) {
// ensure a hard Node link exists to this during the call
Node pending = NodeManager::currentNM()->mkNode(kind::TUPLE, eq, l);
- Debug("cc:detail") << "pending1 " << pending << std::endl;
+ Trace("cc:detail") << "pending1 " << pending << std::endl;
propagate(pending);
} else {
- Debug("cc") << "CC lookup(ap) setting to " << eq << std::endl;
+ Trace("cc") << "CC lookup(ap) setting to " << eq << std::endl;
setLookup(ap, eq);
for(Node::iterator i = ap.begin(); i != ap.end(); ++i) {
appendToUseList(*i, eq);
}
}
}
-
- Debug("cc") << *this;
}/* addEq() */
throw(AssertionException) {
Assert(apply.getKind() == kind::APPLY_UF);
NodeBuilder<> argspb(kindToBuild);
+ // FIXME probably don't have to do find() of operator
argspb << find(apply.getOperator());
for(TNode::iterator i = apply.begin(); i != apply.end(); ++i) {
argspb << find(*i);
template <class OutputChannel>
void CongruenceClosure<OutputChannel>::propagate(TNode seed) {
- Debug("cc:detail") << "=== doing a round of propagation ===" << std::endl
+ Trace("cc:detail") << "=== doing a round of propagation ===" << std::endl
<< "the \"seed\" propagation is: " << seed << std::endl;
std::list<Node> pending;
- Debug("cc") << "seed propagation with: " << seed << std::endl;
+ Trace("cc") << "seed propagation with: " << seed << std::endl;
pending.push_back(seed);
do { // while(!pending.empty())
Node e = pending.front();
pending.pop_front();
- Debug("cc") << "=== top of propagate loop ===" << std::endl
+ Trace("cc") << "=== top of propagate loop ===" << std::endl
<< "=== e is " << e << " ===" << std::endl;
TNode a, b;
a = e[0];
b = e[1];
- Debug("cc:detail") << "propagate equality: " << a << " == " << b << std::endl;
+ Trace("cc:detail") << "propagate equality: " << a << " == " << b << std::endl;
} else {
// e is a tuple ( apply f A... = a , apply f B... = b )
- Debug("cc") << "propagate tuple: " << e << "\n";
+ Trace("cc") << "propagate tuple: " << e << "\n";
Assert(e.getKind() == kind::TUPLE);
Assert(a.getKind() != kind::APPLY_UF);
Assert(b.getKind() != kind::APPLY_UF);
- Debug("cc") << " ( " << a << " , " << b << " )" << std::endl;
+ Trace("cc") << " ( " << a << " , " << b << " )" << std::endl;
}
if(Debug.isOn("cc")) {
- Debug("cc:detail") << "=====at start=====" << std::endl
+ Trace("cc:detail") << "=====at start=====" << std::endl
<< "a :" << a << std::endl
<< "NORMALIZE a:" << normalize(a) << std::endl
<< "b :" << b << std::endl
Node ap = find(a), bp = find(b);
if(ap != bp) {
- Debug("cc:detail") << "EC[a] == " << ap << std::endl
+ Trace("cc:detail") << "EC[a] == " << ap << std::endl
<< "EC[b] == " << bp << std::endl;
{ // w.l.o.g., |classList ap| <= |classList bp|
ClassLists::iterator cl_bpi = d_classList.find(bp);
unsigned sizeA = (cl_api == d_classList.end() ? 0 : (*cl_api).second->size());
unsigned sizeB = (cl_bpi == d_classList.end() ? 0 : (*cl_bpi).second->size());
- Debug("cc") << "sizeA == " << sizeA << " sizeB == " << sizeB << std::endl;
+ Trace("cc") << "sizeA == " << sizeA << " sizeB == " << sizeB << std::endl;
if(sizeA > sizeB) {
- Debug("cc") << "swapping..\n";
+ Trace("cc") << "swapping..\n";
TNode tmp = ap; ap = bp; bp = tmp;
tmp = a; a = b; b = tmp;
}
cl_bp = new(d_context->getCMM()) ClassList(true, d_context, false,
context::ContextMemoryAllocator<TNode>(d_context->getCMM()));
d_classList.insertDataFromContextMemory(bp, cl_bp);
- Debug("cc:detail") << "CC in prop alloc classlist for " << bp << std::endl;
+ Trace("cc:detail") << "CC in prop alloc classlist for " << bp << std::endl;
} else {
cl_bp = (*cl_bpi).second;
}
// we don't store 'ap' in its own class list; so process it here
- Debug("cc:detail") << "calling mergeproof/merge1 " << ap
+ Trace("cc:detail") << "calling mergeproof/merge1 " << ap
<< " AND " << bp << std::endl;
mergeProof(a, b, e);
merge(ap, bp);
- Debug("cc") << " adding ap == " << ap << std::endl
+ Trace("cc") << " adding ap == " << ap << std::endl
<< " to class list of " << bp << std::endl;
cl_bp->push_back(ap);
ClassLists::const_iterator cli = d_classList.find(ap);
Debug("cc") << " it's find ptr is: " << find(c) << std::endl;
}
Assert(find(c) == ap);
- Debug("cc:detail") << "calling merge2 " << c << bp << std::endl;
+ Trace("cc:detail") << "calling merge2 " << c << bp << std::endl;
merge(c, bp);
// move c from classList(ap) to classlist(bp);
//i = cl.erase(i);// FIXME do we need to?
- Debug("cc") << " adding c to class list of " << bp << std::endl;
+ Trace("cc") << " adding c to class list of " << bp << std::endl;
cl_bp->push_back(c);
}
}
- Debug("cc:detail") << "bottom\n";
+ Trace("cc:detail") << "bottom\n";
}
{ // use list handling
i != ul->end();
++i) {
TNode eq = *i;
- Debug("cc") << "CC -- useList: " << eq << std::endl;
+ Trace("cc") << "CC -- useList: " << eq << std::endl;
Assert(eq.getKind() == kind::EQUAL ||
eq.getKind() == kind::IFF);
// change from paper
// if lookup(c1',c2') is some f(d1,d2)=d then
TNode n = lookup(cp);
- Debug("cc:detail") << "CC -- c' is " << cp << std::endl;
+ Trace("cc:detail") << "CC -- c' is " << cp << std::endl;
if(!n.isNull()) {
- Debug("cc:detail") << "CC -- lookup(c') is " << n << std::endl;
+ Trace("cc:detail") << "CC -- lookup(c') is " << n << std::endl;
// add (f(c1,c2)=c,f(d1,d2)=d) to pending
Node tuple = NodeManager::currentNM()->mkNode(kind::TUPLE, eq, n);
- Debug("cc") << "CC add tuple to pending: " << tuple << std::endl;
+ Trace("cc") << "CC add tuple to pending: " << tuple << std::endl;
pending.push_back(tuple);
// remove f(c1,c2)=c from UseList(ap)
- Debug("cc:detail") << "supposed to remove " << eq << std::endl
+ Trace("cc:detail") << "supposed to remove " << eq << std::endl
<< " from UseList of " << ap << std::endl;
//i = ul.erase(i);// FIXME do we need to?
} else {
- Debug("cc") << "CC -- lookup(c') is null" << std::endl;
- Debug("cc") << "CC -- setlookup(c') to " << eq << std::endl;
+ Trace("cc") << "CC -- lookup(c') is null" << std::endl;
+ Trace("cc") << "CC -- setlookup(c') to " << eq << std::endl;
// set lookup(c1',c2') to f(c1,c2)=c
setLookup(cp, eq);
// move f(c1,c2)=c from UseList(ap) to UseList(b')
}
}
}/* use lists */
- Debug("cc:detail") << "CC in prop done with useList of " << ap << std::endl;
+ Trace("cc:detail") << "CC in prop done with useList of " << ap << std::endl;
} else {
- Debug("cc:detail") << "CCs the same ( == " << ap << "), do nothing." << std::endl;
+ Trace("cc:detail") << "CCs the same ( == " << ap << "), do nothing." << std::endl;
}
if(Debug.isOn("cc")) {
}
*/
- Debug("cc") << "CC setting rep of " << ec1 << std::endl;
- Debug("cc") << "CC to " << ec2 << std::endl;
+ Trace("cc") << "CC setting rep of " << ec1 << std::endl;
+ Trace("cc") << "CC to " << ec2 << std::endl;
/* can now be applications
Assert(ec1.getKind() != kind::APPLY_UF);
//Assert(find(ec1) == ec1);
Assert(find(ec2) == ec2);
- d_representative[ec1] = ec2;
+ d_representative.set(ec1, ec2);
if(d_careSet.find(ec1) != d_careSet.end()) {
d_careSet.insert(ec2);
template <class OutputChannel>
void CongruenceClosure<OutputChannel>::mergeProof(TNode a, TNode b, TNode e) {
- Debug("cc") << " -- merge-proofing " << a << "\n"
+ Trace("cc") << " -- merge-proofing " << a << "\n"
<< " and " << b << "\n"
<< " with " << e << "\n";
// proof forest gets a -> b labeled with e
// first reverse all the edges in proof forest to root of this proof tree
- Debug("cc") << "CC PROOF reversing proof tree\n";
+ Trace("cc") << "CC PROOF reversing proof tree\n";
// c and p are child and parent in (old) proof tree
Node c = a, p = d_proof[a], edgePf = d_proofLabel[a];
// when we hit null p, we're at the (former) root
- Debug("cc") << "CC PROOF start at c == " << c << std::endl
+ Trace("cc") << "CC PROOF start at c == " << c << std::endl
<< " p == " << p << std::endl
<< " edgePf == " << edgePf << std::endl;
while(!p.isNull()) {
c = p;
p = pParSave;
edgePf = pLabelSave;
- Debug("cc") << "CC PROOF now at c == " << c << std::endl
+ Trace("cc") << "CC PROOF now at c == " << c << std::endl
<< " p == " << p << std::endl
<< " edgePf == " << edgePf << std::endl;
}
template <class OutputChannel>
Node CongruenceClosure<OutputChannel>::normalize(TNode t) const
throw(AssertionException) {
- Debug("cc:detail") << "normalize " << t << std::endl;
+ Trace("cc:detail") << "normalize " << t << std::endl;
if(t.getKind() != kind::APPLY_UF) {// t is a constant
t = find(t);
- Debug("cc:detail") << " find " << t << std::endl;
+ Trace("cc:detail") << " find " << t << std::endl;
return t;
} else {// t is an apply
NodeBuilder<> apb(kind::TUPLE);
}
Node ap = apb;
- Debug("cc:detail") << " got ap " << ap << std::endl;
+ Trace("cc:detail") << " got ap " << ap << std::endl;
Node theLookup = lookup(ap);
if(allConstants && !theLookup.isNull()) {
}/* normalize() */
+// This is the find() operation for the auxiliary union-find. This
+// union-find is not context-dependent, as it's used only during
+// explain(). It does path compression.
template <class OutputChannel>
-Node CongruenceClosure<OutputChannel>::highestNode(TNode a, __gnu_cxx::hash_map<Node, Node, NodeHashFunction>& unionFind)
+Node CongruenceClosure<OutputChannel>::highestNode(TNode a, UnionFind_t& unionFind) const
throw(AssertionException) {
- __gnu_cxx::hash_map<Node, Node, NodeHashFunction>::iterator i = unionFind.find(a);
+ UnionFind_t::iterator i = unionFind.find(a);
if(i == unionFind.end()) {
return a;
} else {
template <class OutputChannel>
-void CongruenceClosure<OutputChannel>::explainAlongPath(TNode a, TNode c, std::list<std::pair<Node, Node> >& pending, __gnu_cxx::hash_map<Node, Node, NodeHashFunction>& unionFind, std::list<Node>& pf)
+void CongruenceClosure<OutputChannel>::explainAlongPath(TNode a, TNode c, PendingProofList_t& pending, UnionFind_t& unionFind, std::list<Node>& pf)
throw(AssertionException) {
a = highestNode(a, unionFind);
template <class OutputChannel>
-Node CongruenceClosure<OutputChannel>::nearestCommonAncestor(TNode a, TNode b)
+Node CongruenceClosure<OutputChannel>::nearestCommonAncestor(TNode a, TNode b, UnionFind_t& unionFind)
throw(AssertionException) {
+ SeenSet_t seen;
+
Assert(find(a) == find(b));
- return find(a); // FIXME
+
+ do {
+ a = highestNode(a, unionFind);
+ seen.insert(a);
+ a = d_proof[a];
+ } while(!a.isNull());
+
+ for(;;) {
+ b = highestNode(b, unionFind);
+ if(seen.find(b) != seen.end()) {
+ return b;
+ }
+ b = d_proof[b];
+
+ Assert(!b.isNull());
+ }
}/* nearestCommonAncestor() */
b = replace(flatten(b));
}
- std::list<std::pair<Node, Node> > pending;
- __gnu_cxx::hash_map<Node, Node, NodeHashFunction> unionFind;
+ PendingProofList_t pending;
+ UnionFind_t unionFind;
std::list<Node> terms;
pending.push_back(std::make_pair(a, b));
- Debug("cc") << "CC EXPLAINING " << a << " == " << b << std::endl;
+ Trace("cc") << "CC EXPLAINING " << a << " == " << b << std::endl;
do {// while(!pending.empty())
std::pair<Node, Node> eq = pending.front();
a = eq.first;
b = eq.second;
- Node c = nearestCommonAncestor(a, b);
+ Node c = nearestCommonAncestor(a, b, unionFind);
explainAlongPath(a, c, pending, unionFind, terms);
explainAlongPath(b, c, pending, unionFind, terms);
} while(!pending.empty());
- if(Debug.isOn("cc")) {
- Debug("cc") << "CC EXPLAIN final proof has size " << terms.size() << std::endl;
+ if(Trace.isOn("cc")) {
+ Trace("cc") << "CC EXPLAIN final proof has size " << terms.size() << std::endl;
}
NodeBuilder<> pf(kind::AND);
while(!terms.empty()) {
Node p = terms.front();
terms.pop_front();
- Debug("cc") << "CC EXPLAIN " << p << std::endl;
+ Trace("cc") << "CC EXPLAIN " << p << std::endl;
p = proofRewrite(p);
- Debug("cc") << " rewrite " << p << std::endl;
+ Trace("cc") << " rewrite " << p << std::endl;
if(!p.isNull()) {
pf << p;
}
}
- Debug("cc") << "CC EXPLAIN done" << std::endl;
+ Trace("cc") << "CC EXPLAIN done" << std::endl;
Assert(pf.getNumChildren() > 0);
const CongruenceClosure<OutputChannel>& cc) {
out << "==============================================" << std::endl;
- out << "Representatives:" << std::endl;
+ /*out << "Representatives:" << std::endl;
for(typename CongruenceClosure<OutputChannel>::RepresentativeMap::const_iterator i = cc.d_representative.begin(); i != cc.d_representative.end(); ++i) {
out << " " << (*i).first << " => " << (*i).second << std::endl;
- }
+ }*/
out << "ClassLists:" << std::endl;
for(typename CongruenceClosure<OutputChannel>::ClassLists::const_iterator i = cc.d_classList.begin(); i != cc.d_classList.end(); ++i) {