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, 11 insertions, 8 deletions

diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
index c33ccb367..7e17e68f4 100644
--- a/examples/sets-translate/sets_translate.cpp
+++ b/examples/sets-translate/sets_translate.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_util/command.h"
@@ -34,7 +36,7 @@ using namespace CVC4;
 using namespace CVC4::parser;
 using namespace CVC4::options;
 
-bool nonsense(char c) { return !isalnum(c); } 
+bool nonsense(char c) { return !isalnum(c); }
 
 #ifdef ENABLE_AXIOMS
 const bool enableAxioms = true;
@@ -94,7 +96,7 @@ class Mapper {
 
       Type elementType = t.getElementType();
       ostringstream oss_type;
-      oss_type << Expr::setlanguage(language::output::LANG_SMTLIB_V2)
+      oss_type << language::SetLanguage(language::output::LANG_SMTLIB_V2)
                << elementType;
       string elementTypeAsString = oss_type.str();
       elementTypeAsString.erase(
@@ -103,7 +105,7 @@ class Mapper {
 
       // define-sort
       ostringstream oss_name;
-      oss_name << Expr::setlanguage(language::output::LANG_SMTLIB_V2)
+      oss_name << language::SetLanguage(language::output::LANG_SMTLIB_V2)
                << "(Set " << elementType << ")";
       string name = oss_name.str();
       Type newt = em->mkArrayType(t.getElementType(), em->booleanType());
@@ -184,7 +186,8 @@ class Mapper {
         int N = sizeof(setaxioms) / sizeof(setaxioms[0]);
         for(int i = 0; i < N; ++i) {
           string s = setaxioms[i];
-          ostringstream oss; oss << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << elementType;
+          ostringstream oss;
+          oss << language::SetLanguage(language::output::LANG_SMTLIB_V2) << elementType;
           boost::replace_all(s, "HOLDA", elementTypeAsString);
           boost::replace_all(s, "HOLDB", oss.str());
           if( s == "" ) continue;
@@ -207,7 +210,7 @@ class Mapper {
 
 public:
   Mapper(ExprManager* e) : em(e),depth(0) {
-    sout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
+    sout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
   }
 
   void defineSetSort() {
@@ -259,17 +262,17 @@ int main(int argc, char* argv[])
     // Create the expression manager
     Options options;
     options.set(inputLanguage, language::input::LANG_SMTLIB_V2);
-    cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
+    cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
     // cout << Expr::dag(0);
     ExprManager exprManager(options);
 
     Mapper m(&exprManager);
-  
+
     // Create the parser
     ParserBuilder parserBuilder(&exprManager, input, options);
     if(input == "<stdin>") parserBuilder.withStreamInput(cin);
     Parser* parser = parserBuilder.build();
-  
+
     // Variables and assertions
     vector<string> variables;
     vector<string> info_tags;