Use TypeNode in EmptySet (#4740)

This commit changes EmptySet to use TypeNode instead of Type.

6 files changed, 23 insertions, 16 deletions

diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h
index 56f09e2a5..0607a0e6c 100644
--- a/src/theory/sets/normal_form.h
+++ b/src/theory/sets/normal_form.h
@@ -34,7 +34,7 @@ class NormalForm {
     NodeManager* nm = NodeManager::currentNM();
     if (elements.size() == 0)
     {
-      return nm->mkConst(EmptySet(nm->toType(setType)));
+      return nm->mkConst(EmptySet(setType));
     }
     else
     {
@@ -128,7 +128,7 @@ class NormalForm {
   }
   static Node mkBop( Kind k, std::vector< Node >& els, TypeNode tn, unsigned index = 0 ){
     if( index>=els.size() ){
-      return NodeManager::currentNM()->mkConst(EmptySet(tn.toType()));
+      return NodeManager::currentNM()->mkConst(EmptySet(tn));
     }else if( index==els.size()-1 ){
       return els[index];
     }else{
diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp
index 057d3a791..d3c23454e 100644
--- a/src/theory/sets/solver_state.cpp
+++ b/src/theory/sets/solver_state.cpp
@@ -453,7 +453,7 @@ Node SolverState::getEmptySet(TypeNode tn)
   {
     return it->second;
   }
-  Node n = NodeManager::currentNM()->mkConst(EmptySet(tn.toType()));
+  Node n = NodeManager::currentNM()->mkConst(EmptySet(tn));
   d_emptyset[tn] = n;
   return n;
 }
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index fc2a992a9..4c3affe99 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1504,7 +1504,7 @@ TrustNode TheorySetsPrivate::expandDefinition(Node node)
     Node witnessVariable = nm->mkBoundVar(setType.getSetElementType());
 
     Node equal = witnessVariable.eqNode(apply);
-    Node emptySet = nm->mkConst(EmptySet(setType.toType()));
+    Node emptySet = nm->mkConst(EmptySet(setType));
     Node isEmpty = set.eqNode(emptySet);
     Node member = nm->mkNode(MEMBER, witnessVariable, set);
     Node memberAndEqual = member.andNode(equal);
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index c26a3852c..a7fbc8a38 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -120,7 +120,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
 
   case kind::SETMINUS: {
     if(node[0] == node[1]) {
-      Node newNode = nm->mkConst(EmptySet(nm->toType(node[0].getType())));
+      Node newNode = nm->mkConst(EmptySet(node[0].getType()));
       Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
       return RewriteResponse(REWRITE_DONE, newNode);
     } else if(node[0].getKind() == kind::EMPTYSET ||
@@ -128,7 +128,9 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
       Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl;
       return RewriteResponse(REWRITE_AGAIN, node[0]);
     }else if( node[1].getKind() == kind::UNIVERSE_SET ){
-      return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkConst(EmptySet(node[1].getType().toType())));
+      return RewriteResponse(
+          REWRITE_AGAIN,
+          NodeManager::currentNM()->mkConst(EmptySet(node[1].getType())));
     } else if(node[0].isConst() && node[1].isConst()) {
       std::set<Node> left = NormalForm::getElementsFromNormalConstant(node[0]);
       std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]);
@@ -244,7 +246,8 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
     }
 
     if(node[0].getKind() == kind::EMPTYSET) {
-      return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType()))));
+      return RewriteResponse(REWRITE_DONE,
+                             nm->mkConst(EmptySet(node.getType())));
     } else if(node[0].isConst()) {
       std::set<Node> new_tuple_set;
       std::set<Node> tuple_set = NormalForm::getElementsFromNormalConstant(node[0]);
@@ -271,7 +274,8 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
     Trace("sets-rels-postrewrite") << "Sets::postRewrite processing " <<  node << std::endl;
     if( node[0].getKind() == kind::EMPTYSET ||
         node[1].getKind() == kind::EMPTYSET) {
-      return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType()))));
+      return RewriteResponse(REWRITE_DONE,
+                             nm->mkConst(EmptySet(node.getType())));
     } else if( node[0].isConst() && node[1].isConst() ) {
       Trace("sets-rels-postrewrite") << "Sets::postRewrite processing **** " <<  node << std::endl;
       std::set<Node> new_tuple_set;
@@ -315,7 +319,8 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
   case kind::JOIN: {
     if( node[0].getKind() == kind::EMPTYSET ||
         node[1].getKind() == kind::EMPTYSET) {
-      return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType()))));
+      return RewriteResponse(REWRITE_DONE,
+                             nm->mkConst(EmptySet(node.getType())));
     } else if( node[0].isConst() && node[1].isConst() ) {
       Trace("sets-rels-postrewrite") << "Sets::postRewrite processing " <<  node << std::endl;
       std::set<Node> new_tuple_set;
@@ -359,7 +364,8 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
 
   case kind::TCLOSURE: {
     if(node[0].getKind() == kind::EMPTYSET) {
-      return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType()))));
+      return RewriteResponse(REWRITE_DONE,
+                             nm->mkConst(EmptySet(node.getType())));
     } else if (node[0].isConst()) {
       std::set<Node> rel_mems = NormalForm::getElementsFromNormalConstant(node[0]);
       std::set<Node> tc_rel_mems = RelsUtils::computeTC(rel_mems, node);
@@ -379,7 +385,8 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
   
   case kind::IDEN: {
     if(node[0].getKind() == kind::EMPTYSET) {
-      return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType()))));
+      return RewriteResponse(REWRITE_DONE,
+                             nm->mkConst(EmptySet(node.getType())));
     } else if (node[0].isConst()) {
       std::set<Node> iden_rel_mems;
       std::set<Node> rel_mems = NormalForm::getElementsFromNormalConstant(node[0]);
@@ -409,7 +416,8 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
     if( min_card == 0) {
       return RewriteResponse(REWRITE_DONE, nm->mkNullaryOperator( node.getType(), kind::UNIVERSE_SET ));
     } else if(node[0].getKind() == kind::EMPTYSET) {
-      return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType()))));
+      return RewriteResponse(REWRITE_DONE,
+                             nm->mkConst(EmptySet(node.getType())));
     } else if (node[0].isConst()) {
       std::set<Node> has_checked;
       std::set<Node> join_img_mems;
diff --git a/src/theory/sets/theory_sets_type_enumerator.cpp b/src/theory/sets/theory_sets_type_enumerator.cpp
index 5a949a95b..7f5628c66 100644
--- a/src/theory/sets/theory_sets_type_enumerator.cpp
+++ b/src/theory/sets/theory_sets_type_enumerator.cpp
@@ -28,7 +28,7 @@ SetEnumerator::SetEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
       d_currentSetIndex(0),
       d_currentSet()
 {
-  d_currentSet = d_nodeManager->mkConst(EmptySet(type.toType()));
+  d_currentSet = d_nodeManager->mkConst(EmptySet(type));
 }
 
 SetEnumerator::SetEnumerator(const SetEnumerator& enumerator)
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 753dcaf76..5d01a966a 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -139,8 +139,7 @@ struct EmptySetTypeRule {
   {
     Assert(n.getKind() == kind::EMPTYSET);
     EmptySet emptySet = n.getConst<EmptySet>();
-    Type setType = emptySet.getType();
-    return TypeNode::fromType(setType);
+    return emptySet.getType();
   }
 };/* struct EmptySetTypeRule */
 
@@ -444,7 +443,7 @@ struct SetsProperties {
 
   inline static Node mkGroundTerm(TypeNode type) {
     Assert(type.isSet());
-    return NodeManager::currentNM()->mkConst(EmptySet(type.toType()));
+    return NodeManager::currentNM()->mkConst(EmptySet(type));
   }
 };/* struct SetsProperties */