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, 5 insertions, 3 deletions

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;