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.

1 files changed, 10 insertions, 2 deletions

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}