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.

21 files changed, 524 insertions, 294 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 35211a49a..d44bae7ee 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -29,6 +29,7 @@
 #include "expr/sexpr.h"
 #include "options/expr_options.h"
 #include "options/parser_options.h"
+#include "options/set_language.h"
 #include "options/smt_options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -1521,7 +1522,7 @@ void ValidityChecker::printExpr(const Expr& e) {
 void ValidityChecker::printExpr(const Expr& e, std::ostream& os) {
   Expr::setdepth::Scope sd(os, -1);
   Expr::printtypes::Scope pt(os, false);
-  Expr::setlanguage::Scope sl(os, d_em->getOptions()[CVC4::options::outputLanguage]);
+  CVC4::language::SetLanguage::Scope sl(os, d_em->getOptions()[CVC4::options::outputLanguage]);
   os << e;
 }
 
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index c758fe297..09fe2cdc3 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -27,6 +27,7 @@
 #include "expr/node.h"
 #include "expr/node_manager.h"
 #include "expr/type.h"
+#include "options/set_language.h"
 
 using namespace std;
 
@@ -934,7 +935,7 @@ std::string DatatypeConstructorArg::getTypeName() const {
   // Unfortunately, in the case of complex selector types, we can
   // enter nontrivial recursion here.  Make sure that doesn't happen.
   stringstream ss;
-  ss << Expr::setlanguage(language::output::LANG_CVC4);
+  ss << language::SetLanguage(language::output::LANG_CVC4);
   ss.iword(s_printDatatypeNamesOnly) = 1;
   t.toStream(ss);
   return ss.str();
@@ -961,7 +962,7 @@ std::ostream& operator<<(std::ostream& os, const Datatype& dt) {
   Debug("datatypes-output") << "printNameOnly is now " << printNameOnly << std::endl;
 
   // can only output datatypes in the CVC4 native language
-  Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4);
+  language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
 
   os << "DATATYPE " << dt.getName();
   if(dt.isParametric()) {
@@ -992,7 +993,7 @@ std::ostream& operator<<(std::ostream& os, const Datatype& dt) {
 
 std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) {
   // can only output datatypes in the CVC4 native language
-  Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4);
+  language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
 
   os << ctor.getName();
 
@@ -1013,7 +1014,7 @@ std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) {
 
 std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) {
   // can only output datatypes in the CVC4 native language
-  Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4);
+  language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
 
   os << arg.getName() << ": " << arg.getTypeName();
 
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 */
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 */
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 0739e3355..dbd7c049b 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -45,7 +45,6 @@ namespace expr {
 const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc();
 const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc();
 const int ExprDag::s_iosIndex = std::ios_base::xalloc();
-const int ExprSetLanguage::s_iosIndex = std::ios_base::xalloc();
 
 }/* CVC4::expr namespace */
 
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index f609d8990..2e2f17742 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -80,7 +80,6 @@ namespace expr {
   class CVC4_PUBLIC ExprSetDepth;
   class CVC4_PUBLIC ExprPrintTypes;
   class CVC4_PUBLIC ExprDag;
-  class CVC4_PUBLIC ExprSetLanguage;
 
   class ExportPrivate;
 }/* CVC4::expr namespace */
@@ -550,11 +549,6 @@ public:
   typedef expr::ExprDag dag;
 
   /**
-   * IOStream manipulator to set the output language for Exprs.
-   */
-  typedef expr::ExprSetLanguage setlanguage;
-
-  /**
    * Very basic pretty printer for Expr.
    * This is equivalent to calling e.getNode().printAst(...)
    * @param out output stream to print to.
@@ -847,90 +841,6 @@ public:
   };/* class ExprDag::Scope */
 
 };/* class ExprDag */
-
-/**
- * IOStream manipulator to set the output language for Exprs.
- */
-class CVC4_PUBLIC ExprSetLanguage {
-  /**
-   * The allocated index in ios_base for our depth setting.
-   */
-  static const int s_iosIndex;
-
-  /**
-   * The default language to use, for ostreams that haven't yet had a
-   * setlanguage() applied to them and where the current Options
-   * information isn't available.
-   */
-  static const int s_defaultOutputLanguage = language::output::LANG_AUTO;
-
-  /**
-   * When this manipulator is used, the setting is stored here.
-   */
-  OutputLanguage d_language;
-
-public:
-  /**
-   * Construct a ExprSetLanguage with the given setting.
-   */
-  ExprSetLanguage(OutputLanguage l) : d_language(l) {}
-
-  inline void applyLanguage(std::ostream& out) {
-    // (offset by one to detect whether default has been set yet)
-    out.iword(s_iosIndex) = int(d_language) + 1;
-  }
-
-  static inline OutputLanguage getLanguage(std::ostream& out) {
-    long& l = out.iword(s_iosIndex);
-    if(l == 0) {
-      // set the default language on this ostream
-      // (offset by one to detect whether default has been set yet)
-      if(not Options::isCurrentNull()) {
-        l = options::outputLanguage() + 1;
-      }
-      if(l <= 0 || l > language::output::LANG_MAX) {
-        // if called from outside the library, we may not have options
-        // available to us at this point (or perhaps the output language
-        // is not set in Options).  Default to something reasonable, but
-        // don't set "l" since that would make it "sticky" for this
-        // stream.
-        return OutputLanguage(s_defaultOutputLanguage);
-      }
-    }
-    return OutputLanguage(l - 1);
-  }
-
-  static inline void setLanguage(std::ostream& out, OutputLanguage l) {
-    // (offset by one to detect whether default has been set yet)
-    out.iword(s_iosIndex) = int(l) + 1;
-  }
-
-  /**
-   * Set a language on the output stream for the current stack scope.
-   * This makes sure the old language is reset on the stream after
-   * normal OR exceptional exit from the scope, using the RAII C++
-   * idiom.
-   */
-  class Scope {
-    std::ostream& d_out;
-    OutputLanguage d_oldLanguage;
-
-  public:
-
-    inline Scope(std::ostream& out, OutputLanguage language) :
-      d_out(out),
-      d_oldLanguage(ExprSetLanguage::getLanguage(out)) {
-      ExprSetLanguage::setLanguage(out, language);
-    }
-
-    inline ~Scope() {
-      ExprSetLanguage::setLanguage(d_out, d_oldLanguage);
-    }
-
-  };/* class ExprSetLanguage::Scope */
-
-};/* class ExprSetLanguage */
-
 }/* CVC4::expr namespace */
 
 ${getConst_instantiations}
@@ -981,20 +891,6 @@ inline std::ostream& operator<<(std::ostream& out, ExprDag d) {
   return out;
 }
 
-/**
- * Sets the output language when pretty-printing a Expr to an ostream.
- * Use like this:
- *
- *   // let out be an ostream, e an Expr
- *   out << Expr::setlanguage(LANG_SMTLIB_V2_5) << e << endl;
- *
- * The setting stays permanently (until set again) with the stream.
- */
-inline std::ostream& operator<<(std::ostream& out, ExprSetLanguage l) {
-  l.applyLanguage(out);
-  return out;
-}
-
 }/* CVC4::expr namespace */
 
 inline size_t ExprHashFunction::operator()(CVC4::Expr e) const {
diff --git a/src/expr/node.h b/src/expr/node.h
index 384dbcc03..f345ba552 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -38,6 +38,7 @@
 #include "expr/metakind.h"
 #include "expr/expr.h"
 #include "options/language.h"
+#include "options/set_language.h"
 #include "util/configuration.h"
 #include "util/utility.h"
 #include "util/hash.h"
@@ -864,7 +865,7 @@ public:
   /**
    * IOStream manipulator to set the output language for Exprs.
    */
-  typedef expr::ExprSetLanguage setlanguage;
+  typedef language::SetLanguage setlanguage;
 
   /**
    * Very basic pretty printer for Node.
diff --git a/src/expr/sexpr.cpp b/src/expr/sexpr.cpp
index b8ffca5e5..0c0828616 100644
--- a/src/expr/sexpr.cpp
+++ b/src/expr/sexpr.cpp
@@ -30,6 +30,7 @@
 
 #include "base/cvc4_assert.h"
 #include "expr/expr.h"
+#include "options/set_language.h"
 #include "util/smt2_quote_string.h"
 
 
@@ -42,13 +43,151 @@ std::ostream& operator<<(std::ostream& out, PrettySExprs ps) {
   return out;
 }
 
+
+SExpr::~SExpr() {
+  if(d_children != NULL){
+    delete d_children;
+    d_children = NULL;
+  }
+  Assert(d_children == NULL);
+}
+
+SExpr& SExpr::operator=(const SExpr& other) {
+  d_sexprType = other.d_sexprType;
+  d_integerValue = other.d_integerValue;
+  d_rationalValue = other.d_rationalValue;
+  d_stringValue = other.d_stringValue;
+
+  if(d_children == NULL && other.d_children == NULL){
+    // Do nothing.
+  } else if(d_children == NULL){
+    d_children = new SExprVector(*other.d_children);
+  } else if(other.d_children == NULL){
+    delete d_children;
+    d_children = NULL;
+  } else {
+    (*d_children) = other.getChildren();
+  }
+  Assert( isAtom() == other.isAtom() );
+  Assert( (d_children == NULL) == isAtom() );
+  return *this;
+}
+
+SExpr::SExpr() :
+    d_sexprType(SEXPR_STRING),
+    d_integerValue(0),
+    d_rationalValue(0),
+    d_stringValue(""),
+    d_children(NULL) {
+}
+
+
+SExpr::SExpr(const SExpr& other) :
+    d_sexprType(other.d_sexprType),
+    d_integerValue(other.d_integerValue),
+    d_rationalValue(other.d_rationalValue),
+    d_stringValue(other.d_stringValue),
+    d_children(NULL)
+{
+  d_children = (other.d_children == NULL) ? NULL : new SExprVector(*other.d_children);
+  // d_children being NULL is equivalent to the node being an atom.
+  Assert( (d_children == NULL) == isAtom() );
+}
+
+
+SExpr::SExpr(const CVC4::Integer& value) :
+    d_sexprType(SEXPR_INTEGER),
+    d_integerValue(value),
+    d_rationalValue(0),
+    d_stringValue(""),
+    d_children(NULL) {
+  }
+
+SExpr::SExpr(int value) :
+    d_sexprType(SEXPR_INTEGER),
+    d_integerValue(value),
+    d_rationalValue(0),
+    d_stringValue(""),
+    d_children(NULL) {
+}
+
+SExpr::SExpr(long int value) :
+    d_sexprType(SEXPR_INTEGER),
+    d_integerValue(value),
+    d_rationalValue(0),
+    d_stringValue(""),
+    d_children(NULL) {
+}
+
+SExpr::SExpr(unsigned int value) :
+    d_sexprType(SEXPR_INTEGER),
+    d_integerValue(value),
+    d_rationalValue(0),
+    d_stringValue(""),
+    d_children(NULL) {
+}
+
+SExpr::SExpr(unsigned long int value) :
+    d_sexprType(SEXPR_INTEGER),
+    d_integerValue(value),
+    d_rationalValue(0),
+    d_stringValue(""),
+    d_children(NULL) {
+}
+
+SExpr::SExpr(const CVC4::Rational& value) :
+    d_sexprType(SEXPR_RATIONAL),
+    d_integerValue(0),
+    d_rationalValue(value),
+    d_stringValue(""),
+    d_children(NULL) {
+}
+
+SExpr::SExpr(const std::string& value) :
+    d_sexprType(SEXPR_STRING),
+    d_integerValue(0),
+    d_rationalValue(0),
+    d_stringValue(value),
+    d_children(NULL) {
+}
+
+  /**
+   * This constructs a string expression from a const char* value.
+   * This cannot be removed in order to support SExpr("foo").
+   * Given the other constructors this SExpr("foo") converts to bool.
+   * instead of SExpr(string("foo")).
+   */
+SExpr::SExpr(const char* value) :
+    d_sexprType(SEXPR_STRING),
+    d_integerValue(0),
+    d_rationalValue(0),
+    d_stringValue(value),
+    d_children(NULL) {
+}
+
 #warning "TODO: Discuss this change with Clark."
 SExpr::SExpr(bool value) :
     d_sexprType(SEXPR_KEYWORD),
     d_integerValue(0),
     d_rationalValue(0),
     d_stringValue(value ? "true" : "false"),
-    d_children() {
+    d_children(NULL) {
+}
+
+SExpr::SExpr(const Keyword& value) :
+    d_sexprType(SEXPR_KEYWORD),
+    d_integerValue(0),
+    d_rationalValue(0),
+    d_stringValue(value.getString()),
+    d_children(NULL) {
+}
+
+SExpr::SExpr(const std::vector<SExpr>& children) :
+    d_sexprType(SEXPR_NOT_ATOM),
+    d_integerValue(0),
+    d_rationalValue(0),
+    d_stringValue(""),
+    d_children(new SExprVector(children)) {
 }
 
 std::string SExpr::toString() const {
@@ -57,13 +196,39 @@ std::string SExpr::toString() const {
   return ss.str();
 }
 
+/** Is this S-expression an atom? */
+bool SExpr::isAtom() const {
+  return d_sexprType != SEXPR_NOT_ATOM;
+}
+
+/** Is this S-expression an integer? */
+bool SExpr::isInteger() const {
+  return d_sexprType == SEXPR_INTEGER;
+}
+
+/** Is this S-expression a rational? */
+bool SExpr::isRational() const {
+  return d_sexprType == SEXPR_RATIONAL;
+}
+
+/** Is this S-expression a string? */
+bool SExpr::isString() const {
+  return d_sexprType == SEXPR_STRING;
+}
+
+/** Is this S-expression a keyword? */
+bool SExpr::isKeyword() const {
+  return d_sexprType == SEXPR_KEYWORD;
+}
+
+
 std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) {
   SExpr::toStream(out, sexpr);
   return out;
 }
 
 void SExpr::toStream(std::ostream& out, const SExpr& sexpr) throw() {
-  toStream(out, sexpr, Expr::setlanguage::getLanguage(out));
+  toStream(out, sexpr, language::SetLanguage::getLanguage(out));
 }
 
 void SExpr::toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language) throw() {
@@ -181,15 +346,22 @@ const CVC4::Rational& SExpr::getRationalValue() const {
 
 const std::vector<SExpr>& SExpr::getChildren() const {
   CheckArgument( !isAtom(), this );
-  return d_children;
+  Assert( d_children != NULL );
+  return *d_children;
 }
 
 bool SExpr::operator==(const SExpr& s) const {
-  return d_sexprType == s.d_sexprType &&
-         d_integerValue == s.d_integerValue &&
-         d_rationalValue == s.d_rationalValue &&
-         d_stringValue == s.d_stringValue &&
-         d_children == s.d_children;
+  if (d_sexprType == s.d_sexprType &&
+      d_integerValue == s.d_integerValue &&
+      d_rationalValue == s.d_rationalValue &&
+      d_stringValue == s.d_stringValue) {
+    if(d_children == NULL && s.d_children == NULL){
+      return true;
+    } else if(d_children != NULL && s.d_children != NULL){
+      return getChildren() == s.getChildren();
+    }
+  }
+  return false;
 }
 
 bool SExpr::operator!=(const SExpr& s) const {
diff --git a/src/expr/sexpr.h b/src/expr/sexpr.h
index 158be0efb..40fd9dd56 100644
--- a/src/expr/sexpr.h
+++ b/src/expr/sexpr.h
@@ -27,7 +27,7 @@
 #define __CVC4__SEXPR_H
 
 #include <iomanip>
-#include <sstream>
+#include <iosfwd>
 #include <string>
 #include <vector>
 
@@ -50,94 +50,25 @@ public:
  * string value, or a list of other S-expressions.
  */
 class CVC4_PUBLIC SExpr {
-
-  enum SExprTypes {
-    SEXPR_STRING,
-    SEXPR_KEYWORD,
-    SEXPR_INTEGER,
-    SEXPR_RATIONAL,
-    SEXPR_NOT_ATOM
-  } d_sexprType;
-
-  /** The value of an atomic integer-valued S-expression. */
-  CVC4::Integer d_integerValue;
-
-  /** The value of an atomic rational-valued S-expression. */
-  CVC4::Rational d_rationalValue;
-
-  /** The value of an atomic S-expression. */
-  std::string d_stringValue;
-
-  /** The children of a list S-expression. */
-  std::vector<SExpr> d_children;
-
 public:
 
   typedef SExprKeyword Keyword;
 
-  SExpr() :
-    d_sexprType(SEXPR_STRING),
-    d_integerValue(0),
-    d_rationalValue(0),
-    d_stringValue(""),
-    d_children() {
-  }
+  SExpr();
+  SExpr(const SExpr&);
+  SExpr& operator=(const SExpr& other);
+  ~SExpr();
 
-  SExpr(const CVC4::Integer& value) :
-    d_sexprType(SEXPR_INTEGER),
-    d_integerValue(value),
-    d_rationalValue(0),
-    d_stringValue(""),
-    d_children() {
-  }
+  SExpr(const CVC4::Integer& value);
 
-  SExpr(int value) :
-    d_sexprType(SEXPR_INTEGER),
-    d_integerValue(value),
-    d_rationalValue(0),
-    d_stringValue(""),
-    d_children() {
-  }
+  SExpr(int value);
+  SExpr(long int value);
+  SExpr(unsigned int value);
+  SExpr(unsigned long int value);
 
-  SExpr(long int value) :
-    d_sexprType(SEXPR_INTEGER),
-    d_integerValue(value),
-    d_rationalValue(0),
-    d_stringValue(""),
-    d_children() {
-  }
+  SExpr(const CVC4::Rational& value);
 
-  SExpr(unsigned int value) :
-    d_sexprType(SEXPR_INTEGER),
-    d_integerValue(value),
-    d_rationalValue(0),
-    d_stringValue(""),
-    d_children() {
-  }
-
-  SExpr(unsigned long int value) :
-    d_sexprType(SEXPR_INTEGER),
-    d_integerValue(value),
-    d_rationalValue(0),
-    d_stringValue(""),
-    d_children() {
-  }
-
-  SExpr(const CVC4::Rational& value) :
-    d_sexprType(SEXPR_RATIONAL),
-    d_integerValue(0),
-    d_rationalValue(value),
-    d_stringValue(""),
-    d_children() {
-  }
-
-  SExpr(const std::string& value) :
-    d_sexprType(SEXPR_STRING),
-    d_integerValue(0),
-    d_rationalValue(0),
-    d_stringValue(value),
-    d_children() {
-  }
+  SExpr(const std::string& value);
 
   /**
    * This constructs a string expression from a const char* value.
@@ -145,60 +76,30 @@ public:
    * Given the other constructors this SExpr("foo") converts to bool.
    * instead of SExpr(string("foo")).
    */
-  SExpr(const char* value) :
-    d_sexprType(SEXPR_STRING),
-    d_integerValue(0),
-    d_rationalValue(0),
-    d_stringValue(value),
-    d_children() {
-  }
+  SExpr(const char* value);
 
   /**
    * This adds a convenience wrapper to SExpr to cast from bools.
    * This is internally handled as the strings "true" and "false"
    */
   SExpr(bool value);
-
-  SExpr(const Keyword& value) :
-    d_sexprType(SEXPR_KEYWORD),
-    d_integerValue(0),
-    d_rationalValue(0),
-    d_stringValue(value.getString()),
-    d_children() {
-  }
-
-  SExpr(const std::vector<SExpr>& children) :
-    d_sexprType(SEXPR_NOT_ATOM),
-    d_integerValue(0),
-    d_rationalValue(0),
-    d_stringValue(""),
-    d_children(children) {
-  }
+  SExpr(const Keyword& value);
+  SExpr(const std::vector<SExpr>& children);
 
   /** Is this S-expression an atom? */
-  bool isAtom() const {
-    return d_sexprType != SEXPR_NOT_ATOM;
-  }
+  bool isAtom() const;
 
   /** Is this S-expression an integer? */
-  bool isInteger() const {
-    return d_sexprType == SEXPR_INTEGER;
-  }
+  bool isInteger() const;
 
   /** Is this S-expression a rational? */
-  bool isRational() const {
-    return d_sexprType == SEXPR_RATIONAL;
-  }
+  bool isRational() const;
 
   /** Is this S-expression a string? */
-  bool isString() const {
-    return d_sexprType == SEXPR_STRING;
-  }
+  bool isString() const;
 
   /** Is this S-expression a keyword? */
-  bool isKeyword() const {
-    return d_sexprType == SEXPR_KEYWORD;
-  }
+  bool isKeyword() const;
 
   /**
    * This wraps the toStream() printer.
@@ -261,7 +162,7 @@ public:
 
   /**
    * Outputs the SExpr onto the ostream out. This version reads defaults to the
-   * OutputLanguage, Expr::setlanguage::getLanguage(out). The indent level is
+   * OutputLanguage, language::SetLanguage::getLanguage(out). The indent level is
    * set to 2 if PrettySExprs::getPrettySExprs() is on and is 0 otherwise.
    */
   static void toStream(std::ostream& out, const SExpr& sexpr) throw();
@@ -297,6 +198,34 @@ private:
   /** Returns true if this language quotes Keywords when printing. */
   static bool languageQuotesKeywords(OutputLanguage language);
 
+  enum SExprTypes {
+    SEXPR_STRING,
+    SEXPR_KEYWORD,
+    SEXPR_INTEGER,
+    SEXPR_RATIONAL,
+    SEXPR_NOT_ATOM
+  } d_sexprType;
+
+  /** The value of an atomic integer-valued S-expression. */
+  CVC4::Integer d_integerValue;
+
+  /** The value of an atomic rational-valued S-expression. */
+  CVC4::Rational d_rationalValue;
+
+  /** The value of an atomic S-expression. */
+  std::string d_stringValue;
+
+  typedef std::vector<SExpr> SExprVector;
+
+  /**
+   * The children of a list S-expression.
+   * Whenever the SExpr isAtom() holds, this points at NULL.
+   *
+   * This should be a pointer in case the implementation of vector<SExpr> ever
+   * directly contained or allocated an SExpr. If this happened this would trigger,
+   * either the size being infinite or SExpr() being an infinite loop.
+   */
+  SExprVector* d_children;
 };/* class SExpr */
 
 /** Prints an SExpr. */
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index bb6487bf0..a1f737d1d 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -34,6 +34,7 @@
 #include "options/main_options.h"
 #include "options/options.h"
 #include "options/printer_options.h"
+#include "options/set_language.h"
 #include "options/smt_options.h"
 #include "smt_util/command.h"
 
@@ -143,7 +144,7 @@ void CommandExecutorPortfolio::lemmaSharingInit()
 
       // important even for muzzled builds (to get result output right)
       *d_threadOptions[i][options::out]
-        << Expr::setlanguage(d_threadOptions[i][options::outputLanguage]);
+        << language::SetLanguage(d_threadOptions[i][options::outputLanguage]);
     }
   }
 }/* CommandExecutorPortfolio::lemmaSharingInit() */
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index df78df0f3..7e82e1bd1 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -38,6 +38,7 @@
 #include "options/main_options.h"
 #include "options/options.h"
 #include "options/quantifiers_options.h"
+#include "options/set_language.h"
 #include "options/smt_options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -231,7 +232,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   }
 
   // important even for muzzled builds (to get result output right)
-  *opts[options::out] << Expr::setlanguage(opts[options::outputLanguage]);
+  *opts[options::out] << language::SetLanguage(opts[options::outputLanguage]);
 
   // Create the expression manager using appropriate options
   ExprManager* exprMgr;
@@ -283,7 +284,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     opts.set(options::replayStream, new Parser::ExprStream(replayParser));
   }
   if( opts[options::replayLog] != NULL ) {
-    *opts[options::replayLog] << Expr::setlanguage(opts[options::outputLanguage]) << Expr::setdepth(-1);
+    *opts[options::replayLog] << language::SetLanguage(opts[options::outputLanguage]) << Expr::setdepth(-1);
   }
 
   int returnValue = 0;
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index d871bfb0a..cf38708e1 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -227,6 +227,8 @@ liboptions_la_SOURCES = \
 	printer_modes.h \
 	quantifiers_modes.cpp \
 	quantifiers_modes.h \
+	set_language.cpp \
+	set_language.h \
 	simplification_mode.cpp \
 	simplification_mode.h \
 	theoryof_mode.cpp \
diff --git a/src/options/language.h b/src/options/language.h
index d400b4afb..9191a1d59 100644
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -59,7 +59,7 @@ enum CVC4_PUBLIC Language {
   LANG_Z3STR,
   /** The SyGuS input language */
   LANG_SYGUS,
-  
+
   // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10
   // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES
 
diff --git a/src/options/set_language.cpp b/src/options/set_language.cpp
new file mode 100644
index 000000000..db0275e04
--- /dev/null
+++ b/src/options/set_language.cpp
@@ -0,0 +1,81 @@
+/*********************                                                        */
+/*! \file language.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): Francois Bobot, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Definition of input and output languages
+ **
+ ** Definition of input and output languages.
+ **/
+#include "options/set_language.h"
+
+#include <iosfwd>
+#include <iomanip>
+
+#include "options/language.h"
+#include "options/options.h"
+
+namespace CVC4 {
+namespace language {
+
+const int SetLanguage::s_iosIndex = std::ios_base::xalloc();
+
+SetLanguage::Scope::Scope(std::ostream& out, OutputLanguage language)
+  : d_out(out)
+  , d_oldLanguage(SetLanguage::getLanguage(out))
+{
+  SetLanguage::setLanguage(out, language);
+}
+
+SetLanguage::Scope::~Scope(){
+  SetLanguage::setLanguage(d_out, d_oldLanguage);
+}
+
+
+SetLanguage::SetLanguage(OutputLanguage l)
+  : d_language(l)
+{}
+
+void SetLanguage::applyLanguage(std::ostream& out) {
+  // (offset by one to detect whether default has been set yet)
+  out.iword(s_iosIndex) = int(d_language) + 1;
+}
+
+OutputLanguage SetLanguage::getLanguage(std::ostream& out) {
+  long& l = out.iword(s_iosIndex);
+  if(l == 0) {
+    // set the default language on this ostream
+    // (offset by one to detect whether default has been set yet)
+    if(not Options::isCurrentNull()) {
+      l = options::outputLanguage() + 1;
+    }
+    if(l <= 0 || l > language::output::LANG_MAX) {
+      // if called from outside the library, we may not have options
+      // available to us at this point (or perhaps the output language
+      // is not set in Options).  Default to something reasonable, but
+      // don't set "l" since that would make it "sticky" for this
+      // stream.
+      return OutputLanguage(s_defaultOutputLanguage);
+    }
+  }
+  return OutputLanguage(l - 1);
+}
+
+void SetLanguage::setLanguage(std::ostream& out, OutputLanguage l) {
+  // (offset by one to detect whether default has been set yet)
+  out.iword(s_iosIndex) = int(l) + 1;
+}
+
+std::ostream& operator<<(std::ostream& out, SetLanguage l) {
+  l.applyLanguage(out);
+  return out;
+}
+
+}/* CVC4::language namespace */
+}/* CVC4 namespace */
diff --git a/src/options/set_language.h b/src/options/set_language.h
new file mode 100644
index 000000000..53b0a6a63
--- /dev/null
+++ b/src/options/set_language.h
@@ -0,0 +1,99 @@
+/*********************                                                        */
+/*! \file language.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): Francois Bobot, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Definition of input and output languages
+ **
+ ** Definition of input and output languages.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__OPTIONS__SET_LANGUAGE_H
+#define __CVC4__OPTIONS__SET_LANGUAGE_H
+
+#include <iostream>
+#include "options/language.h"
+
+namespace CVC4 {
+namespace language {
+
+/**
+ * IOStream manipulator to set the output language for Exprs.
+ */
+class CVC4_PUBLIC SetLanguage {
+public:
+  /**
+   * Set a language on the output stream for the current stack scope.
+   * This makes sure the old language is reset on the stream after
+   * normal OR exceptional exit from the scope, using the RAII C++
+   * idiom.
+   */
+  class Scope {
+   public:
+    Scope(std::ostream& out, OutputLanguage language);
+    ~Scope();
+   private:
+    std::ostream& d_out;
+    OutputLanguage d_oldLanguage;
+  };/* class SetLanguage::Scope */
+
+  /**
+   * Construct a ExprSetLanguage with the given setting.
+   */
+  SetLanguage(OutputLanguage l);
+
+  void applyLanguage(std::ostream& out);
+
+  static OutputLanguage getLanguage(std::ostream& out);
+
+  static void setLanguage(std::ostream& out, OutputLanguage l);
+
+private:
+
+  /**
+   * The allocated index in ios_base for our depth setting.
+   */
+  static const int s_iosIndex;
+
+  /**
+   * The default language to use, for ostreams that haven't yet had a
+   * setlanguage() applied to them and where the current Options
+   * information isn't available.
+   */
+  static const int s_defaultOutputLanguage = language::output::LANG_AUTO;
+
+  /**
+   * When this manipulator is used, the setting is stored here.
+   */
+  OutputLanguage d_language;
+};/* class SetLanguage */
+
+
+/**
+ * Sets the output language when pretty-printing a Expr to an ostream.
+ * This is used liek this:
+ *
+ *   // let out be an ostream, e an Expr
+ *   out << language::SetLanguage(LANG_SMTLIB_V2_5) << e << endl;
+ *
+ * This used to be used like this:
+ *
+ *   // let out be an ostream, e an Expr
+ *   out << Expr::setlanguage(LANG_SMTLIB_V2_5) << e << endl;
+ *
+ * The setting stays permanently (until set again) with the stream.
+ */
+std::ostream& operator<<(std::ostream& out, SetLanguage l) CVC4_PUBLIC;
+
+}/* CVC4::language namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__OPTIONS__SET_LANGUAGE_H */
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index ff3753a67..efa51963a 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -434,7 +434,7 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em,
 
   Expr e = createPrecedenceTree(parser, em, expressions, operators, 0, expressions.size() - 1);
   if(Debug.isOn("prec") && operators.size() > 1) {
-    Expr::setlanguage::Scope ls(Debug("prec"), language::output::LANG_AST);
+    language::SetLanguage::Scope ls(Debug("prec"), language::output::LANG_AST);
     Debug("prec") << "=> " << e << std::endl;
   }
   return e;
@@ -487,6 +487,7 @@ Expr addNots(ExprManager* em, size_t n, Expr e) {
 
 #include <stdint.h>
 #include <cassert>
+#include "options/set_language.h"
 #include "parser/antlr_tracing.h"
 #include "parser/parser.h"
 #include "smt_util/command.h"
@@ -995,7 +996,7 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::stri
                             << "with type " << oldType << std::endl;
             if(oldType != t) {
               std::stringstream ss;
-              ss << Expr::setlanguage(language::output::LANG_CVC4)
+              ss << language::SetLanguage(language::output::LANG_CVC4)
                  << "incompatible type for `" << *i << "':" << std::endl
                  << "  old type: " << oldType << std::endl
                  << "  new type: " << t << std::endl;
@@ -1418,7 +1419,7 @@ letDecl
   std::string name;
 }
   : identifier[name,CHECK_NONE,SYM_VARIABLE] EQUAL_TOK formula[e]
-    { Debug("parser") << Expr::setlanguage(language::output::LANG_CVC4) << e.getType() << std::endl;
+    { Debug("parser") << language::SetLanguage(language::output::LANG_CVC4) << e.getType() << std::endl;
       PARSER_STATE->defineVar(name, e);
       Debug("parser") << "LET[" << PARSER_STATE->scopeLevel() << "]: "
                       << name << std::endl
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 8ac1fa34c..7f639762a 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -111,6 +111,7 @@ namespace CVC4 {
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/type.h"
+#include "options/set_language.h"
 #include "parser/antlr_input.h"
 #include "parser/parser.h"
 #include "parser/smt2/smt2.h"
@@ -1466,7 +1467,7 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
     { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); }
   | builtinOp[k]
     { std::stringstream ss;
-      ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2_5) << EXPR_MANAGER->mkConst(k);
+      ss << language::SetLanguage(CVC4::language::output::LANG_SMTLIB_V2_5) << EXPR_MANAGER->mkConst(k);
       sexpr = SExpr(ss.str());
     }
   ;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index f93857796..ece4e9177 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -977,7 +977,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
 static std::string quoteSymbol(TNode n) {
 #warning "check the old implementation. It seems off."
   std::stringstream ss;
-  ss << Expr::setlanguage(language::output::LANG_SMTLIB_V2_5);
+  ss << language::SetLanguage(language::output::LANG_SMTLIB_V2_5);
   return CVC4::quoteSymbol(ss.str());
 }
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f3724b432..1bd2b059b 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -56,6 +56,7 @@
 #include "options/printer_options.h"
 #include "options/prop_options.h"
 #include "options/quantifiers_options.h"
+#include "options/set_language.h"
 #include "options/smt_options.h"
 #include "options/strings_options.h"
 #include "options/theory_options.h"
@@ -1658,7 +1659,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
       if(!options::outputLanguage.wasSetByUser() &&
          options::outputLanguage() == language::output::LANG_SMTLIB_V2_5) {
         options::outputLanguage.set(language::output::LANG_SMTLIB_V2_0);
-        *options::out() << Expr::setlanguage(language::output::LANG_SMTLIB_V2_0);
+        *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_0);
       }
       return;
     } else if( (value.isRational() && value.getRationalValue() == Rational(5, 2)) ||
@@ -1667,7 +1668,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
       if(!options::outputLanguage.wasSetByUser() &&
          options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) {
         options::outputLanguage.set(language::output::LANG_SMTLIB_V2_5);
-        *options::out() << Expr::setlanguage(language::output::LANG_SMTLIB_V2_5);
+        *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_5);
       }
       return;
     }
@@ -1774,7 +1775,7 @@ void SmtEngine::defineFunction(Expr func,
   }
 
   stringstream ss;
-  ss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump.getStream()))
+  ss << language::SetLanguage(language::SetLanguage::getLanguage(Dump.getStream()))
      << func;
   DefineFunctionCommand c(ss.str(), func, formals, formula);
   addToModelCommandAndDump(c, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
diff --git a/src/smt/smt_options_handler.cpp b/src/smt/smt_options_handler.cpp
index 3dc5720ab..371cdcddd 100644
--- a/src/smt/smt_options_handler.cpp
+++ b/src/smt/smt_options_handler.cpp
@@ -45,6 +45,7 @@
 #include "options/parser_options.h"
 #include "options/printer_modes.h"
 #include "options/quantifiers_modes.h"
+#include "options/set_language.h"
 #include "options/simplification_mode.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
@@ -1216,12 +1217,12 @@ void SmtOptionsHandler::proofEnabledBuild(std::string option, bool value) throw(
     int dagSetting = expr::ExprDag::getDag(__channel_get); \
     size_t exprDepthSetting = expr::ExprSetDepth::getDepth(__channel_get); \
     bool printtypesSetting = expr::ExprPrintTypes::getPrintTypes(__channel_get); \
-    OutputLanguage languageSetting = expr::ExprSetLanguage::getLanguage(__channel_get); \
+    OutputLanguage languageSetting = language::SetLanguage::getLanguage(__channel_get); \
     __channel_set; \
     __channel_get << Expr::dag(dagSetting); \
     __channel_get << Expr::setdepth(exprDepthSetting); \
     __channel_get << Expr::printtypes(printtypesSetting); \
-    __channel_get << Expr::setlanguage(languageSetting); \
+    __channel_get << language::SetLanguage(languageSetting); \
   }
 
 void SmtOptionsHandler::dumpToFile(std::string option, std::string optarg) {
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index f3bbc65cc..e6478440d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -579,7 +579,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
     }else{
       if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){
         std::stringstream ss;
-        ss << Expr::setlanguage(options::outputLanguage());
+        ss << language::SetLanguage(options::outputLanguage());
         ss << "e_" << tn;
         mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" );
         Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl;