Minor cleanup, remove unused files.

8 files changed, 15 insertions, 566 deletions

diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 55db44c29..a4cd0d124 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -16,10 +16,6 @@ operator CONSTRUCTOR_TYPE 1: "constructor"
 cardinality CONSTRUCTOR_TYPE \
     "::CVC4::theory::datatypes::ConstructorProperties::computeCardinality(%TYPE%)" \
     "theory/datatypes/theory_datatypes_type_rules.h"
-well-founded CONSTRUCTOR_TYPE \
-    "::CVC4::theory::datatypes::ConstructorProperties::isWellFounded(%TYPE%)" \
-    "::CVC4::theory::datatypes::ConstructorProperties::mkGroundTerm(%TYPE%)" \
-    "theory/datatypes/theory_datatypes_type_rules.h"
 
 # selector type has domain type and a range type
 operator SELECTOR_TYPE 2 "selector"
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index b97645ecb..15d1c6c9e 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -264,49 +264,6 @@ struct ConstructorProperties {
     }
     return c;
   }
-
-  inline static bool isWellFounded(TypeNode type) {
-    // Constructors aren't exactly functions, they're like
-    // parameterized ground terms.  So the wellfoundedness is more
-    // like that of a tuple than that of a function.
-    AssertArgument(type.isConstructor(), type);
-    for(unsigned i = 0, i_end = type.getNumChildren(); i < i_end - 1; ++i) {
-      if(!type[i].isWellFounded()) {
-        return false;
-      }
-    }
-    return true;
-  }
-
-  inline static Node mkGroundTerm(TypeNode type) {
-    AssertArgument(type.isConstructor(), type);
-
-    // is this already in the cache ?
-    Node groundTerm = type.getAttribute(GroundTermAttr());
-    if(!groundTerm.isNull()) {
-      return groundTerm;
-    }
-
-    // This is a bit tricky; Constructors have a unique index within
-    // their datatype, but Constructor *types* do not; multiple
-    // Constructors within the same Datatype could share the same
-    // type.  So we scan through the datatype to find one that
-    // matches.
-    //const Datatype& dt = type[type.getNumChildren() - 1].getConst<Datatype>();
-    const Datatype& dt = DatatypeType(type[type.getNumChildren() - 1].toType()).getDatatype();
-    for(Datatype::const_iterator i = dt.begin(),
-          i_end = dt.end();
-        i != i_end;
-        ++i) {
-      if(TypeNode::fromType((*i).getConstructor().getType()) == type) {
-        groundTerm = Node::fromExpr((*i).mkGroundTerm( type.toType() ));
-        type.setAttribute(GroundTermAttr(), groundTerm);
-        return groundTerm;
-      }
-    }
-
-    InternalError("couldn't find a matching constructor?!");
-  }
 };/* struct ConstructorProperties */
 
 struct TupleTypeRule {
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index df787d049..59591dc3b 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -60,7 +60,6 @@ libutil_la_SOURCES = \
 	channel.h \
 	language.cpp \
 	ntuple.h \
-	recursion_breaker.h \
 	subrange_bound.h \
 	dump.h \
 	dump.cpp \
@@ -70,8 +69,6 @@ libutil_la_SOURCES = \
 	cardinality.cpp \
 	cache.h \
 	utility.h \
-	trans_closure.h \
-	trans_closure.cpp \
 	boolean_simplification.h \
 	boolean_simplification.cpp \
 	ite_removal.h \
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index cd27a897b..47bd7de66 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -25,7 +25,6 @@
 #include "expr/node_manager.h"
 #include "expr/node.h"
 #include "expr/attribute.h"
-#include "util/recursion_breaker.h"
 #include "util/matcher.h"
 #include "util/cvc4_assert.h"
 
@@ -38,20 +37,14 @@ namespace expr {
     struct DatatypeIndexTag {};
     struct DatatypeConsIndexTag {};
     struct DatatypeFiniteTag {};
-    struct DatatypeWellFoundedTag {};
     struct DatatypeFiniteComputedTag {};
-    struct DatatypeWellFoundedComputedTag {};
-    struct DatatypeGroundTermTag {};
   }/* CVC4::expr::attr namespace */
 }/* CVC4::expr namespace */
 
 typedef expr::Attribute<expr::attr::DatatypeIndexTag, uint64_t> DatatypeIndexAttr;
 typedef expr::Attribute<expr::attr::DatatypeConsIndexTag, uint64_t> DatatypeConsIndexAttr;
 typedef expr::Attribute<expr::attr::DatatypeFiniteTag, bool> DatatypeFiniteAttr;
-typedef expr::Attribute<expr::attr::DatatypeWellFoundedTag, bool> DatatypeWellFoundedAttr;
 typedef expr::Attribute<expr::attr::DatatypeFiniteComputedTag, bool> DatatypeFiniteComputedAttr;
-typedef expr::Attribute<expr::attr::DatatypeWellFoundedComputedTag, bool> DatatypeWellFoundedComputedAttr;
-typedef expr::Attribute<expr::attr::DatatypeGroundTermTag, Node> DatatypeGroundTermAttr;
 
 const Datatype& Datatype::datatypeOf(Expr item) {
   ExprManagerScope ems(item);
@@ -312,30 +305,30 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
   CheckArgument(isResolved(), this, "this datatype is not yet resolved");
   ExprManagerScope ems(d_self);
 
-  TypeNode self = TypeNode::fromType(d_self);
 
   // is this already in the cache ?
-  Expr groundTerm = self.getAttribute(DatatypeGroundTermAttr()).toExpr();
-  if(!groundTerm.isNull()) {
-    Debug("datatypes") << "\nin cache: " << d_self << " => " << groundTerm << std::endl;
+  std::map< Type, Expr >::iterator it = d_ground_term.find( t );
+  if( it != d_ground_term.end() ){
+    Debug("datatypes") << "\nin cache: " << d_self << " => " << it->second << std::endl;
+    return it->second;
   } else {
     std::vector< Type > processing;
-    groundTerm = computeGroundTerm( t, processing );
-    if(!groundTerm.isNull() && !isParametric() ) {
+    Expr groundTerm = computeGroundTerm( t, processing );
+    if(!groundTerm.isNull() ) {
       // we found a ground-term-constructing constructor!
-      self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
       Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm << std::endl;
     }
-  }
-  if( groundTerm.isNull() ){
-    if( !d_isCo ){
-      // if we get all the way here, we aren't well-founded
-      CheckArgument(false, *this, "datatype is not well-founded, cannot construct a ground term!");
+    d_ground_term[t] = groundTerm;
+    if( groundTerm.isNull() ){
+      if( !d_isCo ){
+        // if we get all the way here, we aren't well-founded
+        CheckArgument(false, *this, "datatype is not well-founded, cannot construct a ground term!");
+      }else{
+        return groundTerm;
+      }
     }else{
       return groundTerm;
     }
-  }else{
-    return groundTerm;
   }
 }
 
@@ -753,69 +746,6 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) {
   return true;
 }
 
-bool DatatypeConstructor::isWellFounded() const throw(IllegalArgumentException) {
-  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-
-  // we're using some internals, so we have to set up this library context
-  ExprManagerScope ems(d_constructor);
-  std::vector< Type > processing;
-  return computeWellFounded( processing );
-}
-
-Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
-  CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-
-  // we're using some internals, so we have to set up this library context
-  ExprManagerScope ems(d_constructor);
-
-  TNode self = Node::fromExpr(d_constructor);
-
-  // is this already in the cache ?
-  Expr groundTerm = self.getAttribute(DatatypeGroundTermAttr()).toExpr();
-  if(!groundTerm.isNull()) {
-    return groundTerm;
-  }
-
-  RecursionBreaker<const DatatypeConstructor*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this);
-  if(breaker.isRecursion()) {
-    // Recursive path, we should skip and go to the next constructor;
-    // see lengthy comments in Datatype::mkGroundTerm().
-    return Expr();
-  }
-
-  std::vector<Expr> groundTerms;
-  groundTerms.push_back(getConstructor());
-
-  // for each selector, get a ground term
-  CheckArgument( t.isDatatype(), t );
-  std::vector< Type > instTypes;
-  std::vector< Type > paramTypes;
-  if( DatatypeType(t).isParametric() ){
-    paramTypes = DatatypeType(t).getDatatype().getParameters();
-    instTypes = DatatypeType(t).getParamTypes();
-  }
-  for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    Type selType = SelectorType((*i).getSelector().getType()).getRangeType();
-    if( DatatypeType(t).isParametric() ){
-      selType = selType.substitute( paramTypes, instTypes );
-    }
-    groundTerms.push_back(selType.mkGroundTerm());
-  }
-
-  groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
-  if( groundTerm.getType()!=t ){
-    Assert( Datatype::datatypeOf( d_constructor ).isParametric() );
-    //type is ambiguous, must apply type ascription
-    Debug("datatypes-gt") << "ambiguous type for " << groundTerm << ", ascribe to " << t << std::endl;
-    groundTerms[0] = getConstructor().getExprManager()->mkExpr(kind::APPLY_TYPE_ASCRIPTION,
-                       getConstructor().getExprManager()->mkConst(AscriptionType(getSpecializedConstructorType(t))),
-                       groundTerms[0]);
-    groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
-  }
-  self.setAttribute(DatatypeGroundTermAttr(), groundTerm);
-  return groundTerm;
-}
-
 Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException) {
 // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_constructor);
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 445048440..6e7e09fa0 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -320,20 +320,6 @@ public:
   bool isFinite() const throw(IllegalArgumentException);
 
   /**
-   * Return true iff this constructor is well-founded (there exist
-   * ground terms).  The constructor must be resolved or an
-   * exception is thrown.
-   */
-  bool isWellFounded() const throw(IllegalArgumentException);
-
-  /**
-   * Construct and return a ground term of this constructor.  The
-   * constructor must be both resolved and well-founded, or else an
-   * exception is thrown.
-   */
-  Expr mkGroundTerm( Type t ) const throw(IllegalArgumentException);
-
-  /**
    * Returns true iff this Datatype constructor has already been
    * resolved.
    */
@@ -483,7 +469,7 @@ private:
   // is this well-founded
   mutable int d_well_founded;
   // ground term for this datatype
-  mutable Expr d_ground_term;
+  mutable std::map< Type, Expr > d_ground_term;
 
   /**
    * Datatypes refer to themselves, recursively, and we have a
diff --git a/src/util/recursion_breaker.h b/src/util/recursion_breaker.h
deleted file mode 100644
index 3369c5c23..000000000
--- a/src/util/recursion_breaker.h
+++ /dev/null
@@ -1,135 +0,0 @@
-/*********************                                                        */
-/*! \file recursion_breaker.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief A utility class to help with detecting recursion in a
- ** computation
- **
- ** A utility class to help with detecting recursion in a computation.
- ** A breadcrumb trail is left, and a function can query the breaker
- ** to see if recursion has occurred.  For example:
- **
- ** @code
- **   int foo(int x) {
- **     RecursionBreaker<int> breaker("foo", x);
- **     if(breaker.isRecursion()) {
- **       ++d_count;
- **       return 0;
- **     }
- **     int xfactor = x * x;
- **     if(x > 0) {
- **       xfactor = -xfactor;
- **     }
- **     int y = foo(11 * x + xfactor);
- **     int z = y < 0 ? y : x * y;
- **     cout << "x == " << x << ", y == " << y << " ==> " << z << endl;
- **     return z;
- **   }
- ** @endcode
- **
- ** Recursion occurs after a while in this example, and the recursion
- ** is broken by the RecursionBreaker.
- **
- ** RecursionBreaker is really just a thread-local set of "what has
- ** been seen."  The above example is trivial, easily fixed by
- ** allocating such a set at the base of the recursion, and passing a
- ** reference to it to each invocation.  But other cases of
- ** nontrivial, mutual recursion exist that aren't so easily broken,
- ** and that's what the RecursionBreaker is for.  See
- ** Datatype::getCardinality(), for example.  A Datatype's cardinality
- ** depends on the cardinalities of the types it references---but
- ** these, in turn can reference the original datatype in a cyclic
- ** fashion.  Where that happens, we need to break the recursion.
- **
- ** Several RecursionBreakers can be used at once; each is identified
- ** by the string tag in its constructor.  If a single function is
- ** involved in the detection of recursion, a good choice is to use
- ** __FUNCTION__:
- **
- **   RecursionBreaker<Foo*>(__FUNCTION__, this) breaker;
- **
- ** Of course, if you're using GNU, you might prefer
- ** __PRETTY_FUNCTION__, since it's robust to overloading, namespaces,
- ** and containing classes.  But neither is a good choice if two
- ** functions need to access the same RecursionBreaker mechanism.
- **
- ** For non-primitive datatypes, it might be a good idea to use a
- ** pointer type to instantiate RecursionBreaker<>, for example with
- ** RecursionBreaker<Foo*>.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__RECURSION_BREAKER_H
-#define __CVC4__RECURSION_BREAKER_H
-
-#include <string>
-#include <map>
-#include <ext/hash_set>
-#include "util/hash.h"
-#include "util/tls.h"
-#include "util/cvc4_assert.h"
-
-namespace CVC4 {
-
-template <class T, class Hasher = std::hash<T> >
-class RecursionBreaker {
-  typedef std::hash_set<T, Hasher> Set;
-  typedef std::map<std::string, Set> Map;
-  static CVC4_THREADLOCAL(Map*) s_maps;
-
-  std::string d_tag;
-  const T d_item;
-  bool d_firstToTag;
-  bool d_recursion;
-
-public:
-  /** Mark that item has been seen for tag. */
-  RecursionBreaker(std::string tag, const T& item) :
-    d_tag(tag),
-    d_item(item) {
-    if(s_maps == NULL) {
-      s_maps = new Map();
-    }
-    d_firstToTag = s_maps->find(tag) == s_maps->end();
-    Set& set = (*s_maps)[tag];
-    d_recursion = (set.find(item) != set.end());
-    Assert(!d_recursion || !d_firstToTag);
-    if(!d_recursion) {
-      set.insert(item);
-    }
-  }
-
-  /** Clean up the seen trail. */
-  ~RecursionBreaker() {
-    Assert(s_maps->find(d_tag) != s_maps->end());
-    if(!d_recursion) {
-      (*s_maps)[d_tag].erase(d_item);
-    }
-    if(d_firstToTag) {
-      Assert((*s_maps)[d_tag].empty());
-      s_maps->erase(d_tag);
-      Assert(s_maps->find(d_tag) == s_maps->end());
-    }
-  }
-
-  /** Return true iff recursion has been detected. */
-  bool isRecursion() const throw() {
-    return d_recursion;
-  }
-
-};/* class RecursionBreaker<T> */
-
-template <class T, class Hasher>
-CVC4_THREADLOCAL(typename RecursionBreaker<T, Hasher>::Map*) RecursionBreaker<T, Hasher>::s_maps;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__RECURSION_BREAKER_H */
diff --git a/src/util/trans_closure.cpp b/src/util/trans_closure.cpp
deleted file mode 100644
index 02b51d751..000000000
--- a/src/util/trans_closure.cpp
+++ /dev/null
@@ -1,128 +0,0 @@
-/*********************                                                        */
-/*! \file trans_closure.cpp
- ** \verbatim
- ** Original author: Clark Barrett
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief The transitive closure module implementation
- **
- ** Implementation file for TransitiveClosure class.
- **/
-
-
-#include "util/trans_closure.h"
-#include "util/cvc4_assert.h"
-
-
-using namespace std;
-
-
-namespace CVC4 {
-
-
-TransitiveClosure::~TransitiveClosure() {
-  unsigned i;
-  for (i = 0; i < adjMatrix.size(); ++i) {
-    if (adjMatrix[i]) {
-      adjMatrix[i]->deleteSelf();
-    }
-  }
-}
-
-
-bool TransitiveClosure::addEdge(unsigned i, unsigned j)
-{
-  Debug("trans-closure") << "Add edge " << i << " -> " << j << std::endl;
-  // Check for loops
-  Assert(i != j, "Cannot add self-loop");
-  if (adjIndex.get() > j && adjMatrix[j] != NULL && adjMatrix[j]->read(i)) {
-    return true;
-  }
-
-  // Grow matrix if necessary
-  unsigned maxSize = ((i > j) ? i : j) + 1;
-  while (maxSize > adjIndex.get()) {
-    if( maxSize > adjMatrix.size() ){
-      adjMatrix.push_back(NULL);
-    }else if( adjMatrix[adjIndex.get()]!=NULL ){
-      adjMatrix[adjIndex.get()]->clear();
-    }
-    adjIndex.set( adjIndex.get() + 1 );
-  }
-
-  // Add edge from i to j and everything j can reach
-  if (adjMatrix[i] == NULL) {
-    adjMatrix[i] = new (true) CDBV(d_context);
-  }
-  adjMatrix[i]->write(j);
-  if (adjMatrix[j] != NULL) {
-    adjMatrix[i]->merge(adjMatrix[j]);
-  }
-
-  // Add edges from everything that can reach i to j and everything that j can reach
-  unsigned k;
-  for (k = 0; k < adjIndex.get(); ++k) {
-    if (adjMatrix[k] != NULL && adjMatrix[k]->read(i)) {
-      adjMatrix[k]->write(j);
-      if (adjMatrix[j] != NULL) {
-        adjMatrix[k]->merge(adjMatrix[j]);
-      }
-    }
-  }
-
-  return false;
-}
-
-bool TransitiveClosure::isConnected(unsigned i, unsigned j)
-{
-  if( i>=adjIndex.get() || j>adjIndex.get() ){//adjMatrix.size() ){
-    return false;
-  }else{
-    return adjMatrix[i] != NULL && adjMatrix[i]->read(j);
-  }
-}
-
-void TransitiveClosure::debugPrintMatrix()
-{
-  unsigned i,j;
-  for (i = 0; i < adjIndex.get(); ++i) {
-    for (j = 0; j < adjIndex.get(); ++j) {
-      if (adjMatrix[i] != NULL && adjMatrix[i]->read(j)) {
-        Debug("trans-closure") << "1 ";
-      }
-      else Debug("trans-closure") << "0 ";
-    }
-    Debug("trans-closure") << endl;
-  }
-}
-
-unsigned TransitiveClosureNode::getId( Node i ){
-  context::CDHashMap< Node, unsigned, NodeHashFunction >::iterator it = nodeMap.find( i );
-  if( it==nodeMap.end() ){
-    unsigned c = d_counter.get();
-    nodeMap[i] = c;
-    d_counter.set( c + 1 );
-    return c;
-  }
-  return (*it).second;
-}
-
-void TransitiveClosureNode::debugPrint(){
-  for( int i=0; i<(int)currEdges.size(); i++ ){
-    Debug("trans-closure") << "currEdges[ " << i << " ] = "
-                           << currEdges[i].first << " -> " << currEdges[i].second;
-    int id1 = getId( currEdges[i].first );
-    int id2 = getId( currEdges[i].second );
-    Debug("trans-closure") << " { " << id1 << " -> " << id2 << " } ";
-    Debug("trans-closure") << std::endl;
-  }
-  debugPrintMatrix();
-}
-
-
-}/* CVC4 namespace */
diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h
deleted file mode 100644
index 27f32377e..000000000
--- a/src/util/trans_closure.h
+++ /dev/null
@@ -1,154 +0,0 @@
-/*********************                                                        */
-/*! \file trans_closure.h
- ** \verbatim
- ** Original author: Clark Barrett
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief The transitive closure module
- **
- ** The transitive closure module.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__UTIL__TRANSITIVE_CLOSURE_H
-#define __CVC4__UTIL__TRANSITIVE_CLOSURE_H
-
-#include "context/context.h"
-#include "expr/node.h"
-#include <map>
-
-#include "context/cdlist.h"
-#include "context/cdhashmap.h"
-#include "context/cdo.h"
-
-namespace CVC4 {
-
-/*
- * Implements context-dependent variable-sized boolean vector
- */
-class CDBV :public context::ContextObj {
-  uint64_t d_data;
-  CDBV* d_next;
-
-  CDBV(const CDBV& cdbv) : ContextObj(cdbv), d_data(cdbv.d_data), d_next(cdbv.d_next) {}
-
-  /**
-   * operator= for CDBV is private to ensure CDBV object is not copied.
-   */
-  CDBV& operator=(const CDBV& cdbv);
-
-protected:
-  context::ContextObj* save(context::ContextMemoryManager* pCMM) {
-    return new(pCMM) CDBV(*this);
-  }
-
-  void restore(context::ContextObj* pContextObj) {
-    d_data = ((CDBV*) pContextObj)->d_data;
-  }
-
-  uint64_t data() { return d_data; }
-
-  CDBV* next() { return d_next; }
-
-public:
-  CDBV(context::Context* context) :
-    ContextObj(context), d_data(0), d_next(NULL)
-  {}
-
-  ~CDBV() {
-    if (d_next != NULL) {
-      d_next->deleteSelf();
-    }
-    destroy();
-  }
-  void clear() { d_data = 0; if( d_next ) d_next->clear(); }
-  bool read(unsigned index) {
-    if (index < 64) return (d_data & (uint64_t(1) << index)) != 0;
-    else if (d_next == NULL) return false;
-    else return d_next->read(index - 64);
-  }
-
-  void write(unsigned index) {
-    if (index < 64) {
-      uint64_t mask = uint64_t(1) << index;
-      if ((d_data & mask) != 0) return;
-      makeCurrent();
-      d_data = d_data | mask;
-    }
-    else if (d_next != NULL) {
-      d_next->write(index - 64);
-    }
-    else {
-      makeCurrent();
-      d_next = new(true) CDBV(getContext());
-      d_next->write(index - 64);
-    }
-  }
-
-  void merge(CDBV* pcdbv) {
-    d_data = d_data | pcdbv->data();
-    if (d_next != NULL && pcdbv->next() != NULL) {
-      d_next->merge(pcdbv->next());
-    }
-  }
-
-};
-
-
-/**
- * Transitive closure module for CVC4.
- *
- */
-class TransitiveClosure {
-  context::Context* d_context;
-  std::vector<CDBV* > adjMatrix;
-  context::CDO<unsigned> adjIndex;
-
-public:
-  TransitiveClosure(context::Context* context) : d_context(context), adjIndex(context,0) {}
-  virtual ~TransitiveClosure();
-
-  /* Add an edge from node i to node j.  Return false if successful, true if this edge would create a cycle */
-  bool addEdge(unsigned i, unsigned j);
-  /** whether node i is connected to node j */
-  bool isConnected(unsigned i, unsigned j);
-  void debugPrintMatrix();
-};
-
-/**
- * Transitive closure module for nodes in CVC4.
- *
- */
-class TransitiveClosureNode : public TransitiveClosure{
-  context::CDO< unsigned > d_counter;
-  context::CDHashMap< Node, unsigned, NodeHashFunction > nodeMap;
-  //for debugging
-  context::CDList< std::pair< Node, Node > > currEdges;
-public:
-  TransitiveClosureNode(context::Context* context) :
-    TransitiveClosure(context), d_counter( context, 0 ), nodeMap( context ), currEdges(context) {}
-  ~TransitiveClosureNode(){}
-
-  /** get id for node */
-  unsigned getId( Node i );
-  /** Add an edge from node i to node j.  Return false if successful, true if this edge would create a cycle */
-  bool addEdgeNode(Node i, Node j) {
-    currEdges.push_back( std::pair< Node, Node >( i, j ) );
-    return addEdge( getId( i ), getId( j ) );
-  }
-  /** whether node i is connected to node j */
-  bool isConnectedNode(Node i, Node j) {
-    return isConnected( getId( i ), getId( j ) );
-  }
-  void debugPrint();
-};
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__UTIL__TRANSITIVE_CLOSURE_H */