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.

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 1981d0a7d90dcde074fae4d084ada20cbca77143..8bf8d9e54683fd06c88f2619178d525cbf8f211c 100644 (file)
--- 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 44871ff99cd726dc07bccb48da224d5861c49df7..c61c7e012df88ee3a4232207914cc99a848bb7bd 100644 (file)
--- 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 0c3f1b4cb2ff67e15f2beb1af33c60b2405d9403..39be675ec678c8112d962e276d817b734d14ecc0 100644 (file)
--- 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 61ef1d39dbf9c77d381f7da06e5d683cbef9684e..eced00c48d5339cbabe27427ff6c603db0cde218 100644 (file)
--- 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 99fe73c22208a66d53378d4e45e1d09a89beec70..031dcb3f092f7a6d254831f01f05ebc3473bbe2e 100644 (file)
--- 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 22a491af54e7be4e9b7720ba91c3f84707ae26e7..f8448f1e9a309b3f9fbe48e816a44fd6ff289a06 100644 (file)
--- 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 006895df733fc91a1ea365845cb91b59b69c1f42..f0a1e740f4acfe4aa4bca02afdf64dd1fa55459c 100644 (file)
--- 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())
       {