diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-12 20:29:17 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-12 20:29:17 +0000 |
commit | 8d691eac8e478576ebceb6406a8e372db5e3f7f1 (patch) | |
tree | cd808cd26804490fd5a2e938bf24fdec85918004 /src | |
parent | 05d29aa0de4c2d4d773a81375fb14584221595ea (diff) |
true and false are only defined if the core theory is loaded in SMT v2 strict mode
Diffstat (limited to 'src')
-rw-r--r-- | src/parser/antlr_input.cpp | 7 | ||||
-rw-r--r-- | src/parser/antlr_input.h | 4 | ||||
-rw-r--r-- | src/parser/input.h | 2 | ||||
-rw-r--r-- | src/parser/parser.cpp | 8 | ||||
-rw-r--r-- | src/parser/parser.h | 2 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 8 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 2 | ||||
-rw-r--r-- | src/parser/smt2/smt2_input.cpp | 8 | ||||
-rw-r--r-- | src/parser/smt2/smt2_input.h | 6 |
9 files changed, 30 insertions, 17 deletions
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 11e3ed604..fc03a2903 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -204,14 +204,13 @@ void AntlrInput::setAntlr3Lexer(pANTLR3_LEXER pLexer) { d_lexer->rec->state->tokSource->nextToken = &nextTokenStr; } -void AntlrInput::setParser(Parser *parser) { +void AntlrInput::setParser(Parser& parser) { // ANTLR isn't using super in the lexer or the parser, AFAICT. // We could also use @lexer/parser::context to add a field to the generated // objects, but then it would have to be declared separately in every // language's grammar and we'd have to in the address of the field anyway. - d_lexer->super = parser; - d_parser->super = parser; - + d_lexer->super = &parser; + d_parser->super = &parser; } void AntlrInput::setAntlr3Parser(pANTLR3_PARSER pParser) { diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 4e075e5dd..27337c35f 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -90,7 +90,7 @@ class Parser; * for the given input language and attach it to an input source of the * appropriate type. */ -class AntlrInput : public Input{ +class AntlrInput : public Input { /** The token lookahead used to lex and parse the input. This should usually be equal to * <code>K</code> for an LL(k) grammar. */ unsigned int d_lookahead; @@ -192,7 +192,7 @@ protected: void setAntlr3Parser(pANTLR3_PARSER pParser); /** Set the Parser object for this input. */ - void setParser(Parser *parser); + virtual void setParser(Parser& parser); }; inline std::string AntlrInput::tokenText(pANTLR3_COMMON_TOKEN token) { diff --git a/src/parser/input.h b/src/parser/input.h index b277f6428..114880bb0 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -150,7 +150,7 @@ protected: virtual Expr parseExpr() throw(ParserException) = 0; /** Set the Parser object for this input. */ - virtual void setParser(Parser *parser) = 0; + virtual void setParser(Parser& parser) = 0; }; }/* CVC4::parser namespace */ diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index a1d6398f0..286867e84 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -35,13 +35,13 @@ using namespace CVC4::kind; namespace CVC4 { namespace parser { -Parser::Parser(ExprManager* exprManager, Input* input) : +Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode) : d_exprManager(exprManager), d_input(input), d_done(false), d_checksEnabled(true), - d_strictMode(false) { - d_input->setParser(this); + d_strictMode(strictMode) { + d_input->setParser(*this); } Expr Parser::getSymbol(const std::string& name, SymbolType type) { @@ -111,14 +111,12 @@ Parser::mkVars(const std::vector<std::string> names, void Parser::defineVar(const std::string& name, const Expr& val) { - Assert(!isDeclared(name)); d_declScope.bind(name,val); Assert(isDeclared(name)); } void Parser::defineType(const std::string& name, const Type& type) { - Assert( !isDeclared(name, SYM_SORT) ); d_declScope.bindType(name,type); Assert( isDeclared(name, SYM_SORT) ) ; } diff --git a/src/parser/parser.h b/src/parser/parser.h index d87a97ec4..c191d9f39 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -129,7 +129,7 @@ public: * @param exprManager the expression manager to use when creating expressions * @param input the parser input */ - Parser(ExprManager* exprManager, Input* input); + Parser(ExprManager* exprManager, Input* input, bool strictMode = false); virtual ~Parser() { } diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 94a9aa30b..dec052859 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -246,8 +246,8 @@ term[CVC4::Expr& expr] { expr = PARSER_STATE->getVariable(name); } /* constants */ - | TRUE_TOK { expr = MK_CONST(true); } - | FALSE_TOK { expr = MK_CONST(false); } +// | TRUE_TOK { expr = MK_CONST(true); } +// | FALSE_TOK { expr = MK_CONST(false); } | INTEGER_LITERAL { expr = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); } | DECIMAL_LITERAL @@ -376,7 +376,7 @@ CHECKSAT_TOK : 'check-sat'; DECLARE_FUN_TOK : 'declare-fun'; DECLARE_SORT_TOK : 'declare-sort'; EXIT_TOK : 'exit'; -FALSE_TOK : 'false'; +//FALSE_TOK : 'false'; ITE_TOK : 'ite'; LET_TOK : 'let'; LPAREN_TOK : '('; @@ -388,7 +388,7 @@ SET_INFO_TOK : 'set-info'; //SMT_VERSION_TOK : ':smt-lib-version'; //SOURCE_TOK : ':source'; //STATUS_TOK : ':status'; -TRUE_TOK : 'true'; +//TRUE_TOK : 'true'; //UNKNOWN_TOK : 'unknown'; //UNSAT_TOK : 'unsat'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 4d3062d81..9fd6588bb 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -60,6 +60,8 @@ void Smt2::addTheory(Parser& parser, Theory theory) { switch(theory) { case THEORY_CORE: parser.defineType("Bool", parser.getExprManager()->booleanType()); + parser.defineVar("true", parser.getExprManager()->mkConst(true)); + parser.defineVar("false", parser.getExprManager()->mkConst(false)); parser.addOperator(kind::AND); parser.addOperator(kind::EQUAL); parser.addOperator(kind::IFF); diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index bcefe166b..6d7a04800 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -20,6 +20,7 @@ #include "parser/input.h" #include "parser/parser.h" #include "parser/parser_exception.h" +#include "parser/smt2/smt2.h" #include "parser/smt2/generated/Smt2Lexer.h" #include "parser/smt2/generated/Smt2Parser.h" @@ -64,5 +65,12 @@ Expr Smt2Input::parseExpr() throw (ParserException) { return d_pSmt2Parser->parseExpr(d_pSmt2Parser); } +void Smt2Input::setParser(Parser& parser) { + super::setParser(parser); + if( !parser.strictModeEnabled() ) { + Smt2::addTheory(parser,Smt2::THEORY_CORE); + } +} + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index ad32edcbc..c003a76ec 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -33,6 +33,7 @@ class ExprManager; namespace parser { class Smt2Input : public AntlrInput { + typedef AntlrInput super; /** The ANTLR3 SMT2 lexer for the input. */ pSmt2Lexer d_pSmt2Lexer; @@ -85,6 +86,11 @@ protected: */ Expr parseExpr() throw(ParserException); + /** Set the Parser object for this input. This implementation overrides the super-class + * implementation to add the core theory symbols to the parser state when strict + * mode is disabled. */ + virtual void setParser(Parser& parser); + };/* class Smt2Input */ }/* CVC4::parser namespace */ |