Use the node-level datatypes API (#3556)

2 files changed, 14 insertions, 20 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
index 6c4f2c620..9fd682aaf 100644
--- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
@@ -14,7 +14,9 @@
 
 #include "theory/quantifiers/cegqi/ceg_dt_instantiator.h"
 
+#include "expr/dtype.h"
 #include "expr/node_algorithm.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -57,16 +59,14 @@ bool DtInstantiator::processEqualTerms(CegInstantiator* ci,
           << "...try based on constructor term " << n << std::endl;
       std::vector<Node> children;
       children.push_back(n.getOperator());
-      const Datatype& dt =
-          static_cast<DatatypeType>(d_type.toType()).getDatatype();
-      unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
+      const DType& dt = d_type.getDType();
+      unsigned cindex = datatypes::utils::indexOf(n.getOperator());
       // now must solve for selectors applied to pv
       for (unsigned j = 0, nargs = dt[cindex].getNumArgs(); j < nargs; j++)
       {
-        Node c = nm->mkNode(
-            APPLY_SELECTOR_TOTAL,
-            Node::fromExpr(dt[cindex].getSelectorInternal(d_type.toType(), j)),
-            pv);
+        Node c = nm->mkNode(APPLY_SELECTOR_TOTAL,
+                            dt[cindex].getSelectorInternal(d_type, j),
+                            pv);
         ci->pushStackVariable(c);
         children.push_back(c);
       }
@@ -146,15 +146,13 @@ Node DtInstantiator::solve_dt(Node v, Node a, Node b, Node sa, Node sb)
     else
     {
       NodeManager* nm = NodeManager::currentNM();
-      unsigned cindex = Datatype::indexOf(a.getOperator().toExpr());
+      unsigned cindex = DType::indexOf(a.getOperator().toExpr());
       TypeNode tn = a.getType();
-      const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+      const DType& dt = tn.getDType();
       for (unsigned i = 0, nchild = a.getNumChildren(); i < nchild; i++)
       {
         Node nn = nm->mkNode(
-            APPLY_SELECTOR_TOTAL,
-            Node::fromExpr(dt[cindex].getSelectorInternal(tn.toType(), i)),
-            sb);
+            APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(tn, i), sb);
         Node s = solve_dt(v, a[i], Node::null(), sa[i], nn);
         if (!s.isNull())
         {
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index bed382e28..1d4a23af1 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -341,13 +341,12 @@ CegHandledStatus CegInstantiator::isCbqiSort(
     // we initialize to handled, we remain handled as long as all subfields
     // of this datatype are not unhandled.
     ret = CEG_HANDLED;
-    const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+    const DType& dt = tn.getDType();
     for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
     {
       for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
       {
-        TypeNode crange = TypeNode::fromType(
-            static_cast<SelectorType>(dt[i][j].getType()).getRangeType());
+        TypeNode crange = dt[i].getArgType(j);
         CegHandledStatus cret = isCbqiSort(crange, visited, qe);
         if (cret == CEG_UNHANDLED)
         {
@@ -520,15 +519,12 @@ void CegInstantiator::registerTheoryIds(TypeNode tn,
     registerTheoryId(tid);
     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++)
         {
-          registerTheoryIds(
-              TypeNode::fromType(
-                  ((SelectorType)dt[i][j].getType()).getRangeType()),
-              visited);
+          registerTheoryIds(dt[i].getArgType(j), visited);
         }
       }
     }