Move Datatype management to ExprManager (#3568)

This is further work towards decoupling the Expr layer from the Node layer.

This commit makes it so that ExprManager does memory management for Datatype while NodeManager maintains a list of DType.

As a reminder, the ownership policy (and level of indirection through DatatypeIndex) is necessary due to not being able to store Datatype within Node since this leads to circular dependencies in the Node AST.

7 files changed, 64 insertions, 46 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();
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 22a491af5..f8448f1e9 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -24,11 +24,12 @@
 #include <typeinfo>
 #include <vector>
 
-#include "expr/expr.h" // for ExprSetDepth etc..
-#include "expr/node_manager_attributes.h" // for VarNameAttr
-#include "options/language.h" // for LANG_AST
-#include "printer/dagification_visitor.h"
+#include "expr/dtype.h"
+#include "expr/expr.h"                     // for ExprSetDepth etc..
+#include "expr/node_manager_attributes.h"  // for VarNameAttr
+#include "options/language.h"              // for LANG_AST
 #include "options/smt_options.h"
+#include "printer/dagification_visitor.h"
 #include "smt/command.h"
 #include "smt/smt_engine.h"
 #include "smt_util/node_visitor.h"
@@ -179,7 +180,9 @@ void CvcPrinter::toStream(
       break;
 
     case kind::DATATYPE_TYPE: {
-      const Datatype& dt = (NodeManager::currentNM()->getDatatypeForIndex( n.getConst< DatatypeIndexConstant >().getIndex() ));
+      const Datatype& dt =
+          NodeManager::currentNM()->toExprManager()->getDatatypeForIndex(
+              n.getConst<DatatypeIndexConstant>().getIndex());
       if( dt.isTuple() ){
         out << '[';
         for (unsigned i = 0; i < dt[0].getNumArgs(); ++ i) {
@@ -347,14 +350,17 @@ void CvcPrinter::toStream(
 
     // DATATYPES
     case kind::PARAMETRIC_DATATYPE: {
-        const Datatype & dt = (NodeManager::currentNM()->getDatatypeForIndex( n[0].getConst< DatatypeIndexConstant >().getIndex() ));
-        out << dt.getName() << '[';
-        for(unsigned i = 1; i < n.getNumChildren(); ++i) {
-          if(i > 1) {
-            out << ',';
-          }
-          out << n[i];
+      const DType& dt = NodeManager::currentNM()->getDTypeForIndex(
+          n[0].getConst<DatatypeIndexConstant>().getIndex());
+      out << dt.getName() << '[';
+      for (unsigned i = 1; i < n.getNumChildren(); ++i)
+      {
+        if (i > 1)
+        {
+          out << ',';
         }
+        out << n[i];
+      }
         out << ']';
       }
       return;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 006895df7..f0a1e740f 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -21,6 +21,7 @@
 #include <typeinfo>
 #include <vector>
 
+#include "expr/dtype.h"
 #include "expr/node_manager_attributes.h"
 #include "options/bv_options.h"
 #include "options/language.h"
@@ -246,7 +247,7 @@ void Smt2Printer::toStream(std::ostream& out,
 
     case kind::DATATYPE_TYPE:
     {
-      const Datatype& dt = (NodeManager::currentNM()->getDatatypeForIndex(
+      const DType& dt = (NodeManager::currentNM()->getDTypeForIndex(
           n.getConst<DatatypeIndexConstant>().getIndex()));
       if (dt.isTuple())
       {