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.

7 files changed, 41 insertions, 37 deletions

diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp
index 7390eefe0..68de230fe 100644
--- a/examples/api/sets.cpp
+++ b/examples/api/sets.cpp
@@ -18,6 +18,7 @@
 
 //#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
 #include "smt/smt_engine.h"
+#include "options/set_language.h"
 
 using namespace std;
 using namespace CVC4;
@@ -34,8 +35,8 @@ int main() {
   smt.setOption("produce-models", true);
 
   // Set output language to SMTLIB2
-  cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
-  
+  cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
+
   Type integer = em.integerType();
   Type set = em.mkSetType(integer);
 
diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp
index 14ab0e64d..2e5d467d3 100644
--- a/examples/api/strings.cpp
+++ b/examples/api/strings.cpp
@@ -18,6 +18,7 @@
 
 //#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
 #include "smt/smt_engine.h"
+#include "options/set_language.h"
 
 using namespace CVC4;
 
@@ -35,8 +36,8 @@ int main() {
   smt.setOption("strings-exp", true);
 
   // Set output language to SMTLIB2
-  std::cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
-  
+  std::cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
+
   // String type
   Type string = em.stringType();
 
diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp
index e23be29bf..9ed4424ba 100644
--- a/examples/hashsmt/sha1_collision.cpp
+++ b/examples/hashsmt/sha1_collision.cpp
@@ -22,16 +22,17 @@
  *      Author: dejan
  */
 
-#include <string>
+#include <boost/uuid/sha1.hpp>
 #include <fstream>
 #include <iostream>
 #include <sstream>
+#include <string>
 
-#include "word.h"
+#include "options/language.h"
+#include "options/set_language.h"
 #include "sha1.hpp"
 #include "smt_util/command.h"
-
-#include <boost/uuid/sha1.hpp>
+#include "word.h"
 
 using namespace std;
 using namespace CVC4;
@@ -69,7 +70,7 @@ int main(int argc, char* argv[]) {
 
     // The output
     ofstream output(argv[3]);
-    output << expr::ExprSetDepth(-1) << expr::ExprSetLanguage(language::output::LANG_SMTLIB_V2);
+    output << expr::ExprSetDepth(-1) << language::SetLanguage(language::output::LANG_SMTLIB_V2);
     output << SetBenchmarkLogicCommand("QF_BV") << endl;
     output << SetBenchmarkStatusCommand(SMT_UNSATISFIABLE) << endl;
 
@@ -103,6 +104,3 @@ int main(int argc, char* argv[]) {
     cerr << e << endl;
   }
 }
-
-
-
diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp
index fadc6ecb9..15c7d8728 100644
--- a/examples/hashsmt/sha1_inversion.cpp
+++ b/examples/hashsmt/sha1_inversion.cpp
@@ -22,16 +22,17 @@
  *      Author: dejan
  */
 
-#include <string>
+#include <boost/uuid/sha1.hpp>
 #include <fstream>
 #include <iostream>
 #include <sstream>
+#include <string>
 
-#include "word.h"
+#include "options/language.h"
+#include "options/set_language.h"
 #include "sha1.hpp"
 #include "smt_util/command.h"
-
-#include <boost/uuid/sha1.hpp>
+#include "word.h"
 
 using namespace std;
 using namespace CVC4;
@@ -50,7 +51,7 @@ int main(int argc, char* argv[]) {
     string msg = argv[1];
     unsigned msgSize = msg.size();
     ofstream output(argv[2]);
-    output << expr::ExprSetDepth(-1) << expr::ExprSetLanguage(language::output::LANG_SMTLIB_V2);
+    output << expr::ExprSetDepth(-1) << language::SetLanguage(language::output::LANG_SMTLIB_V2);
     output << SetBenchmarkLogicCommand("QF_BV") << endl;
     output << SetBenchmarkStatusCommand(SMT_SATISFIABLE) << endl;
 
@@ -58,7 +59,7 @@ int main(int argc, char* argv[]) {
     hashsmt::cvc4_uchar8 *cvc4input = new hashsmt::cvc4_uchar8[msgSize];
     for (unsigned i = 0; i < msgSize; ++ i) {
       stringstream ss;
-      ss << "x" << i; 
+      ss << "x" << i;
       cvc4input[i] = hashsmt::cvc4_uchar8(ss.str());
       output << DeclareFunctionCommand(ss.str(), cvc4input[i].getExpr(), cvc4input[i].getExpr().getType()) << endl;
 
@@ -102,6 +103,3 @@ int main(int argc, char* argv[]) {
     cerr << e << endl;
   }
 }
-
-
-
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;
 }
-
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;
diff --git a/examples/translator.cpp b/examples/translator.cpp
index 522d88573..7d5e912e7 100644
--- a/examples/translator.cpp
+++ b/examples/translator.cpp
@@ -24,6 +24,7 @@
 
 #include "expr/expr.h"
 #include "options/language.h"
+#include "options/set_language.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "smt/smt_engine.h"
@@ -97,7 +98,7 @@ static void readFile(const char* filename, InputLanguage fromLang, OutputLanguag
     toLang = toOutputLanguage(fromLang);
   }
 
-  *out << Expr::setlanguage(toLang);
+  *out << language::SetLanguage(toLang);
 
   Options opts;
   opts.set(options::inputLanguage, fromLang);