From: Dejan Jovanović Date: Fri, 18 Dec 2009 19:57:34 +0000 (+0000) Subject: More fixes X-Git-Tag: cvc5-1.0.0~9349 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=deaeed0271fcaa39c071ced30fb21946ca2e6d0f;p=cvc5.git More fixes --- diff --git a/src/parser/cvc/cvc_lexer.g b/src/parser/cvc/cvc_lexer.g index 47cebbbb0..863b15a95 100644 --- a/src/parser/cvc/cvc_lexer.g +++ b/src/parser/cvc/cvc_lexer.g @@ -70,6 +70,13 @@ COLON options{ paraphrase = "a colon"; } : ':' ; +/** + * Matches the 'l' + */ +SEMICOLON options{ paraphrase = "a semicolon"; } + : ';' + ; + /** * Matches the ',' */ diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index c7f932a0c..a22ce64e7 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -54,15 +54,16 @@ command returns [CVC4::Command* cmd = 0] Expr f; vector ids; } - : ASSERT f = formula { cmd = new AssertCommand(f); } - | QUERY f = formula { cmd = new QueryCommand(f); } - | CHECKSAT f = formula { cmd = new CheckSatCommand(f); } - | CHECKSAT { cmd = new CheckSatCommand(); } + : ASSERT f = formula SEMICOLON { cmd = new AssertCommand(f); } + | QUERY f = formula SEMICOLON { cmd = new QueryCommand(f); } + | CHECKSAT f = formula SEMICOLON { cmd = new CheckSatCommand(f); } + | CHECKSAT SEMICOLON { cmd = new CheckSatCommand(); } | identifierList[ids, CHECK_UNDECLARED] COLON type { // [chris 12/15/2009] FIXME: decls may not be BOOLEAN newPredicates(ids); cmd = new DeclarationCommand(ids); } + SEMICOLON | EOF ; diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index f7045fa7e..56e1f9f17 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -70,7 +70,7 @@ benchAttributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence()] * a corresponding command * @retrurn a command corresponding to the attribute */ -benchAttribute returns [ Command* smt_command = 0] +benchAttribute returns [Command* smt_command = 0] { Expr formula; string logic; @@ -80,7 +80,7 @@ benchAttribute returns [ Command* smt_command = 0] | C_ASSUMPTION formula = annotatedFormula { smt_command = new AssertCommand(formula); } | C_FORMULA formula = annotatedFormula { smt_command = new CheckSatCommand(formula); } | C_STATUS b_status = status { smt_command = new SetBenchmarkStatusCommand(b_status); } - | C_EXTRAPREDS LPAREN (pred_symb_decl)+ RPAREN + | C_EXTRAPREDS LPAREN (predicateDeclaration)+ RPAREN | C_NOTES STRING_LITERAL | annotation ; @@ -120,100 +120,94 @@ annotatedFormula returns [CVC4::Expr formula] /** * Matches an annotated proposition atom, which is either a propositional atom * or built of other atoms using a predicate symbol. + * @return expression representing the atom */ annotatedAtom returns [CVC4::Expr atom] : atom = propositionalAtom ; - - - - - -/** - * Matches an attribute name from the input (:attribute_name). - */ -attribute - : C_IDENTIFIER - ; - /** - * Matches the sort symbol, which can be an arbitrary identifier. - */ -sort_symb returns [std::string s] - : id:IDENTIFIER { s = id->getText(); } - ; - -/** - * Matches an annotation, which is an attribute name, with an optional user value. - */ -annotation - : attribute (USER_VALUE)? +* Matches on of the unary Boolean connectives. +* @return the kind of the Bollean connective +*/ +boolConnective returns [CVC4::Kind kind] + : NOT { kind = CVC4::NOT; } + | IMPLIES { kind = CVC4::IMPLIES; } + | AND { kind = CVC4::AND; } + | OR { kind = CVC4::OR; } + | XOR { kind = CVC4::XOR; } + | IFF { kind = CVC4::IFF; } ; - + /** - * Matches a predicate symbol. - */ -pred_symb returns [std::string p] - : id:IDENTIFIER { p = id->getText(); } + * Mathces a sequence of annotaed formulas and puts them into the formulas + * vector. + * @param formulas the vector to fill with formulas + */ +annotatedFormulas[std::vector& formulas] +{ + Expr f; +} + : ( f = annotatedFormula { formulas.push_back(f); } )+ ; - /** - * Matches a propositional atom. + * Matches a propositional atom and returns the expression of the atom. + * @return atom the expression of the atom */ propositionalAtom returns [CVC4::Expr atom] { std::string p; } - : p = pred_symb {isDeclared(p, SYM_VARIABLE)}? { atom = getVariable(p); } - exception catch [antlr::SemanticException ex] { - rethrow(ex, "Undeclared variable " + p); - } + : p = predicateName[CHECK_DECLARED] { atom = getVariable(p); } | TRUE { atom = getTrueExpr(); } | FALSE { atom = getFalseExpr(); } ; - + /** - * Matches on of the unary Boolean connectives. + * Matches a predicate symbol. + * @param check what kind of check to do with the symbol */ -boolConnective returns [CVC4::Kind kind] - : NOT { kind = CVC4::NOT; } - | IMPLIES { kind = CVC4::IMPLIES; } - | AND { kind = CVC4::AND; } - | OR { kind = CVC4::OR; } - | XOR { kind = CVC4::XOR; } - | IFF { kind = CVC4::IFF; } +predicateName[DeclarationCheck check = CHECK_NONE] returns [std::string p] + : p = identifier[check] ; - -annotatedFormulas[std::vector& formulas] -{ - Expr f; -} - : ( f = annotatedFormula { formulas.push_back(f); } )+ + +/** + * Matches an attribute name from the input (:attribute_name). + */ +attribute + : C_IDENTIFIER + ; + +/** + * Matches the sort symbol, which can be an arbitrary identifier. + * @param check the check to perform on the name + */ +sortName[DeclarationCheck check = CHECK_NONE] returns [std::string s] + : s = identifier[check] ; - + /** - * Matches the declaration of a predicate symbol. + * Matches the declaration of a predicate and declares it */ -pred_symb_decl +predicateDeclaration { string p_name; vector p_sorts; } - : LPAREN p_name = pred_symb sort_symbs[p_sorts] RPAREN { newPredicate(p_name, p_sorts); } + : LPAREN p_name = predicateName[CHECK_UNDECLARED] sortNames[p_sorts] RPAREN { newPredicate(p_name, p_sorts); } ; /** * Matches a sequence of sort symbols and fills them into the given vector. */ -sort_symbs[std::vector& sorts] +sortNames[std::vector& sorts] { - std::string type; + std::string sort; } - : ( type = sort_symb { sorts.push_back(type); })* + : ( sort = sortName[CHECK_UNDECLARED] { sorts.push_back(sort); })* ; - + /** * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'. */ @@ -221,4 +215,12 @@ status returns [ SetBenchmarkStatusCommand::BenchmarkStatus status ] : SAT { status = SetBenchmarkStatusCommand::SMT_SATISFIABLE; } | UNSAT { status = SetBenchmarkStatusCommand::SMT_UNSATISFIABLE; } | UNKNOWN { status = SetBenchmarkStatusCommand::SMT_UNKNOWN; } - ; \ No newline at end of file + ; + +/** + * Matches an annotation, which is an attribute name, with an optional user + */ +annotation + : attribute (USER_VALUE)? + ; + \ No newline at end of file