Use TypeNode in EmptySet (#4740)

This commit changes EmptySet to use TypeNode instead of Type.

4 files changed, 29 insertions, 38 deletions

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));
 }