diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-05-23 21:58:12 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-05-23 21:58:12 +0000 |
commit | 3f7f9df5f0c419b7f7dd39e32852161f406a441f (patch) | |
tree | 67ae6454e4496f6370cf8236500946e2c7e926b0 /src/theory/arrays/union_find.cpp | |
parent | 91656937b2188f05cdd9b42955c04e6157349285 (diff) |
Merge from arrays2 branch.
Diffstat (limited to 'src/theory/arrays/union_find.cpp')
-rw-r--r-- | src/theory/arrays/union_find.cpp | 59 |
1 files changed, 59 insertions, 0 deletions
diff --git a/src/theory/arrays/union_find.cpp b/src/theory/arrays/union_find.cpp new file mode 100644 index 000000000..b0f06b78e --- /dev/null +++ b/src/theory/arrays/union_find.cpp @@ -0,0 +1,59 @@ +/********************* */ +/*! \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. Refactored from the UF union-find. + ** + ** Path-compressing, backtrackable union-find using an undo stack + ** rather than storing items in a CDMap<>. + **/ + +#include <iostream> + +#include "theory/arrays/union_find.h" +#include "util/Assert.h" +#include "expr/node.h" + +using namespace std; + +namespace CVC4 { +namespace theory { +namespace arrays { + +template <class NodeType, class NodeHash> +void UnionFind<NodeType, NodeHash>::notify() { + Trace("arraysuf") << "arraysUF 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("arraysuf") << "arraysUF " << d_trace.size() << " erasing " << p.first << endl; + } else { + d_map[p.first] = p.second; + Trace("arraysuf") << "arraysUF " << d_trace.size() << " replacing " << p << endl; + } + d_trace.pop_back(); + } + Trace("arraysuf") << "arraysUF 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::arrays namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ |