Introduce the Node-level Datatypes API (#3462)

This adds classes corresponding to the Node-level Datatype API "DType", which is a specification for a datatype type. It does not enable the use of this layer yet. A followup PR will update the Expr-level Datatype to use the Node-level code, which is currently verified to be functional on this branch: https://github.com/ajreynol/CVC4/tree/dtype-integrate. Futher PRs will make the internal (Node-level) code forgo the use of the Expr-layer datatype, which will then enable the Expr-layer to be replaced by the Term-layer datatype.

Most of the documentation for the methods in DType/DTypeConstructor/DTypeSelector was copied from Datatype/DatatypeConstructor/DatatypeConstructorArg.

1 files changed, 14 insertions, 0 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 5223fd02c..201e428de 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -24,6 +24,7 @@
 #include "base/check.h"
 #include "base/listener.h"
 #include "expr/attribute.h"
+#include "expr/dtype.h"
 #include "expr/node_manager_attributes.h"
 #include "expr/node_manager_listeners.h"
 #include "expr/type_checker.h"
@@ -186,6 +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();
@@ -253,10 +255,22 @@ unsigned NodeManager::registerDatatype(Datatype* dt) {
 }
 
 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
+{
+  // when the Node-level API is in place, this function will be replaced by a
+  // direct lookup into a d_ownedDTypes vector, similar to d_ownedDatatypes
+  // above.
+  Unreachable() << "NodeManager::getDTypeForIndex: DType is not available in "
+                   "the current implementation.";
+  const Datatype& d = getDatatypeForIndex(index);
+  return *d.d_internal;
+}
+
 void NodeManager::reclaimZombies() {
   // FIXME multithreading
   Assert(!d_attrManager->inGarbageCollection());