Move datatype index constant to its own file (#4859)

Towards removing the Expr-level datatype.

Moves DatatypeIndex to its own file, which is the only thing that is necessary remaining from expr/datatype.h.

Also updates the datatype kinds file in preparation for the removal.

8 files changed, 116 insertions, 56 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index bad2f1f42..993df2594 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -73,6 +73,8 @@ libcvc4_add_sources(
   variable_type_map.h
   datatype.h
   datatype.cpp
+  datatype_index.h
+  datatype_index.cpp
   dtype.h
   dtype.cpp
   dtype_cons.h
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index f8712e20e..a9ac3fbbf 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -21,6 +21,7 @@
 
 #include "base/check.h"
 #include "expr/attribute.h"
+#include "expr/datatype.h"
 #include "expr/dtype.h"
 #include "expr/expr_manager.h"
 #include "expr/expr_manager_scope.h"
@@ -851,12 +852,6 @@ void DatatypeConstructorArg::toStream(std::ostream& out) const
   out << t;
 }
 
-DatatypeIndexConstant::DatatypeIndexConstant(unsigned index) : d_index(index) {}
-std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic) {
-  return out << "index_" << dic.getIndex();
-}
-
-
 std::string Datatype::getName() const
 {
   ExprManagerScope ems(*d_em);
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 54095050f..0deb20d8f 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -36,6 +36,7 @@ namespace CVC4 {
 #include "base/exception.h"
 #include "expr/expr.h"
 #include "expr/type.h"
+#include "expr/datatype_index.h"
 #include "util/hash.h"
 
 
@@ -908,51 +909,6 @@ struct CVC4_PUBLIC DatatypeHashFunction {
 };/* struct DatatypeHashFunction */
 
 
-
-/* stores an index to Datatype residing in NodeManager */
-class CVC4_PUBLIC DatatypeIndexConstant {
- public:
-  DatatypeIndexConstant(unsigned index);
-
-  unsigned getIndex() const { return d_index; }
-  bool operator==(const DatatypeIndexConstant& uc) const
-  {
-    return d_index == uc.d_index;
-  }
-  bool operator!=(const DatatypeIndexConstant& uc) const
-  {
-    return !(*this == uc);
-  }
-  bool operator<(const DatatypeIndexConstant& uc) const
-  {
-    return d_index < uc.d_index;
-  }
-  bool operator<=(const DatatypeIndexConstant& uc) const
-  {
-    return d_index <= uc.d_index;
-  }
-  bool operator>(const DatatypeIndexConstant& uc) const
-  {
-    return !(*this <= uc);
-  }
-  bool operator>=(const DatatypeIndexConstant& uc) const
-  {
-    return !(*this < uc);
-  }
-private:
-  const unsigned d_index;
-};/* class DatatypeIndexConstant */
-
-std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic) CVC4_PUBLIC;
-
-struct CVC4_PUBLIC DatatypeIndexConstantHashFunction {
-  inline size_t operator()(const DatatypeIndexConstant& dic) const {
-    return IntegerHashFunction()(dic.getIndex());
-  }
-};/* struct DatatypeIndexConstantHashFunction */
-
-
-
 // FUNCTION DECLARATIONS FOR OUTPUT STREAMS
 
 std::ostream& operator<<(std::ostream& os, const Datatype& dt) CVC4_PUBLIC;
diff --git a/src/expr/datatype_index.cpp b/src/expr/datatype_index.cpp
new file mode 100644
index 000000000..988965b74
--- /dev/null
+++ b/src/expr/datatype_index.cpp
@@ -0,0 +1,36 @@
+/*********************                                                        */
+/*! \file datatype_index.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief A class representing an index to a datatype living in NodeManager.
+ **/
+#include "expr/datatype_index.h"
+
+#include <sstream>
+#include <string>
+#include "util/integer.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+DatatypeIndexConstant::DatatypeIndexConstant(unsigned index) : d_index(index) {}
+std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic)
+{
+  return out << "index_" << dic.getIndex();
+}
+
+size_t DatatypeIndexConstantHashFunction::operator()(
+    const DatatypeIndexConstant& dic) const
+{
+  return IntegerHashFunction()(dic.getIndex());
+}
+
+}  // namespace CVC4
diff --git a/src/expr/datatype_index.h b/src/expr/datatype_index.h
new file mode 100644
index 000000000..f871129fe
--- /dev/null
+++ b/src/expr/datatype_index.h
@@ -0,0 +1,71 @@
+/*********************                                                        */
+/*! \file datatype_index.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief A class representing an index to a datatype living in NodeManager.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef CVC4__DATATYPE_INDEX_H
+#define CVC4__DATATYPE_INDEX_H
+
+#include <iosfwd>
+#include "util/hash.h"
+
+namespace CVC4 {
+
+/* stores an index to Datatype residing in NodeManager */
+class CVC4_PUBLIC DatatypeIndexConstant
+{
+ public:
+  DatatypeIndexConstant(unsigned index);
+
+  unsigned getIndex() const { return d_index; }
+  bool operator==(const DatatypeIndexConstant& uc) const
+  {
+    return d_index == uc.d_index;
+  }
+  bool operator!=(const DatatypeIndexConstant& uc) const
+  {
+    return !(*this == uc);
+  }
+  bool operator<(const DatatypeIndexConstant& uc) const
+  {
+    return d_index < uc.d_index;
+  }
+  bool operator<=(const DatatypeIndexConstant& uc) const
+  {
+    return d_index <= uc.d_index;
+  }
+  bool operator>(const DatatypeIndexConstant& uc) const
+  {
+    return !(*this <= uc);
+  }
+  bool operator>=(const DatatypeIndexConstant& uc) const
+  {
+    return !(*this < uc);
+  }
+
+ private:
+  const unsigned d_index;
+}; /* class DatatypeIndexConstant */
+
+std::ostream& operator<<(std::ostream& out,
+                         const DatatypeIndexConstant& dic) CVC4_PUBLIC;
+
+struct CVC4_PUBLIC DatatypeIndexConstantHashFunction
+{
+  size_t operator()(const DatatypeIndexConstant& dic) const;
+}; /* struct DatatypeIndexConstantHashFunction */
+
+}  // namespace CVC4
+
+#endif /* CVC4__DATATYPE_H */
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index e3c09b635..4b80529d2 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -45,11 +45,11 @@ constant DATATYPE_TYPE \
     "a datatype type index"
 cardinality DATATYPE_TYPE \
     "%TYPE%.getDType().getCardinality(%TYPE%)" \
-    "expr/datatype.h"
+    "expr/dtype.h"
 well-founded DATATYPE_TYPE \
     "%TYPE%.getDType().isWellFounded()" \
     "%TYPE%.getDType().mkGroundTerm(%TYPE%)" \
-    "expr/datatype.h"
+    "expr/dtype.h"
 
 enumerator DATATYPE_TYPE \
     "::CVC4::theory::datatypes::DatatypesEnumerator" \
@@ -58,11 +58,11 @@ enumerator DATATYPE_TYPE \
 operator PARAMETRIC_DATATYPE 1: "parametric datatype"
 cardinality PARAMETRIC_DATATYPE \
     "%TYPE%.getDType().getCardinality(%TYPE%)" \
-    "expr/datatype.h"
+    "expr/dtype.h"
 well-founded PARAMETRIC_DATATYPE \
     "%TYPE%.getDType().isWellFounded()" \
     "%TYPE%.getDType().mkGroundTerm(%TYPE%)" \
-    "expr/datatype.h"
+    "expr/dtype.h"
 
 enumerator PARAMETRIC_DATATYPE \
     "::CVC4::theory::datatypes::DatatypesEnumerator" \
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index d6d854c44..b89015b00 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -14,7 +14,6 @@
  **/
 #include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h"
 
-#include "expr/datatype.h"
 #include "expr/dtype.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
index 847fd2d9b..23df6f3d5 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
@@ -21,6 +21,7 @@
 #include <vector>
 
 #include "context/cdhashmap.h"
+#include "expr/dtype.h"
 #include "expr/node.h"
 
 namespace CVC4 {