-#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
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
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
--- /dev/null
+##
+# 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 <http://www.antlr.org/>.]
+ )
+ 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 <antlr/CommonAST.hpp>
+ 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 <http://www.antlr.org/>])
+ ]
+ )
+ 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
-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 \
pl_scanner.lpp \
pl.ypp \
smtlib_scanner.lpp \
- smtlib.ypp
+ smtlib.ypp \
+ antlr_parser.cpp \
+ antlr_parser.h
BUILT_SOURCES = \
pl_scanner.cpp \
--- /dev/null
+/*
+ * 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<Expr>& children) {
+ cout << "newExpression(" << kind << ", " << children.size()
+ << ")" << endl;
+ return d_expr_manager->mkExpr(kind, children);
+}
+
+void AntlrParser::newPredicate(std::string p_name,
+ std::vector<std::string>& 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<std::string>& extra_sorts) {
+ cout << "addExtraSorts()" << endl;
+}
--- /dev/null
+/*
+ * antlr_parser.h
+ *
+ * Created on: Nov 30, 2009
+ * Author: dejan
+ */
+
+#ifndef CVC4_PARSER_H_
+#define CVC4_PARSER_H_
+
+#include <vector>
+#include <string>
+#include <iostream>
+
+#include <antlr/LLkParser.hpp>
+#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<Expr>& 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<std::string>& 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<std::string>& 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_ */
--- /dev/null
+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
--- /dev/null
+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"; }
+ : '\"' (~('\"'))* '\"'
+ ;
+
--- /dev/null
+header "post_include_hpp" {
+#include "parser/antlr_parser.h"
+}
+
+header "post_include_cpp" {
+#include <vector>
+
+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<Expr> children;
+}
+ : formula = an_atom
+ | LPAREN kind = connective an_formulas[children] RPAREN { formula = newExpression(kind, children); }
+ ;
+
+an_formulas[std::vector<Expr>& formulas]
+{
+ Expr f;
+}
+ : ( f = an_formula { formulas.push_back(f); } )+
+ ;
+
+/**
+ * Matches the declaration of a predicate symbol.
+ */
+pred_symb_decl
+{
+ string p_name;
+ vector<string> 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<std::string>& 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<string> 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); }
+ ;
projects / cvc5.git / commitdiff