diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-12 20:29:24 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-12 20:29:24 +0000 |
commit | a358ed3b520919acbb72fb9bcd2974ee4165f495 (patch) | |
tree | 52a9dd03f5735114cf196bafbc6a5ee6f5a40b22 /src/parser/smt2/Smt2.g | |
parent | 8d691eac8e478576ebceb6406a8e372db5e3f7f1 (diff) |
Adding ParserBuilder, reducing visibility of Parser and Input constructors
Adding Smt2 subclass of Parser
Checking for multiple calls to set-logic in SMT v2
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r-- | src/parser/smt2/Smt2.g | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index dec052859..105976628 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -52,14 +52,14 @@ options { @lexer::postinclude { #include <stdint.h> -#include "parser/parser.h" +#include "parser/smt2/smt2.h" #include "parser/antlr_input.h" using namespace CVC4; using namespace CVC4::parser; #undef PARSER_STATE -#define PARSER_STATE ((Parser*)LEXER->super) +#define PARSER_STATE ((Smt2*)LEXER->super) } @parser::includes { @@ -89,7 +89,7 @@ using namespace CVC4::parser; /* These need to be macros so they can refer to the PARSER macro, which will be defined * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */ #undef PARSER_STATE -#define PARSER_STATE ((Parser*)PARSER->super) +#define PARSER_STATE ((Smt2*)PARSER->super) #undef EXPR_MANAGER #define EXPR_MANAGER PARSER_STATE->getExprManager() #undef MK_EXPR @@ -132,11 +132,14 @@ command returns [CVC4::Command* cmd] SET_LOGIC_TOK SYMBOL { name = AntlrInput::tokenText($SYMBOL); Debug("parser") << "set logic: '" << name << "' " << std::endl; - Smt2::setLogic(*PARSER_STATE,name); + if( PARSER_STATE->strictModeEnabled() && PARSER_STATE->logicIsSet() ) { + PARSER_STATE->parseError("Only one set-logic is allowed."); + } + PARSER_STATE->setLogic(name); $cmd = new SetBenchmarkLogicCommand(name); } | SET_INFO_TOK KEYWORD symbolicExpr[sexpr] { name = AntlrInput::tokenText($KEYWORD); - Smt2::setInfo(*PARSER_STATE,name,sexpr); + PARSER_STATE->setInfo(name,sexpr); cmd = new SetInfoCommand(name,sexpr); } | /* sort declaration */ DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL |