diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-03 22:20:25 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-03 22:20:25 +0000 |
commit | 64d530e5b9096e66398f92d93cf7bc4268df0e70 (patch) | |
tree | 189d63541053faca0c778b0c92d84db8d2b1e0ff /src/parser | |
parent | 842fd54de1da122f4c7274796550c2fe21c11db2 (diff) |
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.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/Makefile.am | 6 | ||||
-rw-r--r-- | src/parser/antlr_parser.cpp | 1 | ||||
-rw-r--r-- | src/parser/antlr_parser.h | 4 | ||||
-rw-r--r-- | src/parser/cvc/cvc_lexer.g | 59 | ||||
-rw-r--r-- | src/parser/cvc/cvc_parser.g | 122 | ||||
-rw-r--r-- | src/parser/parser.h | 4 | ||||
-rw-r--r-- | src/parser/smt/smt_lexer.g | 86 | ||||
-rw-r--r-- | src/parser/smt/smt_parser.g | 127 |
8 files changed, 234 insertions, 175 deletions
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 4fcaed14d..fe906cbe0 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -10,9 +10,6 @@ # set to zero if interfaces have been removed # or changed # -# LIBCVC4PARSER_RELEASE (-release) should match the CVC4 release version -# -LIBCVC4PARSER_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@ LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@ AM_CPPFLAGS = \ @@ -25,7 +22,8 @@ SUBDIRS = smt cvc nobase_lib_LTLIBRARIES = libcvc4parser.la noinst_LTLIBRARIES = libcvc4parser_noinst.la -libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) +libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) \ + -version-info $(LIBCVC4PARSER_VERSION) libcvc4parser_la_LIBADD = libcvc4parser_noinst.la libcvc4parser_la_LINK = $(CXXLINK) diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 3522bfd75..34bf4bc82 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -25,6 +25,7 @@ #include "antlr_parser.h" #include "util/output.h" #include "util/Assert.h" +#include "util/command.h" using namespace std; using namespace CVC4; diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index ae84318c8..a3015eb22 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -25,11 +25,13 @@ #include "expr/expr.h" #include "expr/expr_manager.h" -#include "util/command.h" #include "util/Assert.h" #include "parser/symbol_table.h" namespace CVC4 { + +class Command; + namespace parser { /** 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 <vector> +#include <vector> 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<string> 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<std::string>& 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<Expr> 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<Expr> 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<Expr> 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<Expr> 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] ; - diff --git a/src/parser/parser.h b/src/parser/parser.h index 618b1c8ab..4f0502f24 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -18,10 +18,10 @@ #include <string> #include <iostream> + #include "cvc4_config.h" #include "parser/parser_exception.h" #include "util/Assert.h" -#include "antlr_parser.h" namespace antlr { class CharScanner; @@ -36,6 +36,8 @@ class ExprManager; namespace parser { +class AntlrParser; + /** * The parser. The parser should be obtained by calling the static methods * getNewParser, and should be deleted when done. diff --git a/src/parser/smt/smt_lexer.g b/src/parser/smt/smt_lexer.g index a82e54e30..e9abab61a 100644 --- a/src/parser/smt/smt_lexer.g +++ b/src/parser/smt/smt_lexer.g @@ -1,13 +1,27 @@ +/* smt_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 SMT-LIB input 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 } - + /** - * AntlrSmtLexer class is a stream tokenizer (lexer) for the SMT-LIB benchmark - * language. + * AntlrSmtLexer class is a stream tokenizer (lexer) for the SMT-LIB benchmark + * language. */ class AntlrSmtLexer extends Lexer; @@ -15,9 +29,9 @@ options { exportVocab = SmtVocabulary; // Name of the shared token vocabulary testLiterals = false; // Do not check for literals by default defaultErrorHandler = false; // Skip the default error handling, just break with exceptions - k = 2; + k = 2; } - + tokens { // Base SMT-LIB tokens DISTINCT = "distinct"; @@ -55,28 +69,28 @@ tokens { /** * 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 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 an identifier starting with a colon. An identifier is a sequence of letters, * digits and "_", "'", "." symbols, starting with a colon. @@ -84,47 +98,47 @@ IDENTIFIER options { paraphrase = "an identifier"; testLiterals = true; } C_IDENTIFIER options { paraphrase = "an identifier starting with a colon"; testLiterals = true; } : ':' ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')* ; - + /** * Matches the value of user-defined annotations or attributes. The only constraint imposed on a user-defined value is that it start with * an open brace and end with closed brace. */ USER_VALUE - : '{' + : '{' ( '\n' { newline(); } - | ~('{' | '}' | '\n') - )* + | ~('{' | '}' | '\n') + )* '}' ; - + /** - * Matches the question mark symbol ('?'). + * Matches the question mark symbol ('?'). */ -QUESTION_MARK options { paraphrase = "a question mark '?'"; } +QUESTION_MARK options { paraphrase = "a question mark '?'"; } : '?' ; - + /** * Matches the dollar sign ('$'). */ -DOLLAR_SIGN options { paraphrase = "a dollar sign '$'"; } +DOLLAR_SIGN options { paraphrase = "a dollar sign '$'"; } : '$' ; - + /** * 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. + * Matches and skips whitespace in the input. */ WHITESPACE options { paraphrase = "whitespace"; } : (' ' | '\t' | '\f') { $setType(antlr::Token::SKIP); } @@ -133,32 +147,32 @@ 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(); } ; - + /** * Matches a numeral from the input (non-empty sequence of digits). */ NUMERAL options { paraphrase = "a numeral"; } : (DIGIT)+ ; - + /** * Matches an allowed escaped character. - */ + */ protected ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r') - ; - + ; + /** * Matches a double quoted string literal. Escaping is supported, and escape - * character '\' has to be escaped. + * character '\' has to be escaped. */ -STRING_LITERAL options { paraphrase = "a string literal"; } +STRING_LITERAL options { paraphrase = "a string literal"; } : '"' (ESCAPE | ~('"'|'\\'))* '"' ; - + /** * Matches the comments and ignores them */ diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index 0db89d4f1..3933a04f0 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -1,24 +1,39 @@ +/* smt_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 SMT-LIB input language. + */ + header "post_include_hpp" { #include "parser/antlr_parser.h" +#include "util/command.h" } header "post_include_cpp" { -#include <vector> +#include <vector> 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 } - + /** - * AntlrSmtParser class is the parser for the SMT-LIB files. + * AntlrSmtParser class is the parser for the SMT-LIB files. */ class AntlrSmtParser extends Parser("AntlrParser"); options { @@ -43,50 +58,50 @@ parseExpr returns [CVC4::Expr expr] */ parseCommand returns [CVC4::Command* cmd] : cmd = benchmark - ; - + ; + /** * Matches the whole SMT-LIB benchmark. * @return the sequence command containing the whole problem - */ + */ benchmark returns [Command* cmd] : LPAREN BENCHMARK IDENTIFIER cmd = benchAttributes RPAREN - | EOF { cmd = 0; } + | EOF { cmd = 0; } ; /** - * Matches a sequence of benchmark attributes and returns a pointer to a + * Matches a sequence of benchmark attributes and returns a pointer to a * command sequence. - * @return the command sequence + * @return the command sequence */ benchAttributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence()] { Command* cmd; } - : (cmd = benchAttribute { if (cmd) cmd_seq->addCommand(cmd); } )+ + : (cmd = benchAttribute { if (cmd) cmd_seq->addCommand(cmd); } )+ ; - + /** - * Matches a benchmark attribute, sucha as ':logic', ':formula', and returns + * Matches a benchmark attribute, sucha as ':logic', ':formula', and returns * a corresponding command * @retrurn a command corresponding to the attribute */ benchAttribute returns [Command* smt_command = 0] { - Expr formula; - string logic; + Expr formula; + string logic; SetBenchmarkStatusCommand::BenchmarkStatus b_status = SetBenchmarkStatusCommand::SMT_UNKNOWN; } - : LOGIC_ATTR logic = identifier - { smt_command = new SetBenchmarkLogicCommand(logic); } - | ASSUMPTION_ATTR formula = annotatedFormula - { smt_command = new AssertCommand(formula); } - | FORMULA_ATTR formula = annotatedFormula + : 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 + | STATUS_ATTR b_status = status + { smt_command = new SetBenchmarkStatusCommand(b_status); } + | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN + | NOTES_ATTR STRING_LITERAL | annotation ; @@ -96,38 +111,38 @@ benchAttribute returns [Command* smt_command = 0] * @return the id string */ identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id] - : x:IDENTIFIER + : x:IDENTIFIER { id = x->getText(); } - { checkDeclaration(id, check) }? + { checkDeclaration(id, check) }? exception catch [antlr::SemanticException& ex] { switch (check) { case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared"); case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared"); default: throw ex; - } - } + } + } ; -/** +/** * Matches an annotated formula. - * @return the expression representing the formula + * @return the expression representing the formula */ -annotatedFormula returns [CVC4::Expr formula] -{ - Kind kind; +annotatedFormula returns [CVC4::Expr formula] +{ + Kind kind; vector<Expr> children; } - : formula = annotatedAtom - | LPAREN kind = boolConnective annotatedFormulas[children] RPAREN { formula = mkExpr(kind, children); } + : formula = annotatedAtom + | LPAREN kind = boolConnective annotatedFormulas[children] RPAREN { formula = mkExpr(kind, children); } ; /** - * Matches an annotated proposition atom, which is either a propositional atom - * or built of other atoms using a predicate symbol. + * 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 +annotatedAtom returns [CVC4::Expr atom] + : atom = propositionalAtom ; /** @@ -135,7 +150,7 @@ annotatedAtom returns [CVC4::Expr atom] * @return the kind of the Bollean connective */ boolConnective returns [CVC4::Kind kind] - : NOT { kind = CVC4::NOT; } + : NOT { kind = CVC4::NOT; } | IMPLIES { kind = CVC4::IMPLIES; } | AND { kind = CVC4::AND; } | OR { kind = CVC4::OR; } @@ -147,7 +162,7 @@ boolConnective returns [CVC4::Kind kind] * Mathces a sequence of annotaed formulas and puts them into the formulas * vector. * @param formulas the vector to fill with formulas - */ + */ annotatedFormulas[std::vector<Expr>& formulas] { Expr f; @@ -157,40 +172,40 @@ annotatedFormulas[std::vector<Expr>& formulas] /** * Matches a propositional atom and returns the expression of the atom. - * @return atom the expression of the atom + * @return atom the expression of the atom */ propositionalAtom returns [CVC4::Expr atom] { std::string p; -} +} : p = predicateName[CHECK_DECLARED] { atom = getVariable(p); } | TRUE { atom = getTrueExpr(); } | FALSE { atom = getFalseExpr(); } ; /** - * Matches a predicate symbol. + * Matches a predicate symbol. * @param check what kind of check to do with the symbol */ predicateName[DeclarationCheck check = CHECK_NONE] returns [std::string p] : p = identifier[check] ; - + /** * Matches an attribute name from the input (:attribute_name). - */ -attribute + */ +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] +sortName[DeclarationCheck check = CHECK_NONE] returns [std::string s] : s = identifier[check] ; - + /** * Matches the declaration of a predicate and declares it */ @@ -199,9 +214,9 @@ predicateDeclaration string p_name; vector<string> p_sorts; } - : LPAREN p_name = predicateName[CHECK_UNDECLARED] sortNames[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. */ @@ -209,7 +224,7 @@ sortNames[std::vector<std::string>& sorts] { std::string sort; } - : ( sort = sortName[CHECK_UNDECLARED] { sorts.push_back(sort); })* + : ( sort = sortName[CHECK_UNDECLARED] { sorts.push_back(sort); })* ; /** @@ -222,9 +237,9 @@ status returns [ SetBenchmarkStatusCommand::BenchmarkStatus status ] ; /** - * Matches an annotation, which is an attribute name, with an optional user + * Matches an annotation, which is an attribute name, with an optional user */ -annotation +annotation : attribute (USER_VALUE)? ; - + |