From: Morgan Deters Date: Wed, 17 Nov 2010 01:39:37 +0000 (+0000) Subject: The "UF engineering issues" release, after much profiling. X-Git-Tag: cvc5-1.0.0~8729 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c7a70635797fe4205b27d29546dd4fe763220794;p=cvc5.git The "UF engineering issues" release, after much profiling. * swap in backtracking data structures (that use and maintain their own undo stack) in some places instead of the usual Context-aware paradigm (MUCH faster). * cosmetic changes to UF, CC modules. --- diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index f27e61544..48f983b3f 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -618,18 +618,18 @@ Node TheoryEngine::getValue(TNode node) { }/* TheoryEngine::getValue(TNode node) */ -bool TheoryEngine::presolve(){ +bool TheoryEngine::presolve() { d_theoryOut.d_conflictNode = Node::null(); d_theoryOut.d_propagatedLiterals.clear(); try { - //d_uf->presolve(); + d_uf->presolve(); d_arith->presolve(); //d_arrays->presolve(); //d_bv->presolve(); } catch(const theory::Interrupted&) { Debug("theory") << "TheoryEngine::presolve() => conflict" << std::endl; } - // Return wheather we have a conflict + // Return whether we have a conflict return d_theoryOut.d_conflictNode.get().isNull(); } diff --git a/src/theory/uf/morgan/Makefile.am b/src/theory/uf/morgan/Makefile.am index e9faa88df..886178a6f 100644 --- a/src/theory/uf/morgan/Makefile.am +++ b/src/theory/uf/morgan/Makefile.am @@ -7,6 +7,10 @@ noinst_LTLIBRARIES = libufmorgan.la libufmorgan_la_SOURCES = \ theory_uf_morgan.h \ - theory_uf_morgan.cpp + theory_uf_morgan.cpp \ + union_find.h \ + union_find.cpp \ + stacking_map.h \ + stacking_map.cpp EXTRA_DIST = diff --git a/src/theory/uf/morgan/stacking_map.cpp b/src/theory/uf/morgan/stacking_map.cpp new file mode 100644 index 000000000..16a85e71b --- /dev/null +++ b/src/theory/uf/morgan/stacking_map.cpp @@ -0,0 +1,83 @@ +/********************* */ +/*! \file stacking_map.cpp + ** \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 Backtrackable map using an undo stack + ** + ** Backtrackable map using an undo stack rather than storing items in + ** a CDMap<>. + **/ + +#include + +#include "theory/uf/morgan/stacking_map.h" +#include "util/Assert.h" +#include "expr/node.h" + +using namespace std; + +namespace CVC4 { +namespace theory { +namespace uf { +namespace morgan { + +template +TNode StackingMap::find(TNode n) const { + typename MapType::const_iterator i = d_map.find(n); + if(i == d_map.end()) { + return TNode(); + } else { + return (*i).second; + } +} + +template +void StackingMap::set(TNode n, TNode newValue) { + Trace("ufsm") << "UFSM setting " << n << " : " << newValue << " @ " << d_trace.size() << endl; + NodeType& ref = d_map[n]; + d_trace.push_back(make_pair(n, TNode(ref))); + d_offset = d_trace.size(); + ref = newValue; +} + +template +void StackingMap::notify() { + Trace("ufsm") << "UFSM cancelling : " << d_offset << " < " << d_trace.size() << " ?" << endl; + while(d_offset < d_trace.size()) { + pair p = d_trace.back(); + if(p.second.isNull()) { + d_map.erase(p.first); + Trace("ufsm") << "UFSM " << d_trace.size() << " erasing " << p.first << endl; + } else { + d_map[p.first] = p.second; + Trace("ufsm") << "UFSM " << d_trace.size() << " replacing " << p << endl; + } + d_trace.pop_back(); + } + Trace("ufufsm") << "UFSM cancelling finished." << endl; +} + +// The following declarations allow us to put functions in the .cpp file +// instead of the header, since we know which instantiations are needed. + +template TNode StackingMap::find(TNode n) const; +template void StackingMap::set(TNode n, TNode newValue); +template void StackingMap::notify(); + +template TNode StackingMap::find(TNode n) const; +template void StackingMap::set(TNode n, TNode newValue); +template void StackingMap::notify(); + +}/* CVC4::theory::uf::morgan namespace */ +}/* CVC4::theory::uf namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/uf/morgan/stacking_map.h b/src/theory/uf/morgan/stacking_map.h new file mode 100644 index 000000000..c54acc363 --- /dev/null +++ b/src/theory/uf/morgan/stacking_map.h @@ -0,0 +1,91 @@ +/********************* */ +/*! \file stacking_map.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 Backtrackable map using an undo stack + ** + ** Backtrackable map using an undo stack rather than storing items in + ** a CDMap<>. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__UF__MORGAN__STACKING_MAP_H +#define __CVC4__THEORY__UF__MORGAN__STACKING_MAP_H + +#include +#include +#include + +#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 StackingMap : context::ContextNotifyObj { + /** Our underlying map type. */ + typedef __gnu_cxx::hash_map MapType; + + /** + * Our map of Nodes to their values. + */ + MapType d_map; + + /** Our undo stack for changes made to d_map. */ + std::vector > d_trace; + + /** Our current offset in the d_trace stack (context-dependent). */ + context::CDO d_offset; + +public: + StackingMap(context::Context* ctxt) : + context::ContextNotifyObj(ctxt), + d_offset(ctxt, 0) { + } + + ~StackingMap() throw() { } + + /** + * Return a Node's value in the key-value map. If n is not a key in + * the map, this function returns TNode::null(). + */ + TNode find(TNode n) const; + + /** + * Set the value in the key-value map for Node n to newValue. + */ + void set(TNode n, TNode newValue); + + /** + * Called by the Context when a pop occurs. Cancels everything to the + * current context level. Overrides ContextNotifyObj::notify(). + */ + void notify(); + +};/* class StackingMap<> */ + +}/* CVC4::theory::uf::morgan namespace */ +}/* CVC4::theory::uf namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /*__CVC4__THEORY__UF__MORGAN__STACKING_MAP_H */ diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp index 4ee698721..cc0296d0a 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.cpp +++ b/src/theory/uf/morgan/theory_uf_morgan.cpp @@ -131,25 +131,6 @@ Node TheoryUFMorgan::constructConflict(TNode diseq) { return conflict; } -TNode TheoryUFMorgan::find(TNode a) { - UnionFind::iterator i = d_unionFind.find(a); - if(i == d_unionFind.end()) { - return a; - } else { - return d_unionFind[a] = find((*i).second); - } -} - -// no path compression -TNode TheoryUFMorgan::debugFind(TNode a) const { - UnionFind::iterator i = d_unionFind.find(a); - if(i == d_unionFind.end()) { - return a; - } else { - return debugFind((*i).second); - } -} - void TheoryUFMorgan::notifyCongruent(TNode a, TNode b) { Debug("uf") << "uf: notified of merge " << a << std::endl << " and " << b << std::endl; @@ -188,7 +169,7 @@ void TheoryUFMorgan::merge(TNode a, TNode b) { // should have already found such a conflict Assert(find(d_trueNode) != find(d_falseNode)); - d_unionFind[a] = b; + d_unionFind.setCanon(a, b); DiseqLists::iterator deq_i = d_disequalities.find(a); if(deq_i != d_disequalities.end()) { diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h index 569f9bb49..d26e6ff8f 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.h +++ b/src/theory/uf/morgan/theory_uf_morgan.h @@ -30,6 +30,7 @@ #include "theory/theory.h" #include "theory/uf/theory_uf.h" +#include "theory/uf/morgan/union_find.h" #include "context/context.h" #include "context/context_mm.h" @@ -75,8 +76,10 @@ private: */ CongruenceClosure d_cc; - typedef context::CDMap UnionFind; - UnionFind d_unionFind; + /** + * Our union find for equalities. + */ + UnionFind d_unionFind; typedef context::CDList > DiseqList; typedef context::CDMap DiseqLists; @@ -130,8 +133,8 @@ public: */ void check(Effort level); - void presolve(){ - Unimplemented(); + void presolve() { + // do nothing for now } /** @@ -172,8 +175,8 @@ private: /** Constructs a conflict from an inconsistent disequality. */ Node constructConflict(TNode diseq); - TNode find(TNode a); - TNode debugFind(TNode a) const; + inline TNode find(TNode a); + inline TNode debugFind(TNode a) const; void appendToDiseqList(TNode of, TNode eq); void addDisequality(TNode eq); @@ -195,6 +198,14 @@ private: };/* class TheoryUFMorgan */ +inline TNode TheoryUFMorgan::find(TNode a) { + return d_unionFind.find(a); +} + +inline TNode TheoryUFMorgan::debugFind(TNode a) const { + return d_unionFind.debugFind(a); +} + }/* CVC4::theory::uf::morgan namespace */ }/* CVC4::theory::uf namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/uf/morgan/union_find.cpp b/src/theory/uf/morgan/union_find.cpp new file mode 100644 index 000000000..135320707 --- /dev/null +++ b/src/theory/uf/morgan/union_find.cpp @@ -0,0 +1,61 @@ +/********************* */ +/*! \file union_find.cpp + ** \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 + +#include "theory/uf/morgan/union_find.h" +#include "util/Assert.h" +#include "expr/node.h" + +using namespace std; + +namespace CVC4 { +namespace theory { +namespace uf { +namespace morgan { + +template +void UnionFind::notify() { + Trace("ufuf") << "UFUF cancelling : " << d_offset << " < " << d_trace.size() << " ?" << endl; + while(d_offset < d_trace.size()) { + pair p = d_trace.back(); + if(p.second.isNull()) { + d_map.erase(p.first); + Trace("ufuf") << "UFUF " << d_trace.size() << " erasing " << p.first << endl; + } else { + d_map[p.first] = p.second; + Trace("ufuf") << "UFUF " << d_trace.size() << " replacing " << p << endl; + } + d_trace.pop_back(); + } + Trace("ufuf") << "UFUF cancelling finished." << endl; +} + +// The following declarations allow us to put functions in the .cpp file +// instead of the header, since we know which instantiations are needed. + +template void UnionFind::notify(); + +template void UnionFind::notify(); + +}/* CVC4::theory::uf::morgan namespace */ +}/* CVC4::theory::uf namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/uf/morgan/union_find.h b/src/theory/uf/morgan/union_find.h new file mode 100644 index 000000000..b848be526 --- /dev/null +++ b/src/theory/uf/morgan/union_find.h @@ -0,0 +1,146 @@ +/********************* */ +/*! \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 +#include +#include + +#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 UnionFind : context::ContextNotifyObj { + /** Our underlying map type. */ + typedef __gnu_cxx::hash_map 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 > d_trace; + + /** Our current offset in the d_trace stack (context-dependent). */ + context::CDO 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 +inline TNode UnionFind::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 +inline TNode UnionFind::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 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 +inline void UnionFind::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 */ diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h index 44f061c12..73033f387 100644 --- a/src/theory/uf/tim/theory_uf_tim.h +++ b/src/theory/uf/tim/theory_uf_tim.h @@ -125,9 +125,8 @@ public: */ void check(Effort level); - void presolve() { - Unimplemented(); + // do nothing } /** diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h index db9d5bc65..90ab11f9f 100644 --- a/src/util/congruence_closure.h +++ b/src/util/congruence_closure.h @@ -34,6 +34,7 @@ #include "context/cdset.h" #include "context/cdlist_context_memory.h" #include "util/exception.h" +#include "theory/uf/morgan/stacking_map.h" namespace CVC4 { @@ -103,7 +104,7 @@ class CongruenceClosure { OutputChannel* d_out; // typedef all of these so that iterators are easy to define - typedef context::CDMap RepresentativeMap; + typedef theory::uf::morgan::StackingMap RepresentativeMap; typedef context::CDList > ClassList; typedef context::CDMap ClassLists; typedef context::CDList > UseList; @@ -115,6 +116,13 @@ class CongruenceClosure { typedef context::CDMap ProofMap; typedef context::CDMap ProofLabel; + // Simple, NON-context-dependent pending list, union find and "seen + // set" types for constructing explanations and + // nearestCommonAncestor(); see explain(). + typedef std::list > PendingProofList_t; + typedef __gnu_cxx::hash_map UnionFind_t; + typedef __gnu_cxx::hash_set SeenSet_t; + RepresentativeMap d_representative; ClassLists d_classList; UseLists d_useList; @@ -210,7 +218,7 @@ public: } } - TNode proofRewrite(TNode pfStep) { + TNode proofRewrite(TNode pfStep) const { ProofMap::const_iterator i = d_proofRewrite.find(pfStep); if(i == d_proofRewrite.end()) { return pfStep; @@ -254,18 +262,17 @@ public: * Find the EC representative for a term t in the current context. */ inline TNode find(TNode t) const throw(AssertionException) { - context::CDMap::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 >& pending, __gnu_cxx::hash_map& unionFind, std::list& pf) + void explainAlongPath(TNode a, TNode c, PendingProofList_t& pending, UnionFind_t& unionFind, std::list& pf) throw(AssertionException); - Node highestNode(TNode a, __gnu_cxx::hash_map& 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); /** @@ -311,7 +318,7 @@ private: * Internal lookup mapping from tuples to equalities. */ inline TNode lookup(TNode a) const { - context::CDMap::iterator i = d_lookup.find(a); + LookupMap::iterator i = d_lookup.find(a); if(i == d_lookup.end()) { return TNode::null(); } else { @@ -343,7 +350,7 @@ private: * 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)); @@ -406,14 +413,14 @@ template void CongruenceClosure::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; } @@ -421,10 +428,10 @@ void CongruenceClosure::addEq(TNode eq, TNode inputEq) { 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 @@ -433,26 +440,24 @@ void CongruenceClosure::addEq(TNode eq, TNode inputEq) { // 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() */ @@ -462,6 +467,7 @@ Node CongruenceClosure::buildRepresentativesOfApply(TNode apply, 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); @@ -472,18 +478,18 @@ Node CongruenceClosure::buildRepresentativesOfApply(TNode apply, template void CongruenceClosure::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 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; @@ -494,11 +500,11 @@ void CongruenceClosure::propagate(TNode seed) { 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); @@ -515,11 +521,11 @@ void CongruenceClosure::propagate(TNode seed) { 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 @@ -532,7 +538,7 @@ void CongruenceClosure::propagate(TNode seed) { 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| @@ -540,9 +546,9 @@ void CongruenceClosure::propagate(TNode seed) { 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; } @@ -555,17 +561,17 @@ void CongruenceClosure::propagate(TNode seed) { cl_bp = new(d_context->getCMM()) ClassList(true, d_context, false, context::ContextMemoryAllocator(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); @@ -581,15 +587,15 @@ void CongruenceClosure::propagate(TNode seed) { 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 @@ -606,7 +612,7 @@ void CongruenceClosure::propagate(TNode seed) { 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 @@ -623,21 +629,21 @@ void CongruenceClosure::propagate(TNode seed) { // 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') @@ -648,9 +654,9 @@ void CongruenceClosure::propagate(TNode seed) { } } }/* 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")) { @@ -679,8 +685,8 @@ void CongruenceClosure::merge(TNode ec1, TNode ec2) { } */ - 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); @@ -691,7 +697,7 @@ void CongruenceClosure::merge(TNode ec1, TNode ec2) { //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); @@ -702,18 +708,18 @@ void CongruenceClosure::merge(TNode ec1, TNode ec2) { template void CongruenceClosure::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()) { @@ -728,7 +734,7 @@ void CongruenceClosure::mergeProof(TNode a, TNode b, TNode e) { 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; } @@ -742,10 +748,10 @@ void CongruenceClosure::mergeProof(TNode a, TNode b, TNode e) { template Node CongruenceClosure::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); @@ -761,7 +767,7 @@ Node CongruenceClosure::normalize(TNode t) const } 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()) { @@ -783,10 +789,13 @@ Node CongruenceClosure::normalize(TNode t) const }/* 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 -Node CongruenceClosure::highestNode(TNode a, __gnu_cxx::hash_map& unionFind) +Node CongruenceClosure::highestNode(TNode a, UnionFind_t& unionFind) const throw(AssertionException) { - __gnu_cxx::hash_map::iterator i = unionFind.find(a); + UnionFind_t::iterator i = unionFind.find(a); if(i == unionFind.end()) { return a; } else { @@ -796,7 +805,7 @@ Node CongruenceClosure::highestNode(TNode a, __gnu_cxx::hash_map< template -void CongruenceClosure::explainAlongPath(TNode a, TNode c, std::list >& pending, __gnu_cxx::hash_map& unionFind, std::list& pf) +void CongruenceClosure::explainAlongPath(TNode a, TNode c, PendingProofList_t& pending, UnionFind_t& unionFind, std::list& pf) throw(AssertionException) { a = highestNode(a, unionFind); @@ -829,10 +838,27 @@ void CongruenceClosure::explainAlongPath(TNode a, TNode c, std::l template -Node CongruenceClosure::nearestCommonAncestor(TNode a, TNode b) +Node CongruenceClosure::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() */ @@ -854,13 +880,13 @@ Node CongruenceClosure::explain(Node a, Node b) b = replace(flatten(b)); } - std::list > pending; - __gnu_cxx::hash_map unionFind; + PendingProofList_t pending; + UnionFind_t unionFind; std::list 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 eq = pending.front(); @@ -869,29 +895,29 @@ Node CongruenceClosure::explain(Node a, Node b) 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); @@ -908,10 +934,10 @@ std::ostream& operator<<(std::ostream& out, const CongruenceClosure& cc) { out << "==============================================" << std::endl; - out << "Representatives:" << std::endl; + /*out << "Representatives:" << std::endl; for(typename CongruenceClosure::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::ClassLists::const_iterator i = cc.d_classList.begin(); i != cc.d_classList.end(); ++i) {