Use the node-level datatypes API (#3556)

3 files changed, 14 insertions, 14 deletions

diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 3a075ec8a..8e09ef6a2 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -13,6 +13,7 @@
  **/
 
 #include "theory/quantifiers/ematching/candidate_generator.h"
+#include "expr/dtype.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/inst_match.h"
 #include "theory/quantifiers/instantiate.h"
@@ -208,7 +209,7 @@ CandidateGeneratorConsExpand::CandidateGeneratorConsExpand(
     : CandidateGeneratorQE(qe, mpat)
 {
   Assert(mpat.getKind() == APPLY_CONSTRUCTOR);
-  d_mpat_type = static_cast<DatatypeType>(mpat.getType().toType());
+  d_mpat_type = mpat.getType();
 }
 
 void CandidateGeneratorConsExpand::reset(Node eqc)
@@ -222,7 +223,7 @@ void CandidateGeneratorConsExpand::reset(Node eqc)
   {
     d_eqc = eqc;
     d_mode = cand_term_ident;
-    Assert(d_eqc.getType().toType() == d_mpat_type);
+    Assert(d_eqc.getType() == d_mpat_type);
   }
 }
 
@@ -237,15 +238,13 @@ Node CandidateGeneratorConsExpand::getNextCandidate()
   // expand it
   NodeManager* nm = NodeManager::currentNM();
   std::vector<Node> children;
-  const Datatype& dt = d_mpat_type.getDatatype();
+  const DType& dt = d_mpat_type.getDType();
   Assert(dt.getNumConstructors() == 1);
   children.push_back(d_op);
   for (unsigned i = 0, nargs = dt[0].getNumArgs(); i < nargs; i++)
   {
-    Node sel =
-        nm->mkNode(APPLY_SELECTOR_TOTAL,
-                   Node::fromExpr(dt[0].getSelectorInternal(d_mpat_type, i)),
-                   curr);
+    Node sel = nm->mkNode(
+        APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(d_mpat_type, i), curr);
     children.push_back(sel);
   }
   return nm->mkNode(APPLY_CONSTRUCTOR, children);
diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h
index 8cff12477..51c5ffa0b 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.h
+++ b/src/theory/quantifiers/ematching/candidate_generator.h
@@ -203,7 +203,7 @@ class CandidateGeneratorConsExpand : public CandidateGeneratorQE
 
  protected:
   /** the (datatype) type of the input match pattern */
-  DatatypeType d_mpat_type;
+  TypeNode d_mpat_type;
   /** we don't care about the operator of n */
   bool isLegalOpCandidate(Node n) override;
 };
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index e639dc446..6fdd6d67a 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -17,6 +17,7 @@
 #include "expr/datatype.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/ematching/candidate_generator.h"
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/instantiate.h"
@@ -203,7 +204,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
       {
         // 1-constructors have a trivial way of generating candidates in a
         // given equivalence class
-        const Datatype& dt = d_match_pattern.getType().getDatatype();
+        const DType& dt = d_match_pattern.getType().getDType();
         if (dt.getNumConstructors() == 1)
         {
           d_cg = new inst::CandidateGeneratorConsExpand(qe, d_match_pattern);
@@ -226,11 +227,11 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector<
       }
     }else if( d_match_pattern.getKind()==INST_CONSTANT ){
       if( d_pattern.getKind()==APPLY_SELECTOR_TOTAL ){
-        Expr selectorExpr = qe->getTermDatabase()->getMatchOperator( d_pattern ).toExpr();
-        size_t selectorIndex = Datatype::cindexOf(selectorExpr);
-        const Datatype& dt = Datatype::datatypeOf(selectorExpr);
-        const DatatypeConstructor& c = dt[selectorIndex];
-        Node cOp = Node::fromExpr(c.getConstructor());
+        Node selectorExpr = qe->getTermDatabase()->getMatchOperator(d_pattern);
+        size_t selectorIndex = datatypes::utils::cindexOf(selectorExpr);
+        const DType& dt = datatypes::utils::datatypeOf(selectorExpr);
+        const DTypeConstructor& c = dt[selectorIndex];
+        Node cOp = c.getConstructor();
         Trace("inst-match-gen") << "Purify dt trigger " << d_pattern << ", will match terms of op " << cOp << std::endl;
         d_cg = new inst::CandidateGeneratorQE( qe, cOp );
       }else{