From 8d691eac8e478576ebceb6406a8e372db5e3f7f1 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Wed, 12 May 2010 20:29:17 +0000 Subject: [PATCH] true and false are only defined if the core theory is loaded in SMT v2 strict mode --- src/parser/antlr_input.cpp | 7 +++---- src/parser/antlr_input.h | 4 ++-- src/parser/input.h | 2 +- src/parser/parser.cpp | 8 +++----- src/parser/parser.h | 2 +- src/parser/smt2/Smt2.g | 8 ++++---- src/parser/smt2/smt2.cpp | 2 ++ src/parser/smt2/smt2_input.cpp | 8 ++++++++ src/parser/smt2/smt2_input.h | 6 ++++++ test/unit/parser/parser_black.h | 20 ++++++++++---------- 10 files changed, 40 insertions(+), 27 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 * K 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 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 */ diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index e7df27083..49ff24863 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -82,11 +82,11 @@ protected: } } - void tryBadInput(const string badInput) { + void tryBadInput(const string badInput, bool strictMode = false) { // cerr << "Testing bad input: '" << badInput << "'\n"; // Debug.on("parser"); Input* input = Input::newStringInput(d_lang, badInput, "test"); - Parser parser(d_exprManager, input); + Parser parser(d_exprManager, input, strictMode); TS_ASSERT_THROWS ( while(parser.nextCommand()); cout << "\nBad input succeeded:\n" << badInput << endl;, @@ -134,10 +134,7 @@ protected: // Debug.on("parser-extra"); // cout << "Testing bad expr: '" << badExpr << "'\n"; Input* input = Input::newStringInput(d_lang, badExpr, "test"); - Parser parser(d_exprManager, input); - if( strictMode ) { - parser.enableStrictMode(); - } + Parser parser(d_exprManager, input, strictMode); setupContext(parser); TS_ASSERT( !parser.done() ); TS_ASSERT_THROWS @@ -278,10 +275,10 @@ public: tryGoodInput(""); // empty string is OK tryGoodInput("(set-logic QF_UF)"); tryGoodInput("(set-info :notes |This is a note, take note!|)"); - tryGoodInput("(set-logic QF_UF)(assert true)"); + tryGoodInput("(set-logic QF_UF) (assert true)"); tryGoodInput("(check-sat)"); tryGoodInput("(exit)"); - tryGoodInput("(assert false) (check-sat)"); + tryGoodInput("(set-logic QF_UF) (assert false) (check-sat)"); tryGoodInput("(set-logic QF_UF) (declare-fun a () Bool) " "(declare-fun b () Bool)"); tryGoodInput("(set-logic QF_UF) (declare-fun a () Bool) " @@ -299,10 +296,13 @@ public: void testBadSmt2Inputs() { tryBadInput("(assert)"); // no args tryBadInput("(set-info :notes |Symbols can't contain the | character|)"); - tryBadInput("(check-sat true)"); // shouldn't have an arg + tryBadInput("(set-logic QF_UF) (check-sat true)"); // shouldn't have an arg tryBadInput("(declare-sort a)"); // no arg tryBadInput("(declare-sort a 0) (declare-sort a 0)"); // double decl - tryBadInput("(declare-fun p Bool)"); // should be "p () Bool" + tryBadInput("(set-logic QF_UF) (declare-fun p Bool)"); // should be "p () Bool" + // strict mode + tryBadInput("(assert true)", true); // no set-logic, core theory symbol "true" undefined + tryBadInput("(declare-fun p Bool)", true); // core theory symbol "Bool" undefined } void testGoodSmt2Exprs() { -- 2.30.2