Use TypeNode in EmptySet (#4740)

This commit changes EmptySet to use TypeNode instead of Type.

1 files changed, 7 insertions, 14 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();