Use the node-level datatypes API (#3556)

1 files changed, 7 insertions, 7 deletions

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 47355aa81..6df412ae3 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -13,6 +13,7 @@
  **/
 #include "theory/theory_model_builder.h"
 
+#include "expr/dtype.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "options/uf_options.h"
@@ -198,7 +199,7 @@ bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn)
   }
   else if (tn.isDatatype())
   {
-    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+    const DType& dt = tn.getDType();
     return dt.involvesUninterpretedType();
   }
   else
@@ -264,12 +265,12 @@ void TheoryEngineModelBuilder::addToTypeList(
       }
       else if (tn.isDatatype())
       {
-        const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+        const DType& dt = tn.getDType();
         for (unsigned i = 0; i < dt.getNumConstructors(); i++)
         {
           for (unsigned j = 0; j < dt[i].getNumArgs(); j++)
           {
-            TypeNode ctn = TypeNode::fromType(dt[i][j].getRangeType());
+            TypeNode ctn = dt[i][j].getRangeType();
             addToTypeList(ctn, type_list, visiting);
           }
         }
@@ -627,10 +628,9 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
       bool isCorecursive = false;
       if (t.isDatatype())
       {
-        const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype();
-        isCorecursive =
-            dt.isCodatatype() && (!dt.isFinite(t.toType())
-                                  || dt.isRecursiveSingleton(t.toType()));
+        const DType& dt = t.getDType();
+        isCorecursive = dt.isCodatatype()
+                        && (!dt.isFinite(t) || dt.isRecursiveSingleton(t));
       }
 #ifdef CVC4_ASSERTIONS
       bool isUSortFiniteRestricted = false;