5 files changed, 44 insertions, 33 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 1981d0a7d..8bf8d9e54 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -115,10 +115,11 @@ ExprManager::~ExprManager()
       }
     }
 #endif
+    // clear the datatypes
+    d_ownedDatatypes.clear();
 
     delete d_nodeManager;
     d_nodeManager = NULL;
-
   } catch(Exception& e) {
     Warning() << "CVC4 threw an exception during cleanup." << std::endl
               << e << std::endl;
@@ -676,10 +677,11 @@ std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(
   std::map<std::string, DatatypeType> nameResolutions;
   std::vector<DatatypeType> dtts;
 
-  //have to build deep copy so that datatypes will live in NodeManager
+  // have to build deep copy so that datatypes will live in this class
   std::vector< Datatype* > dt_copies;
   for(std::vector<Datatype>::iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; ++i) {
-    dt_copies.push_back( new Datatype( *i ) );
+    d_ownedDatatypes.push_back(std::unique_ptr<Datatype>(new Datatype(*i)));
+    dt_copies.push_back(d_ownedDatatypes.back().get());
   }
 
   // First do some sanity checks, set up the final Type to be used for
@@ -689,12 +691,12 @@ std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(
   // pred selector.
   for(std::vector<Datatype*>::iterator i = dt_copies.begin(), i_end = dt_copies.end(); i != i_end; ++i) {
     TypeNode* typeNode;
+    // register datatype with the node manager
+    unsigned index = d_nodeManager->registerDatatype((*i)->d_internal);
     if( (*i)->getNumParameters() == 0 ) {
-      unsigned index = d_nodeManager->registerDatatype( *i );
       typeNode = new TypeNode(d_nodeManager->mkTypeConst(DatatypeIndexConstant(index)));
       //typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
     } else {
-      unsigned index = d_nodeManager->registerDatatype( *i );
       TypeNode cons = d_nodeManager->mkTypeConst(DatatypeIndexConstant(index));
       //TypeNode cons = d_nodeManager->mkTypeConst(*i);
       std::vector< TypeNode > params;
@@ -1098,6 +1100,13 @@ Type ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapColle
               new TypeNode(expr::exportTypeInternal(*t.d_typeNode, t.d_nodeManager, em->d_nodeManager, vmap)));
 }
 
+const Datatype& ExprManager::getDatatypeForIndex(unsigned index) const
+{
+  // when the Node-level API is in place, this function will be deleted.
+  Assert(index < d_ownedDatatypes.size());
+  return *d_ownedDatatypes[index];
+}
+
 ${mkConst_implementations}
 
 }/* CVC4 namespace */
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 44871ff99..c61c7e012 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -79,9 +79,11 @@ private:
   // undefined, private copy constructor and assignment op (disallow copy)
   ExprManager(const ExprManager&) = delete;
   ExprManager& operator=(const ExprManager&) = delete;
-  
-public:
 
+  /** A list of datatypes owned by this expr manager. */
+  std::vector<std::unique_ptr<Datatype> > d_ownedDatatypes;
+
+ public:
   /**
    * Creates an expression manager with default options.
    */
@@ -571,6 +573,12 @@ public:
   /** Returns the maximum arity of the given kind. */
   static unsigned maxArity(Kind kind);
 
+  /**
+   * Return the datatype at the given index owned by this class. Type nodes are
+   * associated with datatypes through the DatatypeIndexConstant class. The
+   * argument index is intended to be a value taken from that class.
+   */
+  const Datatype& getDatatypeForIndex(unsigned index) const;
 };/* class ExprManager */
 
 ${mkConst_instantiations}
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 0c3f1b4cb..39be675ec 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -187,15 +187,7 @@ NodeManager::~NodeManager() {
   d_rt_cache.d_children.clear();
   d_rt_cache.d_data = dummy;
 
-  // TODO: switch to DType
-  for (std::vector<Datatype*>::iterator
-           datatype_iter = d_ownedDatatypes.begin(),
-           datatype_end = d_ownedDatatypes.end();
-       datatype_iter != datatype_end; ++datatype_iter) {
-    Datatype* datatype = *datatype_iter;
-    delete datatype;
-  }
-  d_ownedDatatypes.clear();
+  d_ownedDTypes.clear();
 
   Assert(!d_attrManager->inGarbageCollection());
 
@@ -248,23 +240,17 @@ NodeManager::~NodeManager() {
   d_options = NULL;
 }
 
-unsigned NodeManager::registerDatatype(Datatype* dt) {
-  unsigned sz = d_ownedDatatypes.size();
-  d_ownedDatatypes.push_back( dt );
+size_t NodeManager::registerDatatype(std::shared_ptr<DType> dt)
+{
+  size_t sz = d_ownedDTypes.size();
+  d_ownedDTypes.push_back(dt);
   return sz;
 }
 
-const Datatype & NodeManager::getDatatypeForIndex( unsigned index ) const{
-  // when the Node-level API is in place, this function will be deleted.
-  Assert(index < d_ownedDatatypes.size());
-  return *d_ownedDatatypes[index];
-}
-
 const DType& NodeManager::getDTypeForIndex(unsigned index) const
 {
-  const Datatype& d = getDatatypeForIndex(index);
-  // return its internal representation
-  return *d.d_internal;
+  Assert(index < d_ownedDTypes.size());
+  return *d_ownedDTypes[index];
 }
 
 void NodeManager::reclaimZombies() {
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 61ef1d39d..eced00c48 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -178,7 +178,7 @@ class NodeManager {
   std::vector<NodeManagerListener*> d_listeners;
 
   /** A list of datatypes owned by this node manager. */
-  std::vector<Datatype*> d_ownedDatatypes;
+  std::vector<std::shared_ptr<DType> > d_ownedDTypes;
 
   /**
    * A map of tuple and record types to their corresponding datatype.
@@ -428,9 +428,17 @@ public:
   }
   
   /** register datatype */
-  unsigned registerDatatype(Datatype* dt);
-  /** get datatype for index */
-  const Datatype & getDatatypeForIndex( unsigned index ) const;
+  size_t registerDatatype(std::shared_ptr<DType> dt);
+  /**
+   * Return the datatype at the given index owned by this class. Type nodes are
+   * associated with datatypes through the DatatypeIndexConstant class. The
+   * argument index is intended to be a value taken from that class.
+   *
+   * Type nodes must access their DTypes through a level of indirection to
+   * prevent cycles in the Node AST (as DTypes themselves contain Nodes), which
+   * would lead to memory leaks. Thus TypeNode are given a DatatypeIndexConstant
+   * which is used as an index to retrieve the DType via this call.
+   */
   const DType& getDTypeForIndex(unsigned index) const;
 
   /** Get a Kind from an operator expression */
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 99fe73c22..031dcb3f0 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -576,7 +576,7 @@ const Datatype& DatatypeType::getDatatype() const {
   if (d_typeNode->getKind() == kind::DATATYPE_TYPE)
   {
     DatatypeIndexConstant dic = d_typeNode->getConst<DatatypeIndexConstant>();
-    return d_nodeManager->getDatatypeForIndex(dic.getIndex());
+    return d_nodeManager->toExprManager()->getDatatypeForIndex(dic.getIndex());
   }
   Assert(d_typeNode->getKind() == kind::PARAMETRIC_DATATYPE);
   return DatatypeType((*d_typeNode)[0].toType()).getDatatype();