From: Dejan Jovanović Date: Mon, 1 Feb 2010 21:58:47 +0000 (+0000) Subject: Fixing the CVC grammar for parsing Boolean expressions. All the associativity stufff... X-Git-Tag: cvc5-1.0.0~9319 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=595eb7e203d27a9b24a2b71808bc79dab76fa7ba;p=cvc5.git Fixing the CVC grammar for parsing Boolean expressions. All the associativity stufff is now in the grammar. All the parser tests pass now. --- diff --git a/src/context/context.h b/src/context/context.h index 114c8ed69..3bac70cb6 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -51,7 +51,7 @@ class ContextNotifyObj; class Context { /** - * Pointer to the ContextMemoryManager fot this Context. + * Pointer to the ContextMemoryManager for this Context. */ ContextMemoryManager* d_pCMM; @@ -67,13 +67,13 @@ class Context { /** * Doubly-linked list of objects to notify before every pop. See - * ContextNotifyObj for sturcture of linked list. + * ContextNotifyObj for structure of linked list. */ ContextNotifyObj* d_pCNOpre; /** * Doubly-linked list of objects to notify after every pop. See - * ContextNotifyObj for sturcture of linked list. + * ContextNotifyObj for structure of linked list. */ ContextNotifyObj* d_pCNOpost; @@ -189,7 +189,7 @@ public: { if (pScopePrev != NULL) d_level = pScopePrev->getLevel() + 1; } /** - * Destructor: Restore all of the objects in CotextObjList. Defined inline + * Destructor: Restore all of the objects in ContextObjList. Defined inline * below. */ ~Scope(); diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index b7361eb0f..e7169a02b 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -33,25 +33,6 @@ using namespace CVC4::parser; namespace CVC4 { namespace parser { -unsigned AntlrParser::getPrecedence(Kind kind) { - switch(kind) { - // Boolean operators - case IFF: - return 1; - case IMPLIES: - return 2; - case OR: - return 3; - case XOR: - return 4; - case AND: - return 5; - default: - Unhandled("Undefined precedence - necessary for proper parsing of CVC files!"); - } - return 0; -} - AntlrParser::AntlrParser(const antlr::ParserSharedInputState& state, int k) : antlr::LLkParser(state, k) { } @@ -127,64 +108,6 @@ void AntlrParser::rethrow(antlr::SemanticException& e, string new_message) LT(0).get()->getColumn()); } -Expr AntlrParser::createPrecedenceExpr(const vector& exprs, const vector< - Kind>& kinds) { - Assert( exprs.size() > 0, "Expected non-empty vector expr"); - Assert( kinds.size() + 1 == exprs.size(), "Expected kinds to match exprs"); - return createPrecedenceExpr(exprs, kinds, 0, exprs.size() - 1); -} - - /* Find the index of the kind with the lowest precedence. */ -unsigned AntlrParser::findPivot(const std::vector& kinds, - unsigned start_index, unsigned end_index) const { - Assert( start_index >= 0, "Expected start_index >= 0. "); - Assert( end_index < kinds.size(), "Expected end_index < kinds.size(). "); - Assert( start_index <= end_index, "Expected start_index <= end_index. "); - - int pivot = start_index; - unsigned pivot_precedence = getPrecedence(kinds[pivot]); - - for(unsigned i = start_index + 1; i <= end_index; ++i) { - unsigned current_precedence = getPrecedence(kinds[i]); - if(current_precedence < pivot_precedence) { - pivot = i; - pivot_precedence = current_precedence; - } - } - - return pivot; -} - - /* "Tree-ify" an unparenthesized expression: - e_1 op_1 e_2 op_2 ... e_(n-1) op_(n-1) e_n - represented as a vector of exprs and - kinds . - - This works by finding the lowest precedence operator op_i, - then recursively tree-ifying lhs = (e1 op_1 ... op_(i-1) e_i), - rhs = (e_(i+1) op_(i+1) ... op_(n-1) e_N), and forming the - expression (lhs op_i rhs). - */ -Expr AntlrParser::createPrecedenceExpr(const std::vector& exprs, - const std::vector& kinds, - unsigned start_index, unsigned end_index) { - Assert( exprs.size() > 0, "Expected non-empty vector expr"); - Assert( kinds.size() + 1 == exprs.size(), "Expected kinds to match exprs."); - Assert( start_index >= 0, "Expected start_index >= 0. "); - Assert( end_index < exprs.size(), "Expected end_index < exprs.size. "); - Assert( start_index <= end_index, "Expected start_index <= end_index. "); - - if(start_index == end_index) { - return exprs[start_index]; - } - - unsigned pivot = findPivot(kinds, start_index, end_index - 1); - - Expr child_1 = createPrecedenceExpr(exprs, kinds, start_index, pivot); - Expr child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index); - return d_exprManager->mkExpr(kinds[pivot], child_1, child_2); -} - bool AntlrParser::checkDeclation(string varName, DeclarationCheck check) { switch(check) { case CHECK_DECLARED: diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index 271171281..f83ccd5f2 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -167,15 +167,6 @@ protected: */ Expr mkExpr(Kind kind, const std::vector& children); - /** - * Creates a new expression based on the given string of expressions and kinds, - * where kinds[i] is the operator to place between exprs[i] and exprs[i+1]. - * The expression is created so that it respects the kinds precedence table. - * The exprs vector should be non-empty. If the length of exprs is N, then the - * length of kinds should be N-1 (kinds may be empty). - */ - Expr createPrecedenceExpr(const std::vector& exprs, const std::vector& kinds); - /** * Creates a new predicated over the given sorts. * @param p_name the name of the predicate @@ -196,18 +187,6 @@ protected: private: - - unsigned findPivot(const std::vector& kinds, unsigned start_index, unsigned end_index) const; - - /** - * Creates a new expression based on the given string of expressions and kinds - * The expression is created so that it respects the kinds precedence table. - * The exprs vector should be non-empty. The kinds vector should have one less - * element than the exprs vector. start_index and end_index should be valid - * indices into exprs. - */ - Expr createPrecedenceExpr(const std::vector& exprs, const std::vector& kinds, unsigned start_index, unsigned end_index); - /** The expression manager */ ExprManager* d_exprManager; diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 91864329e..51473312e 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -122,20 +122,86 @@ formula returns [CVC4::Expr formula] * and associativity of the operators. * @return the expression representing the formula */ -boolFormula returns [CVC4::Expr formula] +boolFormula returns [CVC4::Expr formula] + : formula = boolAndFormula + ; + +/** + * Matches a Boolean AND formula of a given kind by doing a recursive descent. + */ +boolAndFormula returns [CVC4::Expr andFormula] { - vector formulas; - vector kinds; - Expr f; - Kind k; + Expr e; + vector exprs; +} + : e = boolXorFormula { exprs.push_back(e); } + ( AND e = boolXorFormula { exprs.push_back(e); } )* + { + andFormula = (exprs.size() > 1 ? mkExpr(CVC4::AND, exprs) : exprs[0]); + } + ; + +/** + * Matches a Boolean XOR formula of a given kind by doing a recursive descent. + */ +boolXorFormula returns [CVC4::Expr xorFormula] +{ + Expr e; + vector exprs; +} + : e = boolOrFormula { exprs.push_back(e); } + ( XOR e = boolOrFormula { exprs.push_back(e); } )* + { + xorFormula = (exprs.size() > 1 ? mkExpr(CVC4::XOR, exprs) : exprs[0]); + } + ; + +/** + * Matches a Boolean OR formula of a given kind by doing a recursive descent. + */ +boolOrFormula returns [CVC4::Expr orFormula] +{ + Expr e; + vector exprs; } - : f = primaryBoolFormula { formulas.push_back(f); } - ( k = boolOperator { kinds.push_back(k); } f = primaryBoolFormula { formulas.push_back(f); } )* + : e = boolImpliesFormula { exprs.push_back(e); } + ( OR e = boolImpliesFormula { exprs.push_back(e); } )* { - // Create the expression based on precedences - formula = createPrecedenceExpr(formulas, kinds); + orFormula = (exprs.size() > 1 ? mkExpr(CVC4::OR, exprs) : exprs[0]); + } + ; + +/** + * Matches a Boolean IMPLIES formula of a given kind by doing a recursive descent. + */ +boolImpliesFormula returns [CVC4::Expr impliesFormula] +{ + vector exprs; + Expr e; +} + : e = boolIffFormula { exprs.push_back(e); } + ( IMPLIES e = boolIffFormula { exprs.push_back(e); } + )* + { + impliesFormula = exprs.back(); + for (int i = exprs.size() - 2; i >= 0; -- i) { + impliesFormula = mkExpr(CVC4::IMPLIES, exprs[i], impliesFormula); + } } ; + +/** + * Matches a Boolean IFF formula of a given kind by doing a recursive descent. + */ +boolIffFormula returns [CVC4::Expr iffFormula] +{ + Expr e; +} + : iffFormula = primaryBoolFormula + ( IFF e = primaryBoolFormula + { iffFormula = mkExpr(CVC4::IFF, iffFormula, e); } + )* + ; /** * Parses a primary Boolean formula. A primary Boolean formula is either a @@ -149,19 +215,6 @@ primaryBoolFormula returns [CVC4::Expr formula] | LPAREN formula = boolFormula RPAREN ; -/** - * Parses the Boolean operators and returns the corresponding CVC4 expression - * kind. - * @param the kind of the Boolean operator - */ -boolOperator returns [CVC4::Kind kind] - : IMPLIES { kind = CVC4::IMPLIES; } - | AND { kind = CVC4::AND; } - | OR { kind = CVC4::OR; } - | XOR { kind = CVC4::XOR; } - | IFF { kind = CVC4::IFF; } - ; - /** * Parses the Boolean atoms (variables and predicates). * @return the expression representing the atom. diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 96fe5f6a5..a38868d3b 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -79,7 +79,7 @@ Parser::~Parser() { } Parser::Parser(istream* input, AntlrParser* antlrParser, CharScanner* antlrLexer, bool deleteInput) : - d_done(false), d_input(input), d_antlrParser(antlrParser), d_antlrLexer(antlrLexer), d_deleteInput(deleteInput) { + d_done(false), d_antlrParser(antlrParser), d_antlrLexer(antlrLexer), d_input(input), d_deleteInput(deleteInput) { } Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang, diff --git a/src/parser/parser.h b/src/parser/parser.h index b099a8142..618b1c8ab 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -117,7 +117,8 @@ private: std::istream* d_input; /** Wherther to de-allocate the input */ - bool d_deleteInput;}; // end of class Parser + bool d_deleteInput; +}; // end of class Parser }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index 56e1f9f17..88216336d 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -34,6 +34,7 @@ options { */ parseExpr returns [CVC4::Expr expr] : expr = annotatedFormula + | EOF ; /** diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 6db3b770b..8a1f781dc 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -99,7 +99,7 @@ const string smtExprContext = "(benchmark foo :extrapreds ((a) (b) (c)) )"; const string goodSmtExprs[] = { "(and a b)", "(or (and a b) c)", - "(implies (and (implies a b) a) b))", + "(implies (and (implies a b) a) b)", "(and (iff a b) (not a))", "(iff (xor a b) (and (or a b) (not (and a b))))" };