Replace Expr-level datatype with Node-level DType (#4875)

[cvc5.git] / src / expr / type.cpp

diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 8232ef339f347f5ae42ed64f867b77aeb7007ece..5dd15dd37c5b5c4c647e613b9fb7266845dec87e 100644 (file)
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -585,19 +585,6 @@ std::vector<Type> ConstructorType::getArgTypes() const {
   return args;
 }
 
-const Datatype& DatatypeType::getDatatype() const
-{
-  NodeManagerScope nms(d_nodeManager);
-  Assert(isDatatype());
-  if (d_typeNode->getKind() == kind::DATATYPE_TYPE)
-  {
-    DatatypeIndexConstant dic = d_typeNode->getConst<DatatypeIndexConstant>();
-    return d_nodeManager->toExprManager()->getDatatypeForIndex(dic.getIndex());
-  }
-  Assert(d_typeNode->getKind() == kind::PARAMETRIC_DATATYPE);
-  return DatatypeType((*d_typeNode)[0].toType()).getDatatype();
-}
-
 bool DatatypeType::isParametric() const {
   return d_typeNode->isParametricDatatype();
 }