diff options
Diffstat (limited to 'src/parser/smt2')
-rw-r--r-- | src/parser/smt2/Smt2.g | 9 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 5 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 15 | ||||
-rw-r--r-- | src/parser/smt2/smt2_input.cpp | 5 | ||||
-rw-r--r-- | src/parser/smt2/smt2_input.h | 2 | ||||
-rw-r--r-- | src/parser/smt2/sygus_input.cpp | 5 |
6 files changed, 31 insertions, 10 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 7f639762a..8be9ad2dd 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -40,6 +40,10 @@ options { @lexer::includes { +// This should come immediately after #include <antlr3.h> in the generated +// files. See the documentation in "parser/antlr_undefines.h" for more details. +#include "parser/antlr_undefines.h" + /** This suppresses warnings about the redefinition of token symbols between * different parsers. The redefinitions should be harmless as long as no * client: (a) #include's the lexer headers for two grammars AND (b) uses the @@ -75,6 +79,11 @@ using namespace CVC4::parser; }/* @lexer::postinclude */ @parser::includes { + +// This should come immediately after #include <antlr3.h> in the generated +// files. See the documentation in "parser/antlr_undefines.h" for more details. +#include "parser/antlr_undefines.h" + #include "parser/parser.h" #include "parser/antlr_tracing.h" #include "smt_util/command.h" diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 355b58067..3b1467b5e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -20,6 +20,7 @@ #include "parser/antlr_input.h" #include "parser/parser.h" #include "parser/smt1/smt1.h" +#include "parser/smt2/smt2_input.h" #include "smt_util/command.h" #include "util/bitvector.h" @@ -40,6 +41,10 @@ Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOn } } +void Smt2::setLanguage(InputLanguage lang) { + ((Smt2Input*) getInput())->setLanguage(lang); +} + void Smt2::addArithmeticOperators() { Parser::addOperator(kind::PLUS); Parser::addOperator(kind::MINUS); diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index c8b89799c..7cf92f008 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -19,16 +19,15 @@ #ifndef __CVC4__PARSER__SMT2_H #define __CVC4__PARSER__SMT2_H +#include <sstream> +#include <stack> +#include <string> +#include <utility> + #include "parser/parser.h" #include "parser/smt1/smt1.h" #include "theory/logic_info.h" #include "util/abstract_value.h" -#include "parser/smt2/smt2_input.h" - -#include <string> -#include <sstream> -#include <utility> -#include <stack> namespace CVC4 { @@ -115,9 +114,7 @@ public: return getInput()->getLanguage() == language::input::LANG_SYGUS; } - void setLanguage(InputLanguage lang) { - ((Smt2Input*) getInput())->setLanguage(lang); - } + void setLanguage(InputLanguage lang); void setInfo(const std::string& flag, const SExpr& sexpr); diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 9f1fae16f..cea6db278 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -14,9 +14,14 @@ ** [[ Add file-specific comments here ]] **/ +// These headers should be the first two included. +// See the documentation in "parser/antlr_undefines.h" for more details. #include <antlr3.h> +#include "parser/antlr_undefines.h" + #include "parser/smt2/smt2_input.h" + #include "expr/expr_manager.h" #include "parser/input.h" #include "parser/parser.h" diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 0eb4a504b..9a07ddc08 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -26,7 +26,7 @@ // extern void Smt2ParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser); namespace CVC4 { - + class Command; class Expr; class ExprManager; diff --git a/src/parser/smt2/sygus_input.cpp b/src/parser/smt2/sygus_input.cpp index 086a04d27..e4f36b3df 100644 --- a/src/parser/smt2/sygus_input.cpp +++ b/src/parser/smt2/sygus_input.cpp @@ -14,9 +14,14 @@ ** [[ Add file-specific comments here ]] **/ +// These headers should be the first two included. +// See the documentation in "parser/antlr_undefines.h" for more details. #include <antlr3.h> +#include "parser/antlr_undefines.h" + #include "parser/smt2/sygus_input.h" + #include "expr/expr_manager.h" #include "parser/input.h" #include "parser/parser.h" |