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.

2 files changed, 7 insertions, 5 deletions

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) {