diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-11-17 01:39:37 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-11-17 01:39:37 +0000 |
commit | c7a70635797fe4205b27d29546dd4fe763220794 (patch) | |
tree | 715eb2c43beebaaa725a3064597761f60975fea6 /src/theory/uf | |
parent | bb2a0e0e12f39a1b4dea8fb0c990decba4708a1c (diff) |
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.
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/morgan/Makefile.am | 6 | ||||
-rw-r--r-- | src/theory/uf/morgan/stacking_map.cpp | 83 | ||||
-rw-r--r-- | src/theory/uf/morgan/stacking_map.h | 91 | ||||
-rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.cpp | 21 | ||||
-rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.h | 23 | ||||
-rw-r--r-- | src/theory/uf/morgan/union_find.cpp | 61 | ||||
-rw-r--r-- | src/theory/uf/morgan/union_find.h | 146 | ||||
-rw-r--r-- | src/theory/uf/tim/theory_uf_tim.h | 3 |
8 files changed, 405 insertions, 29 deletions
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 <iostream> + +#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 <class NodeType, class NodeHash> +TNode StackingMap<NodeType, NodeHash>::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 <class NodeType, class NodeHash> +void StackingMap<NodeType, NodeHash>::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 <class NodeType, class NodeHash> +void StackingMap<NodeType, NodeHash>::notify() { + Trace("ufsm") << "UFSM cancelling : " << d_offset << " < " << d_trace.size() << " ?" << endl; + while(d_offset < d_trace.size()) { + pair<TNode, TNode> 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<Node, NodeHashFunction>::find(TNode n) const; +template void StackingMap<Node, NodeHashFunction>::set(TNode n, TNode newValue); +template void StackingMap<Node, NodeHashFunction>::notify(); + +template TNode StackingMap<TNode, TNodeHashFunction>::find(TNode n) const; +template void StackingMap<TNode, TNodeHashFunction>::set(TNode n, TNode newValue); +template void StackingMap<TNode, TNodeHashFunction>::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 <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 StackingMap : context::ContextNotifyObj { + /** Our underlying map type. */ + typedef __gnu_cxx::hash_map<NodeType, NodeType, NodeHash> MapType; + + /** + * Our map of Nodes to their values. + */ + 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: + 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<CongruenceChannel> d_cc; - typedef context::CDMap<TNode, TNode, TNodeHashFunction> UnionFind; - UnionFind d_unionFind; + /** + * Our union find for equalities. + */ + UnionFind<TNode, TNodeHashFunction> d_unionFind; typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > DiseqList; typedef context::CDMap<Node, DiseqList*, NodeHashFunction> 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 <iostream> + +#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 <class NodeType, class NodeHash> +void UnionFind<NodeType, NodeHash>::notify() { + Trace("ufuf") << "UFUF cancelling : " << d_offset << " < " << d_trace.size() << " ?" << endl; + while(d_offset < d_trace.size()) { + pair<TNode, TNode> 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<Node, NodeHashFunction>::notify(); + +template void UnionFind<TNode, TNodeHashFunction>::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 <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 */ 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 } /** |