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, 24 insertions, 39 deletions

diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h
index 4b3bb204f..e5eada731 100644
--- a/src/expr/emptyset.h
+++ b/src/expr/emptyset.h
@@ -19,65 +19,50 @@
 
 #pragma once
 
+#include <iosfwd>
+
 namespace CVC4 {
   // messy; Expr needs EmptySet (because it's the payload of a
-  // CONSTANT-kinded expression), and EmptySet needs Expr.
-  class CVC4_PUBLIC EmptySet;
+  // 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 CVC4_PUBLIC SetType;
 }/* CVC4 namespace */
 
-#include "expr/expr.h"
-#include "expr/type.h"
-#include <iostream>
-
 namespace CVC4 {
-
 class CVC4_PUBLIC EmptySet {
-
-  const SetType d_type;
-
-  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(SetType setType):d_type(setType) { }
-
-
-  ~EmptySet() throw() {
-  }
+  EmptySet(const SetType& setType);
+  ~EmptySet() throw();
+  EmptySet(const EmptySet& other);
+  EmptySet& operator=(const EmptySet& other);
 
-  SetType getType() const { return d_type; }
+  const SetType& getType() const;
+  bool operator==(const EmptySet& es) const throw();
+  bool operator!=(const EmptySet& es) const throw();
+  bool operator<(const EmptySet& es) const throw();
+  bool operator<=(const EmptySet& es) const throw();
+  bool operator>(const EmptySet& es) const throw() ;
+  bool operator>=(const EmptySet& es) const throw();
 
-  bool operator==(const EmptySet& es) const throw() {
-    return d_type == es.d_type;
-  }
-  bool operator!=(const EmptySet& es) const throw() {
-    return !(*this == es);
-  }
+private:
+  /** Pointer to the SetType node. This is never NULL. */
+  SetType* d_type;
 
-  bool operator<(const EmptySet& es) const throw() {
-    return d_type < es.d_type;
-  }
-  bool operator<=(const EmptySet& es) const throw() {
-    return d_type <= es.d_type;
-  }
-  bool operator>(const EmptySet& es) const throw() {
-    return !(*this <= es);
-  }
-  bool operator>=(const EmptySet& es) const throw() {
-    return !(*this < es);
-  }
+  EmptySet();
 
 };/* class EmptySet */
 
 std::ostream& operator<<(std::ostream& out, const EmptySet& es) CVC4_PUBLIC;
 
 struct CVC4_PUBLIC EmptySetHashFunction {
-  inline size_t operator()(const EmptySet& es) const {
-    return TypeHashFunction()(es.getType());
-  }
+  size_t operator()(const EmptySet& es) const;
 };/* struct EmptySetHashFunction */
 
 }/* CVC4 namespace */