From 86716e3782aae62a38987f7f89bdf5498eca534a Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Tue, 2 Feb 2010 20:04:18 +0000 Subject: [PATCH] Minor changes to parser --- src/parser/antlr_parser.cpp | 16 ++++++++-------- src/parser/antlr_parser.h | 16 ++++++++++------ src/parser/cvc/cvc_parser.g | 7 ++++--- src/parser/smt/smt_lexer.g | 14 +++++++------- src/parser/smt/smt_parser.g | 22 +++++++++++++--------- test/unit/parser/parser_black.h | 8 ++++---- 6 files changed, 46 insertions(+), 37 deletions(-) diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index e7169a02b..961915523 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -72,19 +72,19 @@ Expr AntlrParser::mkExpr(Kind kind, const std::vector& children) { return d_exprManager->mkExpr(kind, children); } -void AntlrParser::newPredicate(std::string p_name, const std::vector< - std::string>& p_sorts) { - if(p_sorts.size() == 0) { - d_varSymbolTable.bindName(p_name, d_exprManager->mkVar()); +void AntlrParser::newPredicate(std::string name, + const std::vector< std::string>& sorts) { + if(sorts.size() == 0) { + d_varSymbolTable.bindName(name, d_exprManager->mkVar()); } else { Unhandled("Non unary predicate not supported yet!"); } } -void AntlrParser::newPredicates(const std::vector& p_names) { - vector sorts; - for(unsigned i = 0; i < p_names.size(); ++i) { - newPredicate(p_names[i], sorts); +void AntlrParser::newPredicates(const std::vector& names, + const std::vector< std::string>& sorts) { + for(unsigned i = 0; i < names.size(); ++i) { + newPredicate(names[i], sorts); } } diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index f83ccd5f2..5cbb7411e 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -168,17 +168,21 @@ protected: Expr mkExpr(Kind kind, const std::vector& children); /** - * Creates a new predicated over the given sorts. - * @param p_name the name of the predicate - * @param p_sorts the arity sorts + * Creates a new predicate over the given sorts. The predicate + * has arity sorts.size(). + * @param name the name of the predicate + * @param sorts the sorts */ - void newPredicate(std::string p_name, const std::vector& p_sorts); + void newPredicate(std::string name, + const std::vector& sorts); /** - * Creates new predicates of given types. + * Creates new predicates over the given sorts. Each predicate + * will have arity sorts.size(). * @param p_names the names of the predicates */ - void newPredicates(const std::vector& p_names); + void newPredicates(const std::vector& names, + const std::vector& sorts); /** * Returns the precedence rank of the kind. diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 51473312e..cb9c9b160 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -59,8 +59,9 @@ command returns [CVC4::Command* cmd = 0] | 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); + // FIXME: switch on type (may not be predicates) + vector sorts; + newPredicates(ids,sorts); cmd = new DeclarationCommand(ids); } SEMICOLON @@ -239,4 +240,4 @@ boolAtom returns [CVC4::Expr atom] predicateSymbol[DeclarationCheck check = CHECK_NONE] returns [std::string pSymbol] : pSymbol = identifier[check] ; - \ No newline at end of file + diff --git a/src/parser/smt/smt_lexer.g b/src/parser/smt/smt_lexer.g index 0b38e1c2e..a82e54e30 100644 --- a/src/parser/smt/smt_lexer.g +++ b/src/parser/smt/smt_lexer.g @@ -42,13 +42,13 @@ tokens { UNKNOWN = "unknown"; BENCHMARK = "benchmark"; // The SMT attribute tokens - C_LOGIC = ":logic"; - C_ASSUMPTION = ":assumption"; - C_FORMULA = ":formula"; - C_STATUS = ":status"; - C_EXTRASORTS = ":extrasorts"; - C_EXTRAFUNS = ":extrafuns"; - C_EXTRAPREDS = ":extrapreds"; + LOGIC_ATTR = ":logic"; + ASSUMPTION_ATTR = ":assumption"; + FORMULA_ATTR = ":formula"; + STATUS_ATTR = ":status"; + EXTRASORTS_ATTR = ":extrasorts"; + EXTRAFUNS_ATTR = ":extrafuns"; + EXTRAPREDS_ATTR = ":extrapreds"; C_NOTES = ":notes"; } diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index 88216336d..84b38c5cf 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -55,8 +55,8 @@ benchmark returns [Command* cmd] ; /** - * Matchecs sequence of benchmark attributes and returns a pointer to a command - * sequence command. + * Matches a sequence of benchmark attributes and returns a pointer to a + * command sequence. * @return the command sequence */ benchAttributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence()] @@ -77,12 +77,16 @@ benchAttribute returns [Command* smt_command = 0] string logic; SetBenchmarkStatusCommand::BenchmarkStatus b_status = SetBenchmarkStatusCommand::SMT_UNKNOWN; } - : C_LOGIC logic = identifier { smt_command = new SetBenchmarkLogicCommand(logic); } - | 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 (predicateDeclaration)+ RPAREN - | C_NOTES STRING_LITERAL + : LOGIC_ATTR logic = identifier + { smt_command = new SetBenchmarkLogicCommand(logic); } + | ASSUMPTION_ATTR formula = annotatedFormula + { smt_command = new AssertCommand(formula); } + | FORMULA_ATTR formula = annotatedFormula + { smt_command = new CheckSatCommand(formula); } + | STATUS_ATTR b_status = status + { smt_command = new SetBenchmarkStatusCommand(b_status); } + | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN + | NOTES_ATTR STRING_LITERAL | annotation ; @@ -224,4 +228,4 @@ status returns [ SetBenchmarkStatusCommand::BenchmarkStatus status ] annotation : attribute (USER_VALUE)? ; - \ No newline at end of file + diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 8a1f781dc..dbfd13598 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -133,7 +133,7 @@ class SmtParserBlack : public CxxTest::TestSuite { void tryGoodInputs(Parser::InputLanguage d_lang, const string goodInputs[], int numInputs) { for(int i = 0; i < numInputs; ++i) { - cout << "Testing input: '" << goodInputs[i] << "'\n"; + cout << "Testing good input: '" << goodInputs[i] << "'\n"; istringstream stream(goodInputs[i]); Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream); TS_ASSERT( !smtParser->done() ); @@ -149,7 +149,7 @@ class SmtParserBlack : public CxxTest::TestSuite { void tryBadInputs(Parser::InputLanguage d_lang, const string badInputs[], int numInputs) { for(int i = 0; i < numInputs; ++i) { - cout << "Testing input: '" << badInputs[i] << "'\n"; + cout << "Testing bad input: '" << badInputs[i] << "'\n"; istringstream stream(badInputs[i]); Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream); TS_ASSERT_THROWS( while(smtParser->parseNextCommand()); , ParserException ); @@ -161,7 +161,7 @@ class SmtParserBlack : public CxxTest::TestSuite { cout << "Using context: " << context << endl; for(int i = 0; i < numExprs; ++i) { try { - cout << "Testing expr: '" << goodBooleanExprs[i] << "'\n"; + cout << "Testing good expr: '" << goodBooleanExprs[i] << "'\n"; istringstream stream(context + goodBooleanExprs[i]); Parser* parser = Parser::getNewParser(d_exprManager, d_lang, stream); TS_ASSERT( !parser->done() ); @@ -184,7 +184,7 @@ class SmtParserBlack : public CxxTest::TestSuite { void tryBadExprs(Parser::InputLanguage d_lang,const string badBooleanExprs[], int numExprs) { for(int i = 0; i < numExprs; ++i) { - cout << "Testing expr: '" << badBooleanExprs[i] << "'\n"; + cout << "Testing bad expr: '" << badBooleanExprs[i] << "'\n"; istringstream stream(badBooleanExprs[i]); Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream); TS_ASSERT_THROWS( smtParser->parseNextExpression(), ParserException ); -- 2.30.2