diff options
| author | Tim King <taking@google.com> | 2015-12-18 17:19:07 -0800 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2015-12-18 17:19:07 -0800 |
| commit | 5f207ba01302c3245e169bfbe2ed91ad0cd659cd (patch) | |
| tree | e1131e8c2891e283ab028fba6a7a677bb4ac9f5f /src/parser/cvc/Cvc.g | |
| parent | 7e4468ba0aa0b08eeb4ba1a86b1fdd839ae169d6 (diff) | |
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.
Diffstat (limited to 'src/parser/cvc/Cvc.g')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 7 |
1 files changed, 4 insertions, 3 deletions
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 |