From 64d530e5b9096e66398f92d93cf7bc4268df0e70 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 3 Feb 2010 22:20:25 +0000 Subject: Addressed many of the concerns of bug 10 (build system code review). Some parts split into other bugs: 19, 20, 21. Addressed concerns of bug 11 (util package code review). Slight parser source file modifications: file comments, #included headers in generated parsers/lexers Added CVC4::Result propagation back through MiniSat->PropEngine->SmtEngine->main(). Silenced MiniSat when verbosity is not requested. --- src/parser/cvc/cvc_lexer.g | 59 ++++++++++++--------- src/parser/cvc/cvc_parser.g | 122 ++++++++++++++++++++++++-------------------- 2 files changed, 104 insertions(+), 77 deletions(-) (limited to 'src/parser/cvc') diff --git a/src/parser/cvc/cvc_lexer.g b/src/parser/cvc/cvc_lexer.g index 52c58a38f..db40be3a8 100644 --- a/src/parser/cvc/cvc_lexer.g +++ b/src/parser/cvc/cvc_lexer.g @@ -1,12 +1,26 @@ +/* cvc_lexer.g + * Original author: dejan + * Major contributors: + * Minor contributors (to current version): none + * This file is part of the CVC4 prototype. + * Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + * Courant Institute of Mathematical Sciences + * New York University + * See the file COPYING in the top-level source directory for licensing + * information. + * + * Lexer for CVC presentation language. + */ + options { language = "Cpp"; // C++ output for antlr namespaceStd = "std"; // Cosmetic option to get rid of long defines in generated code namespaceAntlr = "antlr"; // Cosmetic option to get rid of long defines in generated code namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace } - + /** - * AntlrCvcLexer class is a stream tokenizer (lexer) for the CVC language. + * AntlrCvcLexer class is a stream tokenizer (lexer) for the CVC language. */ class AntlrCvcLexer extends Lexer; @@ -14,15 +28,15 @@ options { exportVocab = CvcVocabulary; // Name of the shared token vocabulary testLiterals = false; // Do not check for literals by default defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions - k = 2; + k = 2; } - + /* * The tokens that might match with the identifiers go here. Otherwise define * them below. */ tokens { - // Types + // Types BOOLEAN = "BOOLEAN"; // Boolean oparators AND = "AND"; @@ -42,7 +56,7 @@ tokens { CHECKSAT = "CHECKSAT"; PRINT = "PRINT"; ECHO = "ECHO"; - + PUSH = "PUSH"; POP = "POP"; POPTO = "POPTO"; @@ -56,56 +70,56 @@ IFF : "<=>"; /** * Matches any letter ('a'-'z' and 'A'-'Z'). */ -protected -ALPHA options { paraphrase = "a letter"; } - : 'a'..'z' +protected +ALPHA options { paraphrase = "a letter"; } + : 'a'..'z' | 'A'..'Z' ; - + /** * Matches the digits (0-9) */ -protected -DIGIT options { paraphrase = "a digit"; } +protected +DIGIT options { paraphrase = "a digit"; } : '0'..'9' ; /** * Matches the ':' */ -COLON options { paraphrase = "a colon"; } +COLON options { paraphrase = "a colon"; } : ':' ; /** * Matches the 'l' */ -SEMICOLON options { paraphrase = "a semicolon"; } +SEMICOLON options { paraphrase = "a semicolon"; } : ';' ; /** * Matches an identifier from the input. An identifier is a sequence of letters, - * digits and "_", "'", "." symbols, starting with a letter. + * digits and "_", "'", "." symbols, starting with a letter. */ IDENTIFIER options { paraphrase = "an identifier"; testLiterals = true; } : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')* ; - + /** * Matches the left bracket ('('). */ -LPAREN options { paraphrase = "a left parenthesis '('"; } +LPAREN options { paraphrase = "a left parenthesis '('"; } : '('; - + /** * Matches the right bracket ('('). */ -RPAREN options { paraphrase = "a right parenthesis ')'"; } +RPAREN options { paraphrase = "a right parenthesis ')'"; } : ')'; /** - * Matches and skips whitespace in the input and ignores it. + * Matches and skips whitespace in the input and ignores it. */ WHITESPACE options { paraphrase = "whitespace"; } : (' ' | '\t' | '\f') { $setType(antlr::Token::SKIP); } @@ -114,7 +128,7 @@ WHITESPACE options { paraphrase = "whitespace"; } /** * Matches and skips the newline symbols in the input. */ -NEWLINE options { paraphrase = "a newline"; } +NEWLINE options { paraphrase = "a newline"; } : ('\r' '\n' | '\r' | '\n') { $setType(antlr::Token::SKIP); newline(); } ; @@ -124,11 +138,10 @@ NEWLINE options { paraphrase = "a newline"; } COMMENT options { paraphrase = "comment"; } : '%' (~('\n' | '\r'))* { $setType(antlr::Token::SKIP); } ; - + /** * Matches a numeral from the input (non-empty sequence of digits). */ NUMERAL options { paraphrase = "a numeral"; } : (DIGIT)+ ; - \ No newline at end of file diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index eb21283a3..ce61deae2 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -1,24 +1,39 @@ +/* cvc_parser.g + * Original author: dejan + * Major contributors: + * Minor contributors (to current version): none + * This file is part of the CVC4 prototype. + * Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + * Courant Institute of Mathematical Sciences + * New York University + * See the file COPYING in the top-level source directory for licensing + * information. + * + * Parser for CVC presentation language. + */ + header "post_include_hpp" { #include "parser/antlr_parser.h" +#include "util/command.h" } header "post_include_cpp" { -#include +#include using namespace std; using namespace CVC4; using namespace CVC4::parser; } - + options { language = "Cpp"; // C++ output for antlr namespaceStd = "std"; // Cosmetic option to get rid of long defines in generated code namespaceAntlr = "antlr"; // Cosmetic option to get rid of long defines in generated code namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace } - + /** - * AntlrCvcParser class is the parser for the files in CVC format. + * AntlrCvcParser class is the parser for the files in CVC format. */ class AntlrCvcParser extends Parser("AntlrParser"); options { @@ -27,7 +42,7 @@ options { defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions k = 2; } - + /** * Parses the next command. * @return command or 0 if EOF @@ -44,9 +59,9 @@ parseExpr returns [CVC4::Expr expr] : expr = formula | EOF ; - + /** - * Matches a command of the input. If a declaration, it will return an empty + * Matches a command of the input. If a declaration, it will return an empty * command. */ command returns [CVC4::Command* cmd = 0] @@ -58,36 +73,36 @@ command returns [CVC4::Command* cmd = 0] | 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 { + | identifierList[ids, CHECK_UNDECLARED] COLON type { // FIXME: switch on type (may not be predicates) vector sorts; - newPredicates(ids,sorts); - cmd = new DeclarationCommand(ids); + newPredicates(ids,sorts); + cmd = new DeclarationCommand(ids); } SEMICOLON - | EOF + | EOF ; /** - * Mathches a list of identifiers separated by a comma and puts them in the + * Mathches a list of identifiers separated by a comma and puts them in the * given list. * @param idList the list to fill with identifiers. - * @param check what kinds of check to perform on the symbols + * @param check what kinds of check to perform on the symbols */ identifierList[std::vector& idList, DeclarationCheck check = CHECK_NONE] { string id; } - : id = identifier[check] { idList.push_back(id); } + : id = identifier[check] { idList.push_back(id); } (COMMA id = identifier[check] { idList.push_back(id); })* ; - + /** * Matches an identifier and returns a string. */ identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id] - : x:IDENTIFIER + : x:IDENTIFIER { id = x->getText(); } { checkDeclaration(id, check) }? exception catch [antlr::SemanticException& ex] { @@ -95,11 +110,11 @@ identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id] case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared"); case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared"); default: throw ex; - } - } + } + } ; - -/** + +/** * Matches a type. * TODO: parse more types */ @@ -107,10 +122,10 @@ type : BOOLEAN ; -/** +/** * Matches a CVC4 formula. * @return the expression representing the formula - */ + */ formula returns [CVC4::Expr formula] : formula = boolFormula ; @@ -121,69 +136,69 @@ formula returns [CVC4::Expr formula] * createPrecedenceExpr method to build the expression using the precedence * and associativity of the operators. * @return the expression representing the formula - */ + */ boolFormula returns [CVC4::Expr formula] - : formula = boolAndFormula + : formula = boolAndFormula ; /** - * Matches a Boolean AND formula of a given kind by doing a recursive descent. + * Matches a Boolean AND formula of a given kind by doing a recursive descent. */ boolAndFormula returns [CVC4::Expr andFormula] { Expr e; vector exprs; } - : e = boolXorFormula { exprs.push_back(e); } + : e = boolXorFormula { exprs.push_back(e); } ( AND e = boolXorFormula { exprs.push_back(e); } )* - { - andFormula = (exprs.size() > 1 ? mkExpr(CVC4::AND, exprs) : exprs[0]); - } + { + andFormula = (exprs.size() > 1 ? mkExpr(CVC4::AND, exprs) : exprs[0]); + } ; /** - * Matches a Boolean XOR formula of a given kind by doing a recursive descent. + * 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); } + : e = boolOrFormula { exprs.push_back(e); } ( XOR e = boolOrFormula { exprs.push_back(e); } )* - { - xorFormula = (exprs.size() > 1 ? mkExpr(CVC4::XOR, exprs) : exprs[0]); - } + { + xorFormula = (exprs.size() > 1 ? mkExpr(CVC4::XOR, exprs) : exprs[0]); + } ; /** - * Matches a Boolean OR formula of a given kind by doing a recursive descent. + * Matches a Boolean OR formula of a given kind by doing a recursive descent. */ boolOrFormula returns [CVC4::Expr orFormula] { Expr e; vector exprs; } - : e = boolImpliesFormula { exprs.push_back(e); } + : e = boolImpliesFormula { exprs.push_back(e); } ( OR e = boolImpliesFormula { exprs.push_back(e); } )* - { - orFormula = (exprs.size() > 1 ? mkExpr(CVC4::OR, exprs) : exprs[0]); - } + { + orFormula = (exprs.size() > 1 ? mkExpr(CVC4::OR, exprs) : exprs[0]); + } ; /** - * Matches a Boolean IMPLIES formula of a given kind by doing a recursive descent. + * 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); } + : e = boolIffFormula { exprs.push_back(e); } + ( IMPLIES e = boolIffFormula { exprs.push_back(e); } )* { - impliesFormula = exprs.back(); + impliesFormula = exprs.back(); for (int i = exprs.size() - 2; i >= 0; -- i) { impliesFormula = mkExpr(CVC4::IMPLIES, exprs[i], impliesFormula); } @@ -191,21 +206,21 @@ boolImpliesFormula returns [CVC4::Expr impliesFormula] ; /** - * Matches a Boolean IFF formula of a given kind by doing a recursive descent. + * 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); } + : iffFormula = primaryBoolFormula + ( IFF e = primaryBoolFormula + { iffFormula = mkExpr(CVC4::IFF, iffFormula, e); } )* ; - + /** - * Parses a primary Boolean formula. A primary Boolean formula is either a - * Boolean atom (variables and predicates) a negation of a primary Boolean + * Parses a primary Boolean formula. A primary Boolean formula is either a + * Boolean atom (variables and predicates) a negation of a primary Boolean * formula or a formula enclosed in parenthesis. * @return the expression representing the formula */ @@ -247,7 +262,7 @@ iteElseFormula returns [CVC4::Expr formula] /** * Parses the Boolean atoms (variables and predicates). * @return the expression representing the atom. - */ + */ boolAtom returns [CVC4::Expr atom] { string p; @@ -259,13 +274,12 @@ boolAtom returns [CVC4::Expr atom] | TRUE { atom = getTrueExpr(); } | FALSE { atom = getFalseExpr(); } ; - + /** * Parses a predicate symbol (an identifier). - * @param what kind of check to perform on the id + * @param what kind of check to perform on the id * @return the predicate symol */ predicateSymbol[DeclarationCheck check = CHECK_NONE] returns [std::string pSymbol] : pSymbol = identifier[check] ; - -- cgit v1.2.3