1 files changed, 261 insertions, 0 deletions
diff --git a/src/theory/example/ecdata.h b/src/theory/example/ecdata.h
new file mode 100644
index 000000000..5e72f0042
--- /dev/null
+++ b/src/theory/example/ecdata.h
@@ -0,0 +1,261 @@
+/*********************                                                        */
+/*! \file ecdata.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** 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 Context dependent equivalence class datastructure for nodes.
+ **
+ ** Context dependent equivalence class datastructure for nodes.
+ ** Currently keeps a context dependent watch list.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__UF__TIM__ECDATA_H
+#define __CVC4__THEORY__UF__TIM__ECDATA_H
+
+#include "expr/node.h"
+#include "context/context.h"
+#include "context/cdo.h"
+#include "context/context_mm.h"
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+namespace tim {
+
+/**
+ * Link is a context dependent linked list of nodes.
+ * Link is intended to be allocated in a Context's memory manager.
+ * The next pointer of the list is context dependent, but the node being
+ * pointed to is fixed for the life of the Link.
+ *
+ * Clients of Link are intended not to modify the node that is being pointed
+ * to in good faith.  This may change in the future.
+ */
+struct Link {
+  /**
+   * Pointer to the next element in linked list.
+   * This is context dependent. 
+   */
+  context::CDO<Link*> d_next;
+
+  /**
+   * Link is supposed to be allocated in a region of a
+   * ContextMemoryManager.  In order to avoid having to decrement the
+   * ref count at deletion time, it is preferrable for the user of
+   * Link to maintain the invariant that data will survival for the
+   * entire scope of the TNode.
+   */
+  TNode d_data;
+
+  /**
+   * Creates a new Link w.r.t. a context for the node n.
+   * An optional parameter is to specify the next element in the link.
+   */
+  Link(context::Context* context, TNode n, Link* l = NULL) :
+    d_next(true, context, l),
+    d_data(n) {
+    Debug("context") << "Link: " << this
+                     << " so cdo is " << &d_next << std::endl;
+  }
+
+  /**
+   * Allocates a new Link in the region for the provided ContextMemoryManager.
+   * This allows for cheap cleanup on pop.
+   */
+  static void* operator new(size_t size, context::ContextMemoryManager* pCMM) {
+    return pCMM->newData(size);
+  }
+
+private:
+
+  /**
+   * The destructor isn't actually defined.  This declaration keeps
+   * the compiler from creating (wastefully) a default definition, and
+   * ensures that we get a link error if someone uses Link in a way
+   * that requires destruction.  Objects of class Link should always
+   * be allocated in a ContextMemoryManager, which doesn't call
+   * destructors.
+   */
+  ~Link() throw();
+
+  /**
+   * Just like the destructor, this is not defined.  This ensures no
+   * one tries to create a Link on the heap.
+   */
+  static void* operator new(size_t size);
+
+};/* struct Link */
+
+
+/**
+ * ECData is a equivalence class object that is context dependent.
+ * It is developed in order to support the congruence closure algorithm
+ * in TheoryUF, and is not intended to be used outside of that package.
+ *
+ * ECData maintains:
+ * - find pointer for the equivalence class (disjoint set forest)
+ * - the node that represents the equivalence class.
+ * - maintains a predecessorlist/watchlist
+ *
+ * ECData does not have support for the canonical find and union operators
+ * for disjoint set forests.  Instead it only provides access to the find
+ * pointer. The implementation of find is ccFind in TheoryUF.
+ * union is broken into 2 phases:
+ *  1) setting the find point with setFind
+ *  2) taking over the watch list of the other node.
+ * This is a technical requirement for the implementation of TheoryUF.
+ * (See ccUnion in TheoryUF for more information.)
+ *
+ * The intended paradigm for iterating over the watch list of ec is:
+ *      for(Link* i = ec->getFirst(); i != NULL; i = i->next );
+ *
+ * See also ECAttr() in theory_uf.h, and theory_uf.cpp where the codde that uses
+ * ECData lives.
+ */
+class ECData : public context::ContextObj {
+private:
+  /**
+   * This is the standard disjoint set forest find pointer.
+   *
+   * Why an ECData pointer instead of a node?
+   * This was chosen to be a ECData pointer in order to shortcut at least one
+   * table every time the find pointer is examined.
+   */
+  ECData* d_find;
+
+  /**
+   * This is pointer back to the node that represents this equivalence class.
+   *
+   * The following invariant should be maintained:
+   *  (n.getAttribute(ECAttr()))->rep == n
+   * i.e. rep is equal to the node that maps to the ECData using ECAttr.
+   *
+   * Tricky part: This needs to be a TNode, not a Node.
+   * Suppose that rep were a hard link.
+   * When a node n maps to an ECData via the ECAttr() there will be a hard
+   * link back to n in the ECData. The attribute does not do garbage collection
+   * until the node gets garbage collected, which does not happen until its
+   * ref count drops to 0. So because of this cycle neither the node and
+   * the ECData will never get garbage collected.
+   * So this needs to be a soft link.
+   */
+  TNode d_rep;
+
+  // Watch list data structures follow
+
+  /**
+   * Maintains watch list size for more efficient merging.
+   */
+  unsigned d_watchListSize;
+
+  /**
+   * Pointer to the beginning of the watchlist.
+   * This value is NULL iff the watch list is empty.
+   */
+  Link* d_first;
+
+  /**
+   * Pointer to the end of the watch-list.
+   * This is maintained in order to constant time list merging.
+   * (This does not give any asymptotic improve as this is currently always
+   * preceeded by an O(|watchlist|) operation.)
+   * This value is NULL iff the watch list is empty.
+   */
+  Link* d_last;
+
+  /** Context-dependent operation: save this ECData */
+  context::ContextObj* save(context::ContextMemoryManager* pCMM);
+
+  /** Context-dependent operation: restore this ECData */
+  void restore(context::ContextObj* pContextObj);
+
+public:
+  /**
+   * Returns true if this ECData object is the current representative of
+   * the equivalence class.
+   */
+  bool isClassRep();
+
+  /**
+   * Adds a node to the watch list of the equivalence class.  Does
+   * context-dependent memory allocation in the Context with which
+   * this ECData was created.
+   *
+   * @param n the node to be added.
+   * @pre isClassRep() == true
+   */
+  void addPredecessor(TNode n);
+
+  /**
+   * Creates a EQ with the representative n
+   * @param context the context to associate with this ecdata.
+   *   This is required as ECData is context dependent
+   * @param n the node that corresponds to this ECData
+   */
+  ECData(context::Context* context, TNode n);
+
+  /** Destructor for ECDatas */
+  ~ECData() {
+    Debug("ufgc") << "Calling ECData destructor" << std::endl;
+    destroy();
+  }
+
+  /**
+   * An ECData takes over the watch list of another ECData.
+   * This is the second step in the union operator for ECData.
+   * This should be called after nslave->setFind(nmaster);
+   * After this is done nslave's watch list should never be accessed by
+   * getLast() or getFirst()
+   */
+  static void takeOverDescendantWatchList(ECData * nslave, ECData * nmaster);
+
+  /**
+   * Returns the representative of this ECData.
+   */
+  Node getRep();
+
+  /**
+   * Returns the size of the equivalence class.
+   */
+  unsigned getWatchListSize();
+
+  /**
+   * Returns a pointer the first member of the watch list.
+   */
+  Link* getFirst();
+
+
+  /**
+   * Returns the find pointer of the ECData.
+   * If isClassRep(), then getFind() == this
+   */
+  ECData* getFind();
+
+  /**
+   * Sets the find pointer of the equivalence class to be another ECData object.
+   *
+   * @pre isClassRep() == true
+   * @pre ec->isClassRep() == true
+   * @post isClassRep() == false
+   * @post ec->isClassRep() == true
+   */
+  void setFind(ECData * ec);
+
+};/* class ECData */
+
+}/* CVC4::theory::uf::tim namespace */
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__UF__TIM__ECDATA_H */