Use the node-level datatypes API (#3556)

3 files changed, 39 insertions, 31 deletions

diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h
index 8ce314c94..79757d311 100644
--- a/src/theory/sets/rels_utils.h
+++ b/src/theory/sets/rels_utils.h
@@ -17,6 +17,9 @@
 #ifndef SRC_THEORY_SETS_RELS_UTILS_H_
 #define SRC_THEORY_SETS_RELS_UTILS_H_
 
+#include "expr/dtype.h"
+#include "expr/node.h"
+
 namespace CVC4 {
 namespace theory {
 namespace sets {
@@ -67,8 +70,9 @@ public:
       return tuple[n_th];
     }
     TypeNode tn = tuple.getType();
-    const Datatype& dt = tn.getDatatype();
-    return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal( tn.toType(), n_th ), tuple);
+    const DType& dt = tn.getDType();
+    return NodeManager::currentNM()->mkNode(
+        kind::APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(tn, n_th), tuple);
   } 
   
   static Node reverseTuple( Node tuple ) {
@@ -77,16 +81,17 @@ public:
     std::vector<TypeNode> tuple_types = tuple.getType().getTupleTypes();
     std::reverse( tuple_types.begin(), tuple_types.end() );
     TypeNode tn = NodeManager::currentNM()->mkTupleType( tuple_types );
-    const Datatype& dt = tn.getDatatype();
-    elements.push_back( Node::fromExpr(dt[0].getConstructor() ) );
+    const DType& dt = tn.getDType();
+    elements.push_back(dt[0].getConstructor());
     for(int i = tuple_types.size() - 1; i >= 0; --i) {
       elements.push_back( nthElementOfTuple(tuple, i) );
     }
     return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, elements );
   }
   static Node constructPair(Node rel, Node a, Node b) {
-    const Datatype& dt = rel.getType().getSetElementType().getDatatype();
-    return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), a, b);
+    const DType& dt = rel.getType().getSetElementType().getDType();
+    return NodeManager::currentNM()->mkNode(
+        kind::APPLY_CONSTRUCTOR, dt[0].getConstructor(), a, b);
   }     
     
 };             
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index e8724aa8b..2f0997982 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -299,12 +299,12 @@ void TheorySetsRels::check(Theory::Effort level)
       }
       hasChecked.insert( fst_mem_rep );
 
-      const Datatype& dt =
-          join_image_term.getType().getSetElementType().getDatatype();
-      Node new_membership = NodeManager::currentNM()->mkNode(kind::MEMBER,
-                                                             NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR,
-                                                                                               Node::fromExpr(dt[0].getConstructor()), fst_mem_rep ),
-                                                             join_image_term);
+      const DType& dt =
+          join_image_term.getType().getSetElementType().getDType();
+      Node new_membership = nm->mkNode(
+          MEMBER,
+          nm->mkNode(APPLY_CONSTRUCTOR, dt[0].getConstructor(), fst_mem_rep),
+          join_image_term);
       if (d_state.isEntailed(new_membership, true))
       {
         ++mem_rep_it;
@@ -429,9 +429,11 @@ void TheorySetsRels::check(Theory::Effort level)
     Node reason = exp;
     Node fst_mem = RelsUtils::nthElementOfTuple( exp[0], 0 );
     Node snd_mem = RelsUtils::nthElementOfTuple( exp[0], 1 );
-    const Datatype& dt =
-        iden_term[0].getType().getSetElementType().getDatatype();
-    Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), fst_mem ), iden_term[0] );
+    const DType& dt = iden_term[0].getType().getSetElementType().getDType();
+    Node fact = nm->mkNode(
+        MEMBER,
+        nm->mkNode(APPLY_CONSTRUCTOR, dt[0].getConstructor(), fst_mem),
+        iden_term[0]);
 
     if( exp[1] != iden_term ) {
       reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, exp[1], iden_term ) );
@@ -767,18 +769,18 @@ void TheorySetsRels::check(Theory::Effort level)
     Node mem = exp[0];
     std::vector<Node>   r1_element;
     std::vector<Node>   r2_element;
-    const Datatype& dt1 = pt_rel[0].getType().getSetElementType().getDatatype();
+    const DType& dt1 = pt_rel[0].getType().getSetElementType().getDType();
     unsigned int s1_len  = pt_rel[0].getType().getSetElementType().getTupleLength();
     unsigned int tup_len = pt_rel.getType().getSetElementType().getTupleLength();
 
-    r1_element.push_back(Node::fromExpr(dt1[0].getConstructor()));
+    r1_element.push_back(dt1[0].getConstructor());
 
     unsigned int i = 0;
     for(; i < s1_len; ++i) {
       r1_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
     }
-    const Datatype& dt2 = pt_rel[1].getType().getSetElementType().getDatatype();
-    r2_element.push_back(Node::fromExpr(dt2[0].getConstructor()));
+    const DType& dt2 = pt_rel[1].getType().getSetElementType().getDType();
+    r2_element.push_back(dt2[0].getConstructor());
     for(; i < tup_len; ++i) {
       r2_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
     }
@@ -825,20 +827,18 @@ void TheorySetsRels::check(Theory::Effort level)
     TypeNode     shared_type    = r2_rep.getType().getSetElementType().getTupleTypes()[0];
     Node shared_x = d_state.getSkolemCache().mkTypedSkolemCached(
         shared_type, mem, join_rel, SkolemCache::SK_JOIN, "srj");
-    const Datatype& dt1 =
-        join_rel[0].getType().getSetElementType().getDatatype();
+    const DType& dt1 = join_rel[0].getType().getSetElementType().getDType();
     unsigned int s1_len         = join_rel[0].getType().getSetElementType().getTupleLength();
     unsigned int tup_len        = join_rel.getType().getSetElementType().getTupleLength();
 
     unsigned int i = 0;
-    r1_element.push_back(Node::fromExpr(dt1[0].getConstructor()));
+    r1_element.push_back(dt1[0].getConstructor());
     for(; i < s1_len-1; ++i) {
       r1_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
     }
     r1_element.push_back(shared_x);
-    const Datatype& dt2 =
-        join_rel[1].getType().getSetElementType().getDatatype();
-    r2_element.push_back(Node::fromExpr(dt2[0].getConstructor()));
+    const DType& dt2 = join_rel[1].getType().getSetElementType().getDType();
+    r2_element.push_back(dt2[0].getConstructor());
     r2_element.push_back(shared_x);
     for(; i < tup_len; ++i) {
       r2_element.push_back(RelsUtils::nthElementOfTuple(mem, i));
@@ -1041,7 +1041,7 @@ void TheorySetsRels::check(Theory::Effort level)
         TypeNode tn = rel.getType().getSetElementType();
         Node r1_rmost = RelsUtils::nthElementOfTuple( r1_rep_exps[i][0], r1_tuple_len-1 );
         Node r2_lmost = RelsUtils::nthElementOfTuple( r2_rep_exps[j][0], 0 );
-        tuple_elements.push_back( Node::fromExpr(tn.getDatatype()[0].getConstructor()) );
+        tuple_elements.push_back(tn.getDType()[0].getConstructor());
 
         if( (areEqual(r1_rmost, r2_lmost) && rel.getKind() == kind::JOIN) ||
             rel.getKind() == kind::PRODUCT ) {
@@ -1226,7 +1226,7 @@ void TheorySetsRels::check(Theory::Effort level)
     if(d_symbolic_tuples.find(n) == d_symbolic_tuples.end()) {
       Trace("rels-debug") << "[Theory::Rels] Reduce tuple var: " << n[0] << " to a concrete one " << " node = " << n << std::endl;
       std::vector<Node> tuple_elements;
-      tuple_elements.push_back(Node::fromExpr((n[0].getType().getDatatype())[0].getConstructor()));
+      tuple_elements.push_back((n[0].getType().getDType())[0].getConstructor());
       for(unsigned int i = 0; i < n[0].getType().getTupleLength(); i++) {
         Node element = RelsUtils::nthElementOfTuple(n[0], i);
         makeSharedTerm(element);
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index a7c506582..d8f5f8c4f 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -21,6 +21,8 @@
 #include "theory/sets/normal_form.h"
 #include "theory/sets/rels_utils.h"
 
+using namespace CVC4::kind;
+
 namespace CVC4 {
 namespace theory {
 namespace sets {
@@ -281,7 +283,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
       while(left_it != left.end()) {
         Trace("rels-debug") << "Sets::postRewrite processing left_it = " <<  *left_it << std::endl;
         std::vector<Node> left_tuple;
-        left_tuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor()));
+        left_tuple.push_back(tn.getDType()[0].getConstructor());
         for(int i = 0; i < left_len; i++) {
           left_tuple.push_back(RelsUtils::nthElementOfTuple(*left_it,i));
         }
@@ -324,7 +326,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
       TypeNode tn = node.getType().getSetElementType();
       while(left_it != left.end()) {
         std::vector<Node> left_tuple;
-        left_tuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor()));
+        left_tuple.push_back(tn.getDType()[0].getConstructor());
         for(int i = 0; i < left_len - 1; i++) {
           left_tuple.push_back(RelsUtils::nthElementOfTuple(*left_it,i));
         }
@@ -431,8 +433,9 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
           ++rel_mems_it_snd;
         }
         if( existing_mems.size() >= min_card ) {
-          const Datatype& dt = node.getType().getSetElementType().getDatatype();
-          join_img_mems.insert(NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt[0].getConstructor()), fst_mem ));
+          const DType& dt = node.getType().getSetElementType().getDType();
+          join_img_mems.insert(
+              nm->mkNode(APPLY_CONSTRUCTOR, dt[0].getConstructor(), fst_mem));
         }
         ++rel_mems_it;
       }