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, 13 insertions, 17 deletions

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;
   }
 }
-
-
-