From 7ae25006aa380df63469f593b523ddf6dd0d2e53 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Fri, 4 Dec 2009 04:06:54 +0000 Subject: [PATCH] Adding support for ANTLR checking in autogen.sh (config/antlr.m4). Commiting antlr SMT grammar that should compile, but is not yet integrated. Tests of compilation and antlr crashes appreciated. --- .settings/org.eclipse.cdt.core.prefs | 22 ++-- config/antlr.m4 | 96 ++++++++++++++ src/parser/Makefile.am | 10 +- src/parser/antlr_parser.cpp | 75 +++++++++++ src/parser/antlr_parser.h | 151 ++++++++++++++++++++++ src/parser/smt/Makefile.am | 19 +++ src/parser/smt/SmtLexer.g | 152 ++++++++++++++++++++++ src/parser/smt/SmtParser.g | 181 +++++++++++++++++++++++++++ 8 files changed, 693 insertions(+), 13 deletions(-) create mode 100644 config/antlr.m4 create mode 100644 src/parser/antlr_parser.cpp create mode 100644 src/parser/antlr_parser.h create mode 100644 src/parser/smt/Makefile.am create mode 100644 src/parser/smt/SmtLexer.g create mode 100644 src/parser/smt/SmtParser.g diff --git a/.settings/org.eclipse.cdt.core.prefs b/.settings/org.eclipse.cdt.core.prefs index 2fc418c48..acec742e4 100644 --- a/.settings/org.eclipse.cdt.core.prefs +++ b/.settings/org.eclipse.cdt.core.prefs @@ -1,4 +1,4 @@ -#Thu Dec 03 15:21:51 EST 2009 +#Thu Dec 03 16:22:24 EST 2009 eclipse.preferences.version=1 org.eclipse.cdt.core.formatter.alignment_for_arguments_in_method_invocation=16 org.eclipse.cdt.core.formatter.alignment_for_base_clause_in_type_declaration=80 @@ -66,15 +66,15 @@ org.eclipse.cdt.core.formatter.insert_space_after_opening_angle_bracket_in_templ org.eclipse.cdt.core.formatter.insert_space_after_opening_brace_in_array_initializer=insert org.eclipse.cdt.core.formatter.insert_space_after_opening_bracket=do not insert org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_cast=do not insert -org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_catch=insert +org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_catch=do not insert org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_exception_specification=do not insert -org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_for=insert -org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_if=insert +org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_for=do not insert +org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_if=do not insert org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_method_declaration=do not insert org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_method_invocation=do not insert org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_parenthesized_expression=do not insert -org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_switch=insert -org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_while=insert +org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_switch=do not insert +org.eclipse.cdt.core.formatter.insert_space_after_opening_paren_in_while=do not insert org.eclipse.cdt.core.formatter.insert_space_after_postfix_operator=do not insert org.eclipse.cdt.core.formatter.insert_space_after_prefix_operator=do not insert org.eclipse.cdt.core.formatter.insert_space_after_question_in_conditional=insert @@ -87,15 +87,15 @@ org.eclipse.cdt.core.formatter.insert_space_before_closing_angle_bracket_in_temp org.eclipse.cdt.core.formatter.insert_space_before_closing_brace_in_array_initializer=insert org.eclipse.cdt.core.formatter.insert_space_before_closing_bracket=do not insert org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_cast=do not insert -org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_catch=insert +org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_catch=do not insert org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_exception_specification=do not insert -org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_for=insert -org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_if=insert +org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_for=do not insert +org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_if=do not insert org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_method_declaration=do not insert org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_method_invocation=do not insert org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_parenthesized_expression=do not insert -org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_switch=insert -org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_while=insert +org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_switch=do not insert +org.eclipse.cdt.core.formatter.insert_space_before_closing_paren_in_while=do not insert org.eclipse.cdt.core.formatter.insert_space_before_colon_in_base_clause=insert org.eclipse.cdt.core.formatter.insert_space_before_colon_in_case=do not insert org.eclipse.cdt.core.formatter.insert_space_before_colon_in_conditional=insert diff --git a/config/antlr.m4 b/config/antlr.m4 new file mode 100644 index 000000000..e19f3c42d --- /dev/null +++ b/config/antlr.m4 @@ -0,0 +1,96 @@ +## +# Check for ANTLR's runantlr script. Will set ANTLR to the location of the +# runantlr script +## +AC_DEFUN([AC_PROG_ANTLR], [ + + # Get the location of the runantlr script + AC_ARG_WITH( + [antlr], + AC_HELP_STRING( + [--with-antlr=RUNANTLR], + [location of the ANTLR's `runantlr` script] + ), + ANTLR="$withval", + ANTLR="runantlr" + ) + + # Check the existance of the runantlr script + AC_CHECK_PROG(ANTLR, "$ANTLR", "$ANTLR", []) + if test no$ANTLR = "no"; + then + AC_MSG_WARN( + [Couldn't find the runantlr script, make sure that the parser code has + been generated already. To obtain ANTLR see .] + ) + AC_MSG_RESULT(no) + fi + + # Define the ANTL related variables + AC_SUBST(ANTLR) +]) + +## +# Check the existnace of the ANTLR C++ runtime library and headers +# Will set ANTLR_CPPFLAGS and ANTLR_LIBS to the location of the ANTLR headers +# and library respectively +## +AC_DEFUN([AC_LIB_ANTLR],[ + + # Get the location of the ANTLR c++ includes and libraries + AC_ARG_WITH( + [antlr-prefix], + AC_HELP_STRING( + [--with-antlr-prefix=PATH], + [set the search path for ANTLR headers and libraries to `PATH/include` + and `PATH/lib`. By default we look in /usr, /usr/local, /opt and + /opt/local. + ] + ), + ANTLR_PREFIXES="$withval", + ANTLR_PREFIXES="/usr/local /usr /opt/local /opt" + ) + + AC_MSG_CHECKING(for antlr C++ runtime library) + + # Use C++ and remember the variables we are changing + AC_LANG_PUSH(C++) + OLD_CPPFLAGS="$CPPFLAGS" + OLD_LIBS="$LIBS" + + # Try all the includes/libs set in ANTLR_PREFIXES + for antlr_prefix in $ANTLR_PREFIXES + do + CPPFLAGS="$OLD_CPPFLAGS -I$antlr_prefix/include" + LIBS="$OLD_LIBS -L$antlr_prefix/lib -lantlr" + AC_LINK_IFELSE( + [ + #include + class MyAST : public ANTLR_USE_NAMESPACE(antlr)CommonAST { + }; + int main() { + MyAST ast; + } + ], + [ + AC_MSG_RESULT(found in $antlr_prefix) + ANTLR_INCLUDES="-I$antlr_prefix/include" + ANTLR_LDFLAGS="-L$antlr_prefix/lib -lantlr" + break + ], + [ + AC_MSG_RESULT(no) + AC_MSG_ERROR([ANTLR C++ runtime not found, see ]) + ] + ) + done + + # Return the old compile variables and pop the language. + LIBS="$OLD_LIBS" + CPPFLAGS="$OLD_CPPFLAGS" + AC_LANG_POP() + + # Define the ANTLR include/libs variables + AC_SUBST(ANTLR_INCLUDES) + AC_SUBST(ANTLR_LDFLAGS) +]) \ No newline at end of file diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 800afc990..d44c970d2 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -1,9 +1,13 @@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -I@builddir@ +INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -I@builddir@ $(ANTLR_INCLUDES) AM_CXXFLAGS = -Wall -fvisibility=hidden AM_CPPFLAGS = -D__BUILDING_CVC4LIB +SUBDIRS = smt . + nobase_lib_LTLIBRARIES = libcvc4parser.la +libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) + libcvc4parser_la_SOURCES = \ parser.cpp \ parser_state.cpp \ @@ -11,7 +15,9 @@ libcvc4parser_la_SOURCES = \ pl_scanner.lpp \ pl.ypp \ smtlib_scanner.lpp \ - smtlib.ypp + smtlib.ypp \ + antlr_parser.cpp \ + antlr_parser.h BUILT_SOURCES = \ pl_scanner.cpp \ diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp new file mode 100644 index 000000000..c1cd85731 --- /dev/null +++ b/src/parser/antlr_parser.cpp @@ -0,0 +1,75 @@ +/* + * antlr_parser.cpp + * + * Created on: Nov 30, 2009 + * Author: dejan + */ + +#include "antlr_parser.h" +#include "expr/expr_manager.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::parser; + +ostream& operator <<(ostream& out, AntlrParser::BenchmarkStatus status) { + switch(status) { + case AntlrParser::SMT_SATISFIABLE: + out << "sat"; + break; + case AntlrParser::SMT_UNSATISFIABLE: + out << "unsat"; + break; + case AntlrParser::SMT_UNKNOWN: + out << "unknown"; + break; + default: + CVC4::UnhandledImpl("Unhandled ostream case for AntlrParser::BenchmarkStatus"); + } + return out; +} + +AntlrParser::AntlrParser(const antlr::ParserSharedInputState& state, int k) : + antlr::LLkParser(state, k) { +} + +AntlrParser::AntlrParser(antlr::TokenBuffer& tokenBuf, int k) : + antlr::LLkParser(tokenBuf, k) { +} + +AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) : + antlr::LLkParser(lexer, k) { +} + +Expr AntlrParser::getVariable(std::string var_name) { + cout << "getVariable(" << var_name << ")" << endl; + return d_expr_manager->mkExpr(VARIABLE); +} + +Expr AntlrParser::getTrueExpr() const { + return d_expr_manager->mkExpr(TRUE); +} + +Expr AntlrParser::getFalseExpr() const { + return d_expr_manager->mkExpr(FALSE); +} + +Expr AntlrParser::newExpression(Kind kind, const std::vector& children) { + cout << "newExpression(" << kind << ", " << children.size() + << ")" << endl; + return d_expr_manager->mkExpr(kind, children); +} + +void AntlrParser::newPredicate(std::string p_name, + std::vector& p_sorts) { + cout << "newPredicate(" << p_name << ", " << p_sorts.size() << ")" << endl; +} + +void AntlrParser::setBenchmarkStatus(BenchmarkStatus status) { + cout << "setBenchmarkStatus()" << endl; + d_benchmark_status = status; +} + +void AntlrParser::addExtraSorts(std::vector& extra_sorts) { + cout << "addExtraSorts()" << endl; +} diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h new file mode 100644 index 000000000..967721d26 --- /dev/null +++ b/src/parser/antlr_parser.h @@ -0,0 +1,151 @@ +/* + * antlr_parser.h + * + * Created on: Nov 30, 2009 + * Author: dejan + */ + +#ifndef CVC4_PARSER_H_ +#define CVC4_PARSER_H_ + +#include +#include +#include + +#include +#include "expr/expr.h" +#include "expr/expr_manager.h" +#include "util/command.h" +#include "util/assert.h" + +namespace CVC4 { + +namespace parser { + +/** + * Wrapper of the ANTLR parser that includes convenience methods that interacts + * with the expression manager. The grammars should have as little C++ code as + * possible and all the state and actuall functionality (besides parsing) should + * go into this class. + */ +class AntlrParser : public antlr::LLkParser { + +public: + + /** The status an SMT benchmark can have */ + enum BenchmarkStatus { + /** Benchmark is satisfiable */ + SMT_SATISFIABLE, + /** Benchmark is unsatisfiable */ + SMT_UNSATISFIABLE, + /** The status of the benchmark is unknown */ + SMT_UNKNOWN + }; + +protected: + + /** + * Class constructor, just tunnels the construction to the antlr + * LLkParser class. + * + * @param state the shared input state + * @param k lookahead + */ + AntlrParser(const antlr::ParserSharedInputState& state, int k); + + /** + * Class constructor, just tunnels the construction to the antlr + * LLkParser class. + * + * @param tokenBuf the token buffer to use in parsing + * @param k lookahead + */ + AntlrParser(antlr::TokenBuffer& tokenBuf, int k); + + /** + * Class constructor, just tunnels the construction to the antlr + * LLkParser class. + * + * @param lexer the lexer to use in parsing + * @param k lookahead + */ + AntlrParser(antlr::TokenStream& lexer, int k); + + /** + * Returns a variable, given a name and a type. + * @param var_name the name of the variable + * @return the variable expression + */ + Expr getVariable(std::string var_name); + + /** + * Returns the true expression. + * @return the true expression + */ + Expr getTrueExpr() const; + + /** + * Returns the false expression. + * @return the false expression + */ + Expr getFalseExpr() const; + + /** + * Creates a new CVC4 expression using the expression manager. + * @param kind the kind of the expression + * @param children the children of the expression + */ + Expr newExpression(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 + */ + void newPredicate(std::string p_name, std::vector& p_sorts); + + /** + * Sets the status of the benchmark. + * @param status the status of the benchmark + */ + void setBenchmarkStatus(BenchmarkStatus status); + + /** + * Returns the status of the parsed benchmark. + * @return the status of the parsed banchmark + */ + BenchmarkStatus getBenchmarkStatus() const; + + /** + * Adds the extra sorts to the signature of the benchmark. + * @param extra_sorts the sorts to add + */ + void addExtraSorts(std::vector& extra_sorts); + + /** + * + */ + void addCommand(Command* cmd); + + /** + * Set's the expression manager to use when creating/managing expression. + * @param expr_manager the expression manager + */ + void setExpressionManager(ExprManager* expr_manager); + +private: + + /** The status of the benchmark */ + BenchmarkStatus d_benchmark_status; + + /** The expression manager */ + ExprManager* d_expr_manager; +}; + +std::ostream& operator << (std::ostream& out, AntlrParser::BenchmarkStatus status); + +} + +} + +#endif /* CVC4_PARSER_H_ */ diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am new file mode 100644 index 000000000..54e3e9bf9 --- /dev/null +++ b/src/parser/smt/Makefile.am @@ -0,0 +1,19 @@ +SOURCES = \ + SmtLexer.g \ + SmtParser.g + SmtLexer.hpp \ + SmtLexer.cpp \ + SmtParser.hpp \ + SmtParser.cpp + +BUILT_SOURCES = \ + SmtLexer.hpp \ + SmtLexer.cpp \ + SmtParser.hpp \ + SmtParser.cpp + +SmtLexer.cpp SmtLexer.hpp: SmtLexer.g + $(ANTLR) SmtLexer.g + +SmtParser.cpp SmtParser.hpp: SmtParser.g + $(ANTLR) SmtParser.g diff --git a/src/parser/smt/SmtLexer.g b/src/parser/smt/SmtLexer.g new file mode 100644 index 000000000..6af685016 --- /dev/null +++ b/src/parser/smt/SmtLexer.g @@ -0,0 +1,152 @@ +options { + language = "Cpp"; // C++ output for antlr + namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace + 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 +} + +/** + * SmtLexer class is a stream tokenizer (lexer) for the SMT-LIB benchmark + * language. + */ +class SmtLexer extends Lexer; + +options { + exportVocab = SmtVocabulary; // 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; +} + +tokens { + // Base SMT-LIB tokens + DISTINCT = "distinct"; + ITE = "ite"; + TRUE = "true"; + FALSE = "false"; + NOT = "not"; + IMPLIES = "implies"; + IF_THEN_ELSE = "if_then_else"; + AND = "and"; + OR = "or"; + XOR = "xor"; + IFF = "iff"; + EXISTS = "exists"; + FORALL = "forall"; + LET = "let"; + FLET = "flet"; + THEORY = "theory"; + LOGIC = "logic"; + SAT = "sat"; + UNSAT = "unsat"; + 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"; +} + +/** + * Matches any letter ('a'-'z' and 'A'-'Z'). + */ +protected +ALPHA options{ paraphrase = "a letter"; } + : 'a'..'z' + | 'A'..'Z' + ; + +/** + * Matches the digits (0-9) + */ +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. + */ +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. + */ +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') + )* + '}' + ; + +/** + * Matches the question mark symbol ('?'). + */ +QUESTION_MARK options { paraphrase = "a question mark '?'"; } + : '?' + ; + +/** + * Matches the dollar sign ('$'). + */ +DOLLAR_SIGN options { paraphrase = "a dollar sign '$'"; } + : '$' + ; + +/** + * Matches the left bracket ('('). + */ +LPAREN options { paraphrase = "a left parenthesis '('"; } + : '('; + +/** + * Matches the right bracket ('('). + */ +RPAREN options { paraphrase = "a right parenthesis ')'"; } + : ')'; + +/** + * Matches and skips whitespace in the input. + */ +WHITESPACE options { paraphrase = "whitespace"; } + : (' ' | '\t' | '\f') { $setType(antlr::Token::SKIP); } + ; + +/** + * Mathces and skips the newline symbols in the input. + */ +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 double quoted string literal. No quote-escaping is supported inside. + */ +STRING_LITERAL options { paraphrase = "a string literal"; } + : '\"' (~('\"'))* '\"' + ; + diff --git a/src/parser/smt/SmtParser.g b/src/parser/smt/SmtParser.g new file mode 100644 index 000000000..f06951907 --- /dev/null +++ b/src/parser/smt/SmtParser.g @@ -0,0 +1,181 @@ +header "post_include_hpp" { +#include "parser/antlr_parser.h" +} + +header "post_include_cpp" { +#include + +using namespace std; +using namespace CVC4; +using namespace CVC4::parser; +} + +options { + language = "Cpp"; // C++ output for antlr + namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace + 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 +} + +/** + * SmtParser class is the parser for the SMT-LIB files. + */ +class SmtParser extends Parser("AntlrParser"); +options { + genHashLines = true; // Include line number information + importVocab = SmtVocabulary; // Export the common vocabulary + defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions + k = 2; +} + +/** + * 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 a predicate symbol from the input. + */ +pred_symb returns [std::string p] + : id:IDENTIFIER { p = id->getText(); } + ; + + +/** + * Matches a propositional atom from the input. + */ +prop_atom returns [CVC4::Expr atom] +{ + std::string p; +} + : p = pred_symb { atom = getVariable(p, boolType()); } + | TRUE { atom = getTrueExpr(); } + | FALSE { atom = getFalseExpr(); } + ; + +/** + * Matches an annotated proposition atom which is either a propositional atom, + * or built of other atoms using a predicate symbol. Annotation can be added if + * enclosed in brackets. The prop_atom rule from the original SMT grammar is inlined + * here in order to get rid of the ugly antlr non-determinism warrnings. + */ +an_atom returns [CVC4::Expr atom] + : atom = prop_atom + ; + +/** + * Matches on of the unary Boolean conectives. + */ +connective 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 an annotated formula. + */ +an_formula returns [CVC4::Expr formula] +{ + Kind kind; + vector children; +} + : formula = an_atom + | LPAREN kind = connective an_formulas[children] RPAREN { formula = newExpression(kind, children); } + ; + +an_formulas[std::vector& formulas] +{ + Expr f; +} + : ( f = an_formula { formulas.push_back(f); } )+ + ; + +/** + * Matches the declaration of a predicate symbol. + */ +pred_symb_decl +{ + string p_name; + vector p_sorts; +} + : LPAREN p_name = pred_symb sort_symbs[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] +{ + std::string type; +} + : ( type = sort_symb { sorts.push_back(type); })* + ; + +/** + * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'. + */ +status returns [ SmtParser::BenchmarkStatus status ] + : SAT { status = SMT_SATISFIABLE; } + | UNSAT { status = SMT_UNSATISFIABLE; } + | UNKNOWN { status = SMT_UNKNOWN; } + ; + +/** + * Matches a benchmark attribute, sucha as ':logic', ':formula', etc. + */ +bench_attribute returns [ Command* smt_command ] +{ + smt_command = 0; + BenchmarkStatus b_status = SMT_UNKNOWN; + Expr formula; + vector sorts; +} + : C_LOGIC IDENTIFIER + | C_ASSUMPTION formula = an_formula { smt_command = new AssertCommand(formula); } + | C_FORMULA formula = an_formula { smt_command = new CheckSatCommand(formula); } + | C_STATUS b_status = status { setBenchmarkStatus(b_status); } + | C_EXTRASORTS LPAREN sort_symbs[sorts] RPAREN { addExtraSorts(sorts); } + | C_EXTRAPREDS LPAREN (pred_symb_decl)+ RPAREN + | C_NOTES STRING_LITERAL + | annotation + ; + +/** + * Returns a pointer to a command sequence command. + */ +bench_attributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence()] +{ + Command* cmd; +} + : (cmd = bench_attribute { cmd_seq->addCommand(cmd); } )+ + ; + +/** + * Matches the whole SMT-LIB benchmark. + */ +benchmark +{ + Command* cmd_seq; +} + : LPAREN BENCHMARK IDENTIFIER cmd_seq = bench_attributes RPAREN { addCommand(cmd_seq); } + ; -- 2.30.2