From 5f207ba01302c3245e169bfbe2ed91ad0cd659cd Mon Sep 17 00:00:00 2001
From: Tim King <taking@google.com>
Date: Fri, 18 Dec 2015 17:19:07 -0800
Subject: 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.
---
 src/parser/cvc/Cvc.g   | 7 ++++---
 src/parser/smt2/Smt2.g | 3 ++-
 2 files changed, 6 insertions(+), 4 deletions(-)

(limited to 'src/parser')

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index ff3753a67..efa51963a 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -434,7 +434,7 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em,
 
   Expr e = createPrecedenceTree(parser, em, expressions, operators, 0, expressions.size() - 1);
   if(Debug.isOn("prec") && operators.size() > 1) {
-    Expr::setlanguage::Scope ls(Debug("prec"), language::output::LANG_AST);
+    language::SetLanguage::Scope ls(Debug("prec"), language::output::LANG_AST);
     Debug("prec") << "=> " << e << std::endl;
   }
   return e;
@@ -487,6 +487,7 @@ Expr addNots(ExprManager* em, size_t n, Expr e) {
 
 #include <stdint.h>
 #include <cassert>
+#include "options/set_language.h"
 #include "parser/antlr_tracing.h"
 #include "parser/parser.h"
 #include "smt_util/command.h"
@@ -995,7 +996,7 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::stri
                             << "with type " << oldType << std::endl;
             if(oldType != t) {
               std::stringstream ss;
-              ss << Expr::setlanguage(language::output::LANG_CVC4)
+              ss << language::SetLanguage(language::output::LANG_CVC4)
                  << "incompatible type for `" << *i << "':" << std::endl
                  << "  old type: " << oldType << std::endl
                  << "  new type: " << t << std::endl;
@@ -1418,7 +1419,7 @@ letDecl
   std::string name;
 }
   : identifier[name,CHECK_NONE,SYM_VARIABLE] EQUAL_TOK formula[e]
-    { Debug("parser") << Expr::setlanguage(language::output::LANG_CVC4) << e.getType() << std::endl;
+    { Debug("parser") << language::SetLanguage(language::output::LANG_CVC4) << e.getType() << std::endl;
       PARSER_STATE->defineVar(name, e);
       Debug("parser") << "LET[" << PARSER_STATE->scopeLevel() << "]: "
                       << name << std::endl
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 8ac1fa34c..7f639762a 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -111,6 +111,7 @@ namespace CVC4 {
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/type.h"
+#include "options/set_language.h"
 #include "parser/antlr_input.h"
 #include "parser/parser.h"
 #include "parser/smt2/smt2.h"
@@ -1466,7 +1467,7 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
     { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); }
   | builtinOp[k]
     { std::stringstream ss;
-      ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2_5) << EXPR_MANAGER->mkConst(k);
+      ss << language::SetLanguage(CVC4::language::output::LANG_SMTLIB_V2_5) << EXPR_MANAGER->mkConst(k);
       sexpr = SExpr(ss.str());
     }
   ;
-- 
cgit v1.2.3