From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 14 Jul 2020 14:33:01 +0000 (-0700)
Subject: Use TypeNode in EmptySet (#4740)
X-Git-Tag: cvc5-1.0.0~3112
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c13527bfa6b47ff4675b429b5e7bb7c6f43ff595;p=cvc5.git

Use TypeNode in EmptySet (#4740)

This commit changes EmptySet to use TypeNode instead of Type.
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 3cca1a071..456e5a606 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -3380,7 +3380,8 @@ Term Solver::mkEmptySet(Sort s) const
   CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || this == s.d_solver, s)
       << "set sort associated to this solver object";
 
-  return mkValHelper<CVC4::EmptySet>(CVC4::EmptySet(*s.d_type));
+  return mkValHelper<CVC4::EmptySet>(
+      CVC4::EmptySet(TypeNode::fromType(*s.d_type)));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
diff --git a/src/expr/emptyset.cpp b/src/expr/emptyset.cpp
index 1c8950b55..6260e4373 100644
--- a/src/expr/emptyset.cpp
+++ b/src/expr/emptyset.cpp
@@ -17,10 +17,9 @@
 
 #include "expr/emptyset.h"
 
-#include <iosfwd>
+#include <iostream>
 
-#include "expr/expr.h"
-#include "expr/type.h"
+#include "expr/type_node.h"
 
 namespace CVC4 {
 
@@ -29,30 +28,24 @@ std::ostream& operator<<(std::ostream& out, const EmptySet& asa) {
 }
 
 size_t EmptySetHashFunction::operator()(const EmptySet& es) const {
-  return TypeHashFunction()(es.getType());
+  return TypeNodeHashFunction()(es.getType());
 }
 
 /**
  * Constructs an emptyset of the specified type. Note that the argument
  * is the type of the set itself, NOT the type of the elements.
  */
-EmptySet::EmptySet(const SetType& setType)
-    : d_type(new SetType(setType))
-{ }
+EmptySet::EmptySet(const TypeNode& setType) : d_type(new TypeNode(setType)) {}
 
-EmptySet::EmptySet(const EmptySet& es)
-    : d_type(new SetType(es.getType()))
-{ }
+EmptySet::EmptySet(const EmptySet& es) : d_type(new TypeNode(es.getType())) {}
 
 EmptySet& EmptySet::operator=(const EmptySet& es) {
   (*d_type) = es.getType();
   return *this;
 }
 
-EmptySet::~EmptySet() { delete d_type; }
-const SetType& EmptySet::getType() const {
-  return *d_type;
-}
+EmptySet::~EmptySet() {}
+const TypeNode& EmptySet::getType() const { return *d_type; }
 bool EmptySet::operator==(const EmptySet& es) const
 {
   return getType() == es.getType();
diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h
index 55e07747e..1b5bc6897 100644
--- a/src/expr/emptyset.h
+++ b/src/expr/emptyset.h
@@ -17,33 +17,29 @@
 
 #include "cvc4_public.h"
 
-#pragma once
+#ifndef CVC4__EMPTY_SET_H
+#define CVC4__EMPTY_SET_H
 
 #include <iosfwd>
+#include <memory>
 
 namespace CVC4 {
-  // messy; Expr needs EmptySet (because it's the payload of a
-  // CONSTANT-kinded expression), EmptySet needs SetType, and
-  // SetType needs Expr. Using a forward declaration here in
-  // order to break the build cycle.
-  // Uses of SetType need to be as an incomplete type throughout
-  // this header.
-  class SetType;
-}/* CVC4 namespace */
 
-namespace CVC4 {
-class CVC4_PUBLIC EmptySet {
+class TypeNode;
+
+class CVC4_PUBLIC EmptySet
+{
  public:
   /**
    * Constructs an emptyset of the specified type. Note that the argument
    * is the type of the set itself, NOT the type of the elements.
    */
-  EmptySet(const SetType& setType);
+  EmptySet(const TypeNode& setType);
   ~EmptySet();
   EmptySet(const EmptySet& other);
   EmptySet& operator=(const EmptySet& other);
 
-  const SetType& getType() const;
+  const TypeNode& getType() const;
   bool operator==(const EmptySet& es) const;
   bool operator!=(const EmptySet& es) const;
   bool operator<(const EmptySet& es) const;
@@ -52,17 +48,18 @@ class CVC4_PUBLIC EmptySet {
   bool operator>=(const EmptySet& es) const;
 
  private:
-  /** Pointer to the SetType node. This is never NULL. */
-  SetType* d_type;
-
   EmptySet();
 
-};/* class EmptySet */
+  std::unique_ptr<TypeNode> d_type;
+}; /* class EmptySet */
 
 std::ostream& operator<<(std::ostream& out, const EmptySet& es) CVC4_PUBLIC;
 
-struct CVC4_PUBLIC EmptySetHashFunction {
+struct CVC4_PUBLIC EmptySetHashFunction
+{
   size_t operator()(const EmptySet& es) const;
-};/* struct EmptySetHashFunction */
+}; /* struct EmptySetHashFunction */
+
+}  // namespace CVC4
 
-}/* CVC4 namespace */
+#endif /* CVC4__EMPTY_SET_H */
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 132d4bfaa..226736e8f 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -181,8 +181,8 @@ private:
     if(n.getMetaKind() == metakind::CONSTANT) {
       if(n.getKind() == kind::EMPTYSET) {
         Type type = d_from->exportType(
-            n.getConst< ::CVC4::EmptySet>().getType(), d_to, d_vmap);
-        return d_to->mkConst(::CVC4::EmptySet(type));
+            n.getConst< ::CVC4::EmptySet>().getType().toType(), d_to, d_vmap);
+        return d_to->mkConst(::CVC4::EmptySet(TypeNode::fromType(type)));
       }
       return exportConstant(n, NodeManager::fromExprManager(d_to), d_vmap);
     } else if(n.getMetaKind() == metakind::NULLARY_OPERATOR ){
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 499cba457..1a28a16eb 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -959,7 +959,7 @@ public:
   /**
    * Convert a type node to a type.
    */
-  inline Type toType(TypeNode tn);
+  inline Type toType(const TypeNode& tn);
 
   /**
    * Convert a type to a type node.
@@ -1184,7 +1184,8 @@ inline NodeManager* NodeManager::fromExprManager(ExprManager* exprManager) {
   return exprManager->getNodeManager();
 }
 
-inline Type NodeManager::toType(TypeNode tn) {
+inline Type NodeManager::toType(const TypeNode& tn)
+{
   return Type(this, new TypeNode(tn));
 }
 
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 372800b2b..e9b186ae2 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -378,7 +378,8 @@ void TheorySep::check(Effort e) {
               }
               std::vector< Node > labels;
               getLabelChildren( s_atom, s_lbl, children, labels );
-              Node empSet = NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType().toType()));
+              Node empSet =
+                  NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType()));
               Assert(children.size() > 1);
               if( s_atom.getKind()==kind::SEP_STAR ){
                 //reduction for heap : union, pairwise disjoint
@@ -429,9 +430,11 @@ void TheorySep::check(Effort e) {
               //conc = conc.isNull() ? ssn : NodeManager::currentNM()->mkNode( kind::AND, conc, ssn );
               
             }else if( s_atom.getKind()==kind::SEP_EMP ){
-              //conc = s_lbl.eqNode( NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType().toType())) );
+              // conc = s_lbl.eqNode(
+              // NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType())) );
               Node lem;
-              Node emp_s = NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType().toType()));
+              Node emp_s =
+                  NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType()));
               if( polarity ){
                 lem = NodeManager::currentNM()->mkNode( kind::OR, fact.negate(), s_lbl.eqNode( emp_s ) );
               }else{
@@ -1235,7 +1238,7 @@ Node TheorySep::mkUnion( TypeNode tn, std::vector< Node >& locs ) {
   Node u;
   if( locs.empty() ){
     TypeNode ltn = NodeManager::currentNM()->mkSetType(tn);
-    return NodeManager::currentNM()->mkConst(EmptySet(ltn.toType()));
+    return NodeManager::currentNM()->mkConst(EmptySet(ltn));
   }else{
     for( unsigned i=0; i<locs.size(); i++ ){
       Node s = locs[i];
@@ -1343,7 +1346,7 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
             return Node::null();
           }
         }
-        Node empSet = NodeManager::currentNM()->mkConst(EmptySet(rtn.toType()));
+        Node empSet = NodeManager::currentNM()->mkConst(EmptySet(rtn));
         if( n.getKind()==kind::SEP_STAR ){
 
           //disjoint contraints
@@ -1435,7 +1438,8 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
       return ret;
     }else if( n.getKind()==kind::SEP_EMP ){
       //return NodeManager::currentNM()->mkConst( lbl_v.getKind()==kind::EMPTYSET );
-      return lbl_v.eqNode( NodeManager::currentNM()->mkConst(EmptySet(lbl_v.getType().toType())) );
+      return lbl_v.eqNode(
+          NodeManager::currentNM()->mkConst(EmptySet(lbl_v.getType())));
     }else{
       std::map< Node, Node >::iterator it = visited.find( n );
       if( it==visited.end() ){
@@ -1780,7 +1784,7 @@ void TheorySep::debugPrintHeap( HeapInfo& heap, const char * c ) {
 Node TheorySep::HeapInfo::getValue( TypeNode tn ) {
   Assert(d_heap_locs.size() == d_heap_locs_model.size());
   if( d_heap_locs.empty() ){
-    return NodeManager::currentNM()->mkConst(EmptySet(tn.toType()));
+    return NodeManager::currentNM()->mkConst(EmptySet(tn));
   }else if( d_heap_locs.size()==1 ){
     return d_heap_locs[0];
   }else{
diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp
index e993d05dd..10348a415 100644
--- a/src/theory/sep/theory_sep_rewriter.cpp
+++ b/src/theory/sep/theory_sep_rewriter.cpp
@@ -110,7 +110,8 @@ RewriteResponse TheorySepRewriter::postRewrite(TNode node) {
         }
       }
       if( node[0].getKind()==kind::SEP_EMP ){
-        retNode = node[1].eqNode( NodeManager::currentNM()->mkConst(EmptySet(node[1].getType().toType())) );
+        retNode = node[1].eqNode(
+            NodeManager::currentNM()->mkConst(EmptySet(node[1].getType())));
       }
       break;
     }
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 */
 
diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h
index 19d36614d..67a36200f 100644
--- a/test/unit/theory/theory_sets_type_enumerator_white.h
+++ b/test/unit/theory/theory_sets_type_enumerator_white.h
@@ -56,7 +56,7 @@ class SetEnumeratorWhite : public CxxTest::TestSuite
 
     Node actual0 = *setEnumerator;
     Node expected0 =
-        d_nm->mkConst(EmptySet(d_nm->mkSetType(boolType).toType()));
+        d_nm->mkConst(EmptySet(d_nm->mkSetType(boolType)));
     TS_ASSERT_EQUALS(expected0, actual0);
     TS_ASSERT(!setEnumerator.isFinished());
 
@@ -92,7 +92,7 @@ class SetEnumeratorWhite : public CxxTest::TestSuite
 
     Node actual0 = *setEnumerator;
     Node expected0 =
-        d_nm->mkConst(EmptySet(d_nm->mkSetType(typeNode).toType()));
+        d_nm->mkConst(EmptySet(d_nm->mkSetType(typeNode)));
     TS_ASSERT_EQUALS(expected0, actual0);
     TS_ASSERT(!setEnumerator.isFinished());
 
@@ -158,7 +158,7 @@ class SetEnumeratorWhite : public CxxTest::TestSuite
 
     Node actual0 = *setEnumerator;
     Node expected0 =
-        d_nm->mkConst(EmptySet(d_nm->mkSetType(datatype).toType()));
+        d_nm->mkConst(EmptySet(d_nm->mkSetType(datatype)));
     TS_ASSERT_EQUALS(expected0, actual0);
     TS_ASSERT(!setEnumerator.isFinished());
 
@@ -217,7 +217,7 @@ class SetEnumeratorWhite : public CxxTest::TestSuite
 
     Node actual0 = *setEnumerator;
     Node expected0 =
-        d_nm->mkConst(EmptySet(d_nm->mkSetType(bitVector2).toType()));
+        d_nm->mkConst(EmptySet(d_nm->mkSetType(bitVector2)));
     TS_ASSERT_EQUALS(expected0, actual0);
     TS_ASSERT(!setEnumerator.isFinished());