src/theory/uf/morgan/union_find.h

   1 /*********************                                                        */
   2 /*! \file union_find.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Path-compressing, backtrackable union-find using an undo
  15  ** stack
  16  **
  17  ** Path-compressing, backtrackable union-find using an undo stack
  18  ** rather than storing items in a CDMap<>.
  19  **/
  20
  21 #include "cvc4_private.h"
  22
  23 #ifndef __CVC4__THEORY__UF__MORGAN__UNION_FIND_H
  24 #define __CVC4__THEORY__UF__MORGAN__UNION_FIND_H
  25
  26 #include <utility>
  27 #include <vector>
  28 #include <ext/hash_map>
  29
  30 #include "expr/node.h"
  31 #include "context/cdo.h"
  32
  33 namespace CVC4 {
  34
  35 namespace context {
  36   class Context;
  37 }/* CVC4::context namespace */
  38
  39 namespace theory {
  40 namespace uf {
  41 namespace morgan {
  42
  43 // NodeType \in { Node, TNode }
  44 template <class NodeType, class NodeHash>
  45 class UnionFind : context::ContextNotifyObj {
  46   /** Our underlying map type. */
  47   typedef __gnu_cxx::hash_map<NodeType, NodeType, NodeHash> MapType;
  48
  49   /**
  50    * Our map of Nodes to their canonical representatives.
  51    * If a Node is not present in the map, it is its own
  52    * representative.
  53    */
  54   MapType d_map;
  55
  56   /** Our undo stack for changes made to d_map. */
  57   std::vector<std::pair<TNode, TNode> > d_trace;
  58
  59   /** Our current offset in the d_trace stack (context-dependent). */
  60   context::CDO<size_t> d_offset;
  61
  62 public:
  63   UnionFind(context::Context* ctxt) :
  64     context::ContextNotifyObj(ctxt),
  65     d_offset(ctxt, 0) {
  66   }
  67
  68   ~UnionFind() throw() { }
  69
  70   /**
  71    * Return a Node's union-find representative, doing path compression.
  72    */
  73   inline TNode find(TNode n);
  74
  75   /**
  76    * Return a Node's union-find representative, NOT doing path compression.
  77    * This is useful for Assert() statements, debug checking, and similar
  78    * things that you do NOT want to mutate the structure.
  79    */
  80   inline TNode debugFind(TNode n) const;
  81
  82   /**
  83    * Set the canonical representative of n to newParent.  They should BOTH
  84    * be their own canonical representatives on entry to this funciton.
  85    */
  86   inline void setCanon(TNode n, TNode newParent);
  87
  88   /**
  89    * Called by the Context when a pop occurs.  Cancels everything to the
  90    * current context level.  Overrides ContextNotifyObj::notify().
  91    */
  92   void notify();
  93
  94 };/* class UnionFind<> */
  95
  96 template <class NodeType, class NodeHash>
  97 inline TNode UnionFind<NodeType, NodeHash>::debugFind(TNode n) const {
  98   typename MapType::const_iterator i = d_map.find(n);
  99   if(i == d_map.end()) {
 100     return n;
 101   } else {
 102     return debugFind((*i).second);
 103   }
 104 }
 105
 106 template <class NodeType, class NodeHash>
 107 inline TNode UnionFind<NodeType, NodeHash>::find(TNode n) {
 108   Trace("ufuf") << "UFUF find of " << n << std::endl;
 109   typename MapType::iterator i = d_map.find(n);
 110   if(i == d_map.end()) {
 111     Trace("ufuf") << "UFUF   it is rep" << std::endl;
 112     return n;
 113   } else {
 114     Trace("ufuf") << "UFUF   not rep: par is " << (*i).second << std::endl;
 115     std::pair<TNode, TNode> pr = *i;
 116     // our iterator is invalidated by the recursive call to find(),
 117     // since it mutates the map
 118     TNode p = find(pr.second);
 119     if(p == pr.second) {
 120       return p;
 121     }
 122     d_trace.push_back(std::make_pair(n, pr.second));
 123     d_offset = d_trace.size();
 124     Trace("ufuf") << "UFUF   setting canon of " << n << " : " << p << " @ " << d_trace.size() << std::endl;
 125     pr.second = p;
 126     d_map.insert(pr);
 127     return p;
 128   }
 129 }
 130
 131 template <class NodeType, class NodeHash>
 132 inline void UnionFind<NodeType, NodeHash>::setCanon(TNode n, TNode newParent) {
 133   Assert(d_map.find(n) == d_map.end());
 134   Assert(d_map.find(newParent) == d_map.end());
 135   if(n != newParent) {
 136     Trace("ufuf") << "UFUF setting canon of " << n << " : " << newParent << " @ " << d_trace.size() << std::endl;
 137     d_map[n] = newParent;
 138     d_trace.push_back(std::make_pair(n, TNode::null()));
 139     d_offset = d_trace.size();
 140   }
 141 }
 142
 143 }/* CVC4::theory::uf::morgan namespace */
 144 }/* CVC4::theory::uf namespace */
 145 }/* CVC4::theory namespace */
 146 }/* CVC4 namespace */
 147
 148 #endif /*__CVC4__THEORY__UF__MORGAN__UNION_FIND_H */