Modifying emptyset.h and sexpr. Adding SetLanguage.

- Modifies expr/emptyset.h to use SetType only as an incomplete type within expr/emptyset.h. This breaks the include cycle between expr/emptyset.h, expr/expr.h and expr/type.h.
- Refactors SExpr to avoid a potentially infinite cycle. This is likely overkill, but it works.
- Moving Expr::setlanguage and related utilities out of the Expr class and into their own file. This allows files in util/ to know the output language set on an ostream.

1 files changed, 59 insertions, 1 deletions

diff --git a/src/expr/emptyset.cpp b/src/expr/emptyset.cpp
index 69e34b848..a6e2c1ece 100644
--- a/src/expr/emptyset.cpp
+++ b/src/expr/emptyset.cpp
@@ -17,7 +17,10 @@
 
 #include "expr/emptyset.h"
 
-#include <iostream>
+#include <iosfwd>
+
+#include "expr/expr.h"
+#include "expr/type.h"
 
 namespace CVC4 {
 
@@ -25,4 +28,59 @@ std::ostream& operator<<(std::ostream& out, const EmptySet& asa) {
   return out << "emptyset(" << asa.getType() << ')';
 }
 
+size_t EmptySetHashFunction::operator()(const EmptySet& es) const {
+  return TypeHashFunction()(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 EmptySet& es)
+    : d_type(new SetType(es.getType()))
+{ }
+
+EmptySet& EmptySet::operator=(const EmptySet& es) {
+  (*d_type) = es.getType();
+  return *this;
+}
+
+
+EmptySet::~EmptySet() throw() {
+  delete d_type;
+}
+
+const SetType& EmptySet::getType() const {
+  return *d_type;
+}
+
+bool EmptySet::operator==(const EmptySet& es) const throw() {
+  return getType() == es.getType();
+}
+
+bool EmptySet::operator!=(const EmptySet& es) const throw() {
+  return !(*this == es);
+}
+
+bool EmptySet::operator<(const EmptySet& es) const throw() {
+  return getType() < es.getType();
+}
+
+bool EmptySet::operator<=(const EmptySet& es) const throw() {
+  return getType() <= es.getType();
+}
+
+bool EmptySet::operator>(const EmptySet& es) const throw() {
+  return !(*this <= es);
+}
+
+bool EmptySet::operator>=(const EmptySet& es) const throw() {
+  return !(*this < es);
+}
+
+
 }/* CVC4 namespace */