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, 9 insertions, 7 deletions

diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp
index d4aecbba9..db76390a7 100644
--- a/examples/nra-translate/normalize.cpp
+++ b/examples/nra-translate/normalize.cpp
@@ -23,7 +23,9 @@
 #include <vector>
 
 #include "expr/expr.h"
+#include "options/language.h"
 #include "options/options.h"
+#include "options/set_language.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "smt/smt_engine.h"
@@ -35,18 +37,19 @@ using namespace CVC4::parser;
 using namespace CVC4::options;
 using namespace CVC4::theory;
 
-int main(int argc, char* argv[]) 
+int main(int argc, char* argv[])
 {
 
-  // Get the filename 
+  // Get the filename
   string input(argv[1]);
 
   // Create the expression manager
   Options options;
   options.set(inputLanguage, language::input::LANG_SMTLIB_V2);
   ExprManager exprManager(options);
-  
-  cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << Expr::setdepth(-1);
+
+  cout << language::SetLanguage(language::output::LANG_SMTLIB_V2)
+       << Expr::setdepth(-1);
 
   // Create the parser
   ParserBuilder parserBuilder(&exprManager, input, options);
@@ -76,12 +79,11 @@ int main(int argc, char* argv[])
     }
 
     cout << *cmd << endl;
-    delete cmd;  
+    delete cmd;
   }
 
   cout << "(check-sat)" << endl;
-	
+
   // Get rid of the parser
   delete parser;
 }
-