diff options
| -rw-r--r-- | .cproject | 2 | ||||
| -rw-r--r-- | .project | 2 | ||||
| -rw-r--r-- | .settings/org.eclipse.cdt.core.prefs | 6 | ||||
| -rw-r--r-- | configure.ac | 1 | ||||
| -rw-r--r-- | src/main/main.cpp | 11 | ||||
| -rw-r--r-- | src/parser/Makefile.am | 5 | ||||
| -rw-r--r-- | src/parser/antlr_parser.cpp | 84 | ||||
| -rw-r--r-- | src/parser/antlr_parser.h | 44 | ||||
| -rw-r--r-- | src/parser/cvc/CvcLexer.g | 127 | ||||
| -rw-r--r-- | src/parser/cvc/CvcParser.g | 111 | ||||
| -rw-r--r-- | src/parser/cvc/Makefile.am | 28 | ||||
| -rw-r--r-- | src/parser/cvc/Makefile.in | 502 | ||||
| -rw-r--r-- | src/parser/parser.cpp | 76 | ||||
| -rw-r--r-- | src/parser/parser.h | 70 | ||||
| -rw-r--r-- | src/util/assert.h | 18 | ||||
| -rw-r--r-- | src/util/command.cpp | 5 | ||||
| -rw-r--r-- | src/util/command.h | 4 |
17 files changed, 1048 insertions, 48 deletions
@@ -19,7 +19,7 @@ <folderInfo id="cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216" name="/" resourcePath=""> <toolChain id="cdt.managedbuild.toolchain.gnu.base.1311293674" name="cdt.managedbuild.toolchain.gnu.base" superClass="cdt.managedbuild.toolchain.gnu.base"> <targetPlatform archList="all" binaryParser="org.eclipse.cdt.core.ELF" id="cdt.managedbuild.target.gnu.platform.base.1799734525" name="Debug Platform" osList="linux,hpux,aix,qnx" superClass="cdt.managedbuild.target.gnu.platform.base"/> -<builder buildPath="${workspace_loc/cvc4/}" id="cdt.managedbuild.target.gnu.builder.base.549477204" incrementalBuildTarget="all" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make Builder" parallelBuildOn="true" parallelizationNumber="-1" superClass="cdt.managedbuild.target.gnu.builder.base"/> +<builder buildPath="${workspace_loc/cvc4/}" id="cdt.managedbuild.target.gnu.builder.base.549477204" incrementalBuildTarget="all" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make Builder" parallelBuildOn="false" parallelizationNumber="-1" superClass="cdt.managedbuild.target.gnu.builder.base"/> <tool id="cdt.managedbuild.tool.gnu.archiver.base.888684090" name="GCC Archiver" superClass="cdt.managedbuild.tool.gnu.archiver.base"/> <tool id="cdt.managedbuild.tool.gnu.cpp.compiler.base.1803857875" name="GCC C++ Compiler" superClass="cdt.managedbuild.tool.gnu.cpp.compiler.base"> <inputType id="cdt.managedbuild.tool.gnu.cpp.compiler.input.1333398893" superClass="cdt.managedbuild.tool.gnu.cpp.compiler.input"/> @@ -23,7 +23,7 @@ </dictionary> <dictionary> <key>org.eclipse.cdt.make.core.buildArguments</key> - <value>-j</value> + <value></value> </dictionary> <dictionary> <key>org.eclipse.cdt.make.core.buildCommand</key> diff --git a/.settings/org.eclipse.cdt.core.prefs b/.settings/org.eclipse.cdt.core.prefs index acec742e4..720185193 100644 --- a/.settings/org.eclipse.cdt.core.prefs +++ b/.settings/org.eclipse.cdt.core.prefs @@ -1,6 +1,6 @@ -#Thu Dec 03 16:22:24 EST 2009 +#Sun Dec 06 22:53:15 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_arguments_in_method_invocation=18 org.eclipse.cdt.core.formatter.alignment_for_base_clause_in_type_declaration=80 org.eclipse.cdt.core.formatter.alignment_for_compact_if=0 org.eclipse.cdt.core.formatter.alignment_for_conditional_expression=80 @@ -8,7 +8,7 @@ org.eclipse.cdt.core.formatter.alignment_for_declarator_list=16 org.eclipse.cdt.core.formatter.alignment_for_enumerator_list=48 org.eclipse.cdt.core.formatter.alignment_for_expression_list=0 org.eclipse.cdt.core.formatter.alignment_for_expressions_in_array_initializer=16 -org.eclipse.cdt.core.formatter.alignment_for_parameters_in_method_declaration=16 +org.eclipse.cdt.core.formatter.alignment_for_parameters_in_method_declaration=18 org.eclipse.cdt.core.formatter.alignment_for_throws_clause_in_method_declaration=16 org.eclipse.cdt.core.formatter.brace_position_for_array_initializer=end_of_line org.eclipse.cdt.core.formatter.brace_position_for_block=end_of_line diff --git a/configure.ac b/configure.ac index e6ad11733..e739f5cee 100644 --- a/configure.ac +++ b/configure.ac @@ -346,6 +346,7 @@ AC_CONFIG_FILES([ src/util/Makefile src/context/Makefile src/parser/Makefile + src/parser/cvc/Makefile src/parser/smt/Makefile src/theory/Makefile test/Makefile diff --git a/src/main/main.cpp b/src/main/main.cpp index b7833e3ca..4c3a21811 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -65,8 +65,17 @@ int main(int argc, char *argv[]) { else parser = new SmtParser(&exprMgr, argv[firstArgIndex]); break; + case Options::LANG_CVC4: + if(inputFromStdin) + parser = new CvcParser(&exprMgr, cin); + else + parser = new CvcParser(&exprMgr, argv[firstArgIndex]); + break; + case Options::LANG_AUTO: + cerr << "Auto language detection not supported yet." << endl; + abort(); default: - cerr << "Language" << options.lang << "not supported yet." << endl; + cerr << "Unknown language" << endl; abort(); } diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 3c2bfc8ab..5e601fd59 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -19,13 +19,14 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. $(ANTLR_INCLUDES) AM_CXXFLAGS = -Wall -fvisibility=hidden AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB -SUBDIRS = smt +SUBDIRS = smt cvc nobase_lib_LTLIBRARIES = libcvc4parser.la libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) libcvc4parser_la_LIBADD = \ - @builddir@/smt/libparsersmt.la + @builddir@/smt/libparsersmt.la \ + @builddir@/cvc/libparsercvc.la libcvc4parser_la_SOURCES = \ parser.h \ diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index c4e6eef19..52f3c4668 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -26,12 +26,30 @@ ostream& operator <<(ostream& out, AntlrParser::BenchmarkStatus status) { out << "unknown"; break; default: - CVC4::UnhandledImpl( - "Unhandled ostream case for AntlrParser::BenchmarkStatus"); + Unhandled("Unhandled ostream case for AntlrParser::BenchmarkStatus"); } return out; } +unsigned AntlrParser::getPrecedence(Kind kind) { + switch(kind) { + // Boolean operators + case OR: + return 5; + case AND: + return 4; + case IFF: + return 3; + case IMPLIES: + return 2; + case XOR: + return 1; + default: + Unhandled ("Undefined precedence - necessary for proper parsing of CVC files!"); + } + return 0; +} + AntlrParser::AntlrParser(const antlr::ParserSharedInputState& state, int k) : antlr::LLkParser(state, k) { } @@ -56,23 +74,37 @@ Expr AntlrParser::getFalseExpr() const { return d_expr_manager->mkExpr(FALSE); } +Expr AntlrParser::newExpression(Kind kind, const Expr& child) { + return d_expr_manager->mkExpr(kind, child); +} + +Expr AntlrParser::newExpression(Kind kind, const Expr& child_1, const Expr& child_2) { + return d_expr_manager->mkExpr(kind, child_1, child_2); +} + Expr AntlrParser::newExpression(Kind kind, const std::vector<Expr>& children) { return d_expr_manager->mkExpr(kind, children); } -void AntlrParser::newPredicate(std::string p_name, - std::vector<std::string>& p_sorts) { +void AntlrParser::newPredicate(std::string p_name, const std::vector< + std::string>& p_sorts) { if(p_sorts.size() == 0) d_var_symbol_table.bindName(p_name, d_expr_manager->mkExpr(VARIABLE)); else Unhandled("Non unary predicate not supported yet!"); } +void AntlrParser::newPredicates(const std::vector<std::string>& p_names) { + vector<string> sorts; + for(unsigned i = 0; i < p_names.size(); ++i) + newPredicate(p_names[i], sorts); +} + void AntlrParser::setBenchmarkStatus(BenchmarkStatus status) { d_benchmark_status = status; } -void AntlrParser::addExtraSorts(std::vector<std::string>& extra_sorts) { +void AntlrParser::addExtraSorts(const std::vector<std::string>& extra_sorts) { } void AntlrParser::setExpressionManager(ExprManager* em) { @@ -88,6 +120,44 @@ bool AntlrParser::isDeclared(string name, SymbolType type) { } } -void AntlrParser::rethrow(antlr::SemanticException& e, string new_message) throw(antlr::SemanticException) { - throw antlr::SemanticException(new_message, getFilename(), LT(0).get()->getLine(), LT(0).get()->getColumn()); +void AntlrParser::rethrow(antlr::SemanticException& e, string new_message) + throw (antlr::SemanticException) { + throw antlr::SemanticException(new_message, getFilename(), + LT(0).get()->getLine(), + LT(0).get()->getColumn()); +} + +Expr AntlrParser::createPrecedenceExpr(const vector<Expr>& exprs, const vector< + Kind>& kinds) { + return createPrecedenceExpr(exprs, kinds, 0, exprs.size() - 1); +} + +unsigned AntlrParser::findPivot(const std::vector<Kind>& kinds, + unsigned start_index, unsigned end_index) const { + + int pivot = start_index; + unsigned pivot_precedence = getPrecedence(kinds[pivot]); + + for(unsigned i = start_index + 1; i <= end_index; ++i) { + unsigned current_precedence = getPrecedence(kinds[i]); + if(current_precedence > pivot_precedence) { + pivot = i; + pivot_precedence = current_precedence; + } + } + + return pivot; +} + +Expr AntlrParser::createPrecedenceExpr(const std::vector<Expr>& exprs, + const std::vector<Kind>& kinds, + unsigned start_index, unsigned end_index) { + if(start_index == end_index) + return exprs[start_index]; + + unsigned pivot = findPivot(kinds, start_index, end_index - 1); + + Expr child_1 = createPrecedenceExpr(exprs, kinds, start_index, pivot); + Expr child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index); + return d_expr_manager->mkExpr(kinds[pivot], child_1, child_2); } diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index 31310da30..6bac079c8 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -123,6 +123,20 @@ protected: Expr getFalseExpr() const; /** + * Creates a new unary CVC4 expression using the expression manager. + * @param kind the kind of the expression + * @param child the child + */ + Expr newExpression(Kind kind, const Expr& child); + + /** + * Creates a new binary 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 Expr& child_1, const Expr& child_2); + + /** * Creates a new CVC4 expression using the expression manager. * @param kind the kind of the expression * @param children the children of the expression @@ -130,11 +144,23 @@ protected: Expr newExpression(Kind kind, const std::vector<Expr>& children); /** + * Creates a new expression based on the given string of expressions and kinds. + * The expression is created so that it respects the kinds precedence table. + */ + Expr createPrecedenceExpr(const std::vector<Expr>& exprs, const std::vector<Kind>& kinds); + + /** * 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); + void newPredicate(std::string p_name, const std::vector<std::string>& p_sorts); + + /** + * Creates new predicates of given types. + * @param p_names the names of the predicates + */ + void newPredicates(const std::vector<std::string>& p_names); /** * Sets the status of the benchmark. @@ -152,10 +178,24 @@ protected: * 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 addExtraSorts(const std::vector<std::string>& extra_sorts); + + /** + * Returns the precedence rank of the kind. + */ + static unsigned getPrecedence(Kind kind); private: + + unsigned findPivot(const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index) const; + + /** + * Creates a new expression based on the given string of expressions and kinds. + * The expression is created so that it respects the kinds precedence table. + */ + Expr createPrecedenceExpr(const std::vector<Expr>& exprs, const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index); + /** The status of the benchmark */ BenchmarkStatus d_benchmark_status; diff --git a/src/parser/cvc/CvcLexer.g b/src/parser/cvc/CvcLexer.g new file mode 100644 index 000000000..8d706963f --- /dev/null +++ b/src/parser/cvc/CvcLexer.g @@ -0,0 +1,127 @@ +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. + */ +class AntlrCvcLexer extends Lexer; + +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; +} + +tokens { + // Types + BOOLEAN = "BOOLEAN"; + // Boolean oparators + AND = "AND"; + IF = "IF"; + THEN = "THEN"; + ELSE = "ELSE"; + ELSEIF = "ELSIF"; + ENDIF = "ENDIF"; + NOT = "NOT"; + OR = "OR"; + TRUE = "TRUE"; + FALSE = "FALSE"; + XOR = "XOR"; + IMPLIES = "=>"; + IFF = "<=>"; + // Commands + ASSERT = "ASSERT"; + QUERY = "QUERY"; + CHECKSAT = "CHECKSAT"; + PRINT = "PRINT"; + EXHO = "ECHO"; + + PUSH = "PUSH"; + POP = "POP"; + POPTO = "POPTO"; +} + +/** + * 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 the ':' + */ +COLON options{ paraphrase = "a comma"; } + : ':' + ; + +/** + * Matches the ',' + */ +COMMA options{ paraphrase = "a comma"; } + : ',' + ; + +/** + * 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 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 and ignores it. + */ +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(); } + ; + +/** + * Mathces the comments and ignores them + */ +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/CvcParser.g b/src/parser/cvc/CvcParser.g new file mode 100644 index 000000000..625f2c381 --- /dev/null +++ b/src/parser/cvc/CvcParser.g @@ -0,0 +1,111 @@ +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 + 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. + */ +class AntlrCvcParser extends Parser("AntlrParser"); +options { + genHashLines = true; // Include line number information + importVocab = CvcVocabulary; // Import the common vocabulary + defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions + k = 2; +} + +/** + * Matches a command of the input. If a declaration, it will return an empty + * command. + */ +command returns [CVC4::Command* cmd = 0] +{ + Expr f; + vector<string> ids; +} + : ASSERT f = formula { cmd = new AssertCommand(f); } + | QUERY f = formula { cmd = new QueryCommand(f); } + | CHECKSAT f = formula { cmd = new CheckSatCommand(f); } + | CHECKSAT { cmd = new CheckSatCommand(); } + | identifierList[ids] COLON type { + newPredicates(ids); + cmd = new EmptyCommand("Declaration"); + } + | EOF + ; + +identifierList[std::vector<std::string>& id_list] + : id1:IDENTIFIER { id_list.push_back(id1->getText()); } + ( + COMMA + id2:IDENTIFIER { id_list.push_back(id2->getText()); } + )* + ; + +type + : BOOLEAN + ; + +formula returns [CVC4::Expr formula] + : formula = bool_formula + ; + +bool_formula returns [CVC4::Expr formula] +{ + vector<Expr> formulas; + vector<Kind> kinds; + Expr f1, f2; + Kind k; +} + : f1 = primary_bool_formula { formulas.push_back(f1); } + ( k = bool_operator { kinds.push_back(k); } f2 = primary_bool_formula { formulas.push_back(f2); } )* + { + // Create the expression based on precedences + formula = createPrecedenceExpr(formulas, kinds); + } + ; + +primary_bool_formula returns [CVC4::Expr formula] + : formula = bool_atom + | NOT formula = primary_bool_formula { formula = newExpression(CVC4::NOT, formula); } + | LPAREN formula = bool_formula RPAREN + ; + +bool_operator returns [CVC4::Kind kind] + : IMPLIES { kind = CVC4::IMPLIES; } + | AND { kind = CVC4::AND; } + | OR { kind = CVC4::OR; } + | XOR { kind = CVC4::XOR; } + | IFF { kind = CVC4::IFF; } + ; + +bool_atom returns [CVC4::Expr atom] +{ + string p; +} + : p = predicate_sym {isDeclared(p, SYM_VARIABLE)}? { atom = getVariable(p); } + exception catch [antlr::SemanticException ex] { + rethrow(ex, "Undeclared variable " + p); + } + | TRUE { atom = getTrueExpr(); } + | FALSE { atom = getFalseExpr(); } + ; + +predicate_sym returns [std::string p] + : id:IDENTIFIER { p = id->getText(); } + ; +
\ No newline at end of file diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am new file mode 100644 index 000000000..9f548d656 --- /dev/null +++ b/src/parser/cvc/Makefile.am @@ -0,0 +1,28 @@ +INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. +AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB + +noinst_LTLIBRARIES = libparsercvc.la + +libparsercvc_la_SOURCES = \ + CvcLexer.g \ + CvcParser.g \ + AntlrCvcLexer.hpp \ + AntlrCvcLexer.cpp \ + AntlrCvcParser.hpp \ + AntlrCvcParser.cpp + +BUILT_SOURCES = \ + AntlrCvcLexer.hpp \ + AntlrCvcLexer.cpp \ + AntlrCvcParser.hpp \ + AntlrCvcParser.cpp + + +AntlrCvcLexer.hpp: CvcLexer.g +AntlrCvcLexer.cpp: CvcLexer.g + $(ANTLR) @srcdir@/CvcLexer.g + +AntlrCvcParser.hpp: CvcParser.g AntlrCvcLexer.cpp +AntlrCvcParser.cpp: CvcParser.g AntlrCvcLexer.cpp + $(ANTLR) @srcdir@/CvcParser.g diff --git a/src/parser/cvc/Makefile.in b/src/parser/cvc/Makefile.in new file mode 100644 index 000000000..54c641bb6 --- /dev/null +++ b/src/parser/cvc/Makefile.in @@ -0,0 +1,502 @@ +# Makefile.in generated by automake 1.9.6 from Makefile.am. +# @configure_input@ + +# Copyright (C) 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001, 2002, +# 2003, 2004, 2005 Free Software Foundation, Inc. +# This Makefile.in is free software; the Free Software Foundation +# gives unlimited permission to copy and/or distribute it, +# with or without modifications, as long as this notice is preserved. + +# This program is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY, to the extent permitted by law; without +# even the implied warranty of MERCHANTABILITY or FITNESS FOR A +# PARTICULAR PURPOSE. + +@SET_MAKE@ + +srcdir = @srcdir@ +top_srcdir = @top_srcdir@ +VPATH = @srcdir@ +pkgdatadir = $(datadir)/@PACKAGE@ +pkglibdir = $(libdir)/@PACKAGE@ +pkgincludedir = $(includedir)/@PACKAGE@ +top_builddir = ../../.. +am__cd = CDPATH="$${ZSH_VERSION+.}$(PATH_SEPARATOR)" && cd +INSTALL = @INSTALL@ +install_sh_DATA = $(install_sh) -c -m 644 +install_sh_PROGRAM = $(install_sh) -c +install_sh_SCRIPT = $(install_sh) -c +INSTALL_HEADER = $(INSTALL_DATA) +transform = $(program_transform_name) +NORMAL_INSTALL = : +PRE_INSTALL = : +POST_INSTALL = : +NORMAL_UNINSTALL = : +PRE_UNINSTALL = : +POST_UNINSTALL = : +build_triplet = @build@ +host_triplet = @host@ +target_triplet = @target@ +subdir = src/parser/cvc +DIST_COMMON = $(srcdir)/Makefile.am $(srcdir)/Makefile.in +ACLOCAL_M4 = $(top_srcdir)/aclocal.m4 +am__aclocal_m4_deps = $(top_srcdir)/config/antlr.m4 \ + $(top_srcdir)/config/libtool.m4 \ + $(top_srcdir)/config/ltoptions.m4 \ + $(top_srcdir)/config/ltsugar.m4 \ + $(top_srcdir)/config/ltversion.m4 \ + $(top_srcdir)/config/lt~obsolete.m4 $(top_srcdir)/configure.ac +am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \ + $(ACLOCAL_M4) +mkinstalldirs = $(install_sh) -d +CONFIG_HEADER = $(top_builddir)/config.h +CONFIG_CLEAN_FILES = +LTLIBRARIES = $(noinst_LTLIBRARIES) +libparsercvc_la_LIBADD = +am_libparsercvc_la_OBJECTS = AntlrCvcLexer.lo AntlrCvcParser.lo +libparsercvc_la_OBJECTS = $(am_libparsercvc_la_OBJECTS) +DEFAULT_INCLUDES = -I. -I$(srcdir) -I$(top_builddir) +depcomp = $(SHELL) $(top_srcdir)/config/depcomp +am__depfiles_maybe = depfiles +CXXCOMPILE = $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \ + $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS) +LTCXXCOMPILE = $(LIBTOOL) --tag=CXX --mode=compile $(CXX) $(DEFS) \ + $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) \ + $(AM_CXXFLAGS) $(CXXFLAGS) +CXXLD = $(CXX) +CXXLINK = $(LIBTOOL) --tag=CXX --mode=link $(CXXLD) $(AM_CXXFLAGS) \ + $(CXXFLAGS) $(AM_LDFLAGS) $(LDFLAGS) -o $@ +COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \ + $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS) +LTCOMPILE = $(LIBTOOL) --tag=CC --mode=compile $(CC) $(DEFS) \ + $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) \ + $(AM_CFLAGS) $(CFLAGS) +CCLD = $(CC) +LINK = $(LIBTOOL) --tag=CC --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) \ + $(AM_LDFLAGS) $(LDFLAGS) -o $@ +SOURCES = $(libparsercvc_la_SOURCES) +DIST_SOURCES = $(libparsercvc_la_SOURCES) +ETAGS = etags +CTAGS = ctags +DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST) +ACLOCAL = @ACLOCAL@ +AMDEP_FALSE = @AMDEP_FALSE@ +AMDEP_TRUE = @AMDEP_TRUE@ +AMTAR = @AMTAR@ +ANTLR = @ANTLR@ +ANTLR_INCLUDES = @ANTLR_INCLUDES@ +ANTLR_LDFLAGS = @ANTLR_LDFLAGS@ +AR = @AR@ +AS = @AS@ +AUTOCONF = @AUTOCONF@ +AUTOHEADER = @AUTOHEADER@ +AUTOMAKE = @AUTOMAKE@ +AWK = @AWK@ +CC = @CC@ +CCDEPMODE = @CCDEPMODE@ +CFLAGS = @CFLAGS@ +CPP = @CPP@ +CPPFLAGS = @CPPFLAGS@ +CVC4_LIBRARY_RELEASE_CODE = @CVC4_LIBRARY_RELEASE_CODE@ +CVC4_LIBRARY_VERSION = @CVC4_LIBRARY_VERSION@ +CVC4_PARSER_LIBRARY_VERSION = @CVC4_PARSER_LIBRARY_VERSION@ +CXX = @CXX@ +CXXCPP = @CXXCPP@ +CXXDEPMODE = @CXXDEPMODE@ +CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ +CXXTESTGEN = @CXXTESTGEN@ +CYGPATH_W = @CYGPATH_W@ +DEFS = @DEFS@ +DEPDIR = @DEPDIR@ +DLLTOOL = @DLLTOOL@ +DOXYGEN = @DOXYGEN@ +DSYMUTIL = @DSYMUTIL@ +DUMPBIN = @DUMPBIN@ +ECHO_C = @ECHO_C@ +ECHO_N = @ECHO_N@ +ECHO_T = @ECHO_T@ +EGREP = @EGREP@ +EXEEXT = @EXEEXT@ +FGREP = @FGREP@ +GREP = @GREP@ +HAVE_CXXTESTGEN_FALSE = @HAVE_CXXTESTGEN_FALSE@ +HAVE_CXXTESTGEN_TRUE = @HAVE_CXXTESTGEN_TRUE@ +INSTALL_DATA = @INSTALL_DATA@ +INSTALL_PROGRAM = @INSTALL_PROGRAM@ +INSTALL_SCRIPT = @INSTALL_SCRIPT@ +INSTALL_STRIP_PROGRAM = @INSTALL_STRIP_PROGRAM@ +LD = @LD@ +LDFLAGS = @LDFLAGS@ +LEX = @LEX@ +LEXLIB = @LEXLIB@ +LEX_OUTPUT_ROOT = @LEX_OUTPUT_ROOT@ +LIBOBJS = @LIBOBJS@ +LIBS = @LIBS@ +LIBTOOL = @LIBTOOL@ +LIPO = @LIPO@ +LN_S = @LN_S@ +LTLIBOBJS = @LTLIBOBJS@ +MAKEINFO = @MAKEINFO@ +NM = @NM@ +NMEDIT = @NMEDIT@ +OBJDUMP = @OBJDUMP@ +OBJEXT = @OBJEXT@ +OTOOL = @OTOOL@ +OTOOL64 = @OTOOL64@ +PACKAGE = @PACKAGE@ +PACKAGE_BUGREPORT = @PACKAGE_BUGREPORT@ +PACKAGE_NAME = @PACKAGE_NAME@ +PACKAGE_STRING = @PACKAGE_STRING@ +PACKAGE_TARNAME = @PACKAGE_TARNAME@ +PACKAGE_URL = @PACKAGE_URL@ +PACKAGE_VERSION = @PACKAGE_VERSION@ +PATH_SEPARATOR = @PATH_SEPARATOR@ +PERL = @PERL@ +RANLIB = @RANLIB@ +SED = @SED@ +SET_MAKE = @SET_MAKE@ +SHELL = @SHELL@ +STRIP = @STRIP@ +TEST_CPPFLAGS = @TEST_CPPFLAGS@ +TEST_CXXFLAGS = @TEST_CXXFLAGS@ +TEST_LDFLAGS = @TEST_LDFLAGS@ +VERSION = @VERSION@ +YACC = @YACC@ +YFLAGS = @YFLAGS@ +ac_ct_CC = @ac_ct_CC@ +ac_ct_CXX = @ac_ct_CXX@ +ac_ct_DUMPBIN = @ac_ct_DUMPBIN@ +am__fastdepCC_FALSE = @am__fastdepCC_FALSE@ +am__fastdepCC_TRUE = @am__fastdepCC_TRUE@ +am__fastdepCXX_FALSE = @am__fastdepCXX_FALSE@ +am__fastdepCXX_TRUE = @am__fastdepCXX_TRUE@ +am__include = @am__include@ +am__leading_dot = @am__leading_dot@ +am__quote = @am__quote@ +am__tar = @am__tar@ +am__untar = @am__untar@ +bindir = @bindir@ +build = @build@ +build_alias = @build_alias@ +build_cpu = @build_cpu@ +build_os = @build_os@ +build_vendor = @build_vendor@ +datadir = @datadir@ +datarootdir = @datarootdir@ +docdir = @docdir@ +dvidir = @dvidir@ +exec_prefix = @exec_prefix@ +host = @host@ +host_alias = @host_alias@ +host_cpu = @host_cpu@ +host_os = @host_os@ +host_vendor = @host_vendor@ +htmldir = @htmldir@ +includedir = @includedir@ +infodir = @infodir@ +install_sh = @install_sh@ +libdir = @libdir@ +libexecdir = @libexecdir@ +localedir = @localedir@ +localstatedir = @localstatedir@ +lt_ECHO = @lt_ECHO@ +mandir = @mandir@ +mkdir_p = @mkdir_p@ +oldincludedir = @oldincludedir@ +pdfdir = @pdfdir@ +prefix = @prefix@ +program_transform_name = @program_transform_name@ +psdir = @psdir@ +sbindir = @sbindir@ +sharedstatedir = @sharedstatedir@ +sysconfdir = @sysconfdir@ +target = @target@ +target_alias = @target_alias@ +target_cpu = @target_cpu@ +target_os = @target_os@ +target_vendor = @target_vendor@ +INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. +AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB +noinst_LTLIBRARIES = libparsercvc.la +libparsercvc_la_SOURCES = \ + CvcLexer.g \ + CvcParser.g \ + AntlrCvcLexer.hpp \ + AntlrCvcLexer.cpp \ + AntlrCvcParser.hpp \ + AntlrCvcParser.cpp + +BUILT_SOURCES = \ + AntlrCvcLexer.hpp \ + AntlrCvcLexer.cpp \ + AntlrCvcParser.hpp \ + AntlrCvcParser.cpp + +all: $(BUILT_SOURCES) + $(MAKE) $(AM_MAKEFLAGS) all-am + +.SUFFIXES: +.SUFFIXES: .cpp .lo .o .obj +$(srcdir)/Makefile.in: $(srcdir)/Makefile.am $(am__configure_deps) + @for dep in $?; do \ + case '$(am__configure_deps)' in \ + *$$dep*) \ + cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh \ + && exit 0; \ + exit 1;; \ + esac; \ + done; \ + echo ' cd $(top_srcdir) && $(AUTOMAKE) --foreign src/parser/cvc/Makefile'; \ + cd $(top_srcdir) && \ + $(AUTOMAKE) --foreign src/parser/cvc/Makefile +.PRECIOUS: Makefile +Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status + @case '$?' in \ + *config.status*) \ + cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh;; \ + *) \ + echo ' cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe)'; \ + cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe);; \ + esac; + +$(top_builddir)/config.status: $(top_srcdir)/configure $(CONFIG_STATUS_DEPENDENCIES) + cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh + +$(top_srcdir)/configure: $(am__configure_deps) + cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh +$(ACLOCAL_M4): $(am__aclocal_m4_deps) + cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh + +clean-noinstLTLIBRARIES: + -test -z "$(noinst_LTLIBRARIES)" || rm -f $(noinst_LTLIBRARIES) + @list='$(noinst_LTLIBRARIES)'; for p in $$list; do \ + dir="`echo $$p | sed -e 's|/[^/]*$$||'`"; \ + test "$$dir" != "$$p" || dir=.; \ + echo "rm -f \"$${dir}/so_locations\""; \ + rm -f "$${dir}/so_locations"; \ + done +libparsercvc.la: $(libparsercvc_la_OBJECTS) $(libparsercvc_la_DEPENDENCIES) + $(CXXLINK) $(libparsercvc_la_LDFLAGS) $(libparsercvc_la_OBJECTS) $(libparsercvc_la_LIBADD) $(LIBS) + +mostlyclean-compile: + -rm -f *.$(OBJEXT) + +distclean-compile: + -rm -f *.tab.c + +@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrCvcLexer.Plo@am__quote@ +@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrCvcParser.Plo@am__quote@ + +.cpp.o: +@am__fastdepCXX_TRUE@ if $(CXXCOMPILE) -MT $@ -MD -MP -MF "$(DEPDIR)/$*.Tpo" -c -o $@ $<; \ +@am__fastdepCXX_TRUE@ then mv -f "$(DEPDIR)/$*.Tpo" "$(DEPDIR)/$*.Po"; else rm -f "$(DEPDIR)/$*.Tpo"; exit 1; fi +@AMDEP_TRUE@@am__fastdepCXX_FALSE@ source='$<' object='$@' libtool=no @AMDEPBACKSLASH@ +@AMDEP_TRUE@@am__fastdepCXX_FALSE@ DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@ +@am__fastdepCXX_FALSE@ $(CXXCOMPILE) -c -o $@ $< + +.cpp.obj: +@am__fastdepCXX_TRUE@ if $(CXXCOMPILE) -MT $@ -MD -MP -MF "$(DEPDIR)/$*.Tpo" -c -o $@ `$(CYGPATH_W) '$<'`; \ +@am__fastdepCXX_TRUE@ then mv -f "$(DEPDIR)/$*.Tpo" "$(DEPDIR)/$*.Po"; else rm -f "$(DEPDIR)/$*.Tpo"; exit 1; fi +@AMDEP_TRUE@@am__fastdepCXX_FALSE@ source='$<' object='$@' libtool=no @AMDEPBACKSLASH@ +@AMDEP_TRUE@@am__fastdepCXX_FALSE@ DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@ +@am__fastdepCXX_FALSE@ $(CXXCOMPILE) -c -o $@ `$(CYGPATH_W) '$<'` + +.cpp.lo: +@am__fastdepCXX_TRUE@ if $(LTCXXCOMPILE) -MT $@ -MD -MP -MF "$(DEPDIR)/$*.Tpo" -c -o $@ $<; \ +@am__fastdepCXX_TRUE@ then mv -f "$(DEPDIR)/$*.Tpo" "$(DEPDIR)/$*.Plo"; else rm -f "$(DEPDIR)/$*.Tpo"; exit 1; fi +@AMDEP_TRUE@@am__fastdepCXX_FALSE@ source='$<' object='$@' libtool=yes @AMDEPBACKSLASH@ +@AMDEP_TRUE@@am__fastdepCXX_FALSE@ DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@ +@am__fastdepCXX_FALSE@ $(LTCXXCOMPILE) -c -o $@ $< + +mostlyclean-libtool: + -rm -f *.lo + +clean-libtool: + -rm -rf .libs _libs + +distclean-libtool: + -rm -f libtool +uninstall-info-am: + +ID: $(HEADERS) $(SOURCES) $(LISP) $(TAGS_FILES) + list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \ + unique=`for i in $$list; do \ + if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \ + done | \ + $(AWK) ' { files[$$0] = 1; } \ + END { for (i in files) print i; }'`; \ + mkid -fID $$unique +tags: TAGS + +TAGS: $(HEADERS) $(SOURCES) $(TAGS_DEPENDENCIES) \ + $(TAGS_FILES) $(LISP) + tags=; \ + here=`pwd`; \ + list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \ + unique=`for i in $$list; do \ + if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \ + done | \ + $(AWK) ' { files[$$0] = 1; } \ + END { for (i in files) print i; }'`; \ + if test -z "$(ETAGS_ARGS)$$tags$$unique"; then :; else \ + test -n "$$unique" || unique=$$empty_fix; \ + $(ETAGS) $(ETAGSFLAGS) $(AM_ETAGSFLAGS) $(ETAGS_ARGS) \ + $$tags $$unique; \ + fi +ctags: CTAGS +CTAGS: $(HEADERS) $(SOURCES) $(TAGS_DEPENDENCIES) \ + $(TAGS_FILES) $(LISP) + tags=; \ + here=`pwd`; \ + list='$(SOURCES) $(HEADERS) $(LISP) $(TAGS_FILES)'; \ + unique=`for i in $$list; do \ + if test -f "$$i"; then echo $$i; else echo $(srcdir)/$$i; fi; \ + done | \ + $(AWK) ' { files[$$0] = 1; } \ + END { for (i in files) print i; }'`; \ + test -z "$(CTAGS_ARGS)$$tags$$unique" \ + || $(CTAGS) $(CTAGSFLAGS) $(AM_CTAGSFLAGS) $(CTAGS_ARGS) \ + $$tags $$unique + +GTAGS: + here=`$(am__cd) $(top_builddir) && pwd` \ + && cd $(top_srcdir) \ + && gtags -i $(GTAGS_ARGS) $$here + +distclean-tags: + -rm -f TAGS ID GTAGS GRTAGS GSYMS GPATH tags + +distdir: $(DISTFILES) + @srcdirstrip=`echo "$(srcdir)" | sed 's|.|.|g'`; \ + topsrcdirstrip=`echo "$(top_srcdir)" | sed 's|.|.|g'`; \ + list='$(DISTFILES)'; for file in $$list; do \ + case $$file in \ + $(srcdir)/*) file=`echo "$$file" | sed "s|^$$srcdirstrip/||"`;; \ + $(top_srcdir)/*) file=`echo "$$file" | sed "s|^$$topsrcdirstrip/|$(top_builddir)/|"`;; \ + esac; \ + if test -f $$file || test -d $$file; then d=.; else d=$(srcdir); fi; \ + dir=`echo "$$file" | sed -e 's,/[^/]*$$,,'`; \ + if test "$$dir" != "$$file" && test "$$dir" != "."; then \ + dir="/$$dir"; \ + $(mkdir_p) "$(distdir)$$dir"; \ + else \ + dir=''; \ + fi; \ + if test -d $$d/$$file; then \ + if test -d $(srcdir)/$$file && test $$d != $(srcdir); then \ + cp -pR $(srcdir)/$$file $(distdir)$$dir || exit 1; \ + fi; \ + cp -pR $$d/$$file $(distdir)$$dir || exit 1; \ + else \ + test -f $(distdir)/$$file \ + || cp -p $$d/$$file $(distdir)/$$file \ + || exit 1; \ + fi; \ + done +check-am: all-am +check: $(BUILT_SOURCES) + $(MAKE) $(AM_MAKEFLAGS) check-am +all-am: Makefile $(LTLIBRARIES) +installdirs: +install: $(BUILT_SOURCES) + $(MAKE) $(AM_MAKEFLAGS) install-am +install-exec: install-exec-am +install-data: install-data-am +uninstall: uninstall-am + +install-am: all-am + @$(MAKE) $(AM_MAKEFLAGS) install-exec-am install-data-am + +installcheck: installcheck-am +install-strip: + $(MAKE) $(AM_MAKEFLAGS) INSTALL_PROGRAM="$(INSTALL_STRIP_PROGRAM)" \ + install_sh_PROGRAM="$(INSTALL_STRIP_PROGRAM)" INSTALL_STRIP_FLAG=-s \ + `test -z '$(STRIP)' || \ + echo "INSTALL_PROGRAM_ENV=STRIPPROG='$(STRIP)'"` install +mostlyclean-generic: + +clean-generic: + +distclean-generic: + -test -z "$(CONFIG_CLEAN_FILES)" || rm -f $(CONFIG_CLEAN_FILES) + +maintainer-clean-generic: + @echo "This command is intended for maintainers to use" + @echo "it deletes files that may require special tools to rebuild." + -test -z "$(BUILT_SOURCES)" || rm -f $(BUILT_SOURCES) +clean: clean-am + +clean-am: clean-generic clean-libtool clean-noinstLTLIBRARIES \ + mostlyclean-am + +distclean: distclean-am + -rm -rf ./$(DEPDIR) + -rm -f Makefile +distclean-am: clean-am distclean-compile distclean-generic \ + distclean-libtool distclean-tags + +dvi: dvi-am + +dvi-am: + +html: html-am + +info: info-am + +info-am: + +install-data-am: + +install-exec-am: + +install-info: install-info-am + +install-man: + +installcheck-am: + +maintainer-clean: maintainer-clean-am + -rm -rf ./$(DEPDIR) + -rm -f Makefile +maintainer-clean-am: distclean-am maintainer-clean-generic + +mostlyclean: mostlyclean-am + +mostlyclean-am: mostlyclean-compile mostlyclean-generic \ + mostlyclean-libtool + +pdf: pdf-am + +pdf-am: + +ps: ps-am + +ps-am: + +uninstall-am: uninstall-info-am + +.PHONY: CTAGS GTAGS all all-am check check-am clean clean-generic \ + clean-libtool clean-noinstLTLIBRARIES ctags distclean \ + distclean-compile distclean-generic distclean-libtool \ + distclean-tags distdir dvi dvi-am html html-am info info-am \ + install install-am install-data install-data-am install-exec \ + install-exec-am install-info install-info-am install-man \ + install-strip installcheck installcheck-am installdirs \ + maintainer-clean maintainer-clean-generic mostlyclean \ + mostlyclean-compile mostlyclean-generic mostlyclean-libtool \ + pdf pdf-am ps ps-am tags uninstall uninstall-am \ + uninstall-info-am + + +AntlrCvcLexer.hpp: CvcLexer.g +AntlrCvcLexer.cpp: CvcLexer.g + $(ANTLR) @srcdir@/CvcLexer.g + +AntlrCvcParser.hpp: CvcParser.g AntlrCvcLexer.cpp +AntlrCvcParser.cpp: CvcParser.g AntlrCvcLexer.cpp + $(ANTLR) @srcdir@/CvcParser.g +# Tell versions [3.59,3.63) of GNU make to not export all variables. +# Otherwise a system limit (for SysV at least) may be exceeded. +.NOEXPORT: diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index b9091668e..65a5d11c1 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -20,6 +20,8 @@ #include "parser/antlr_parser.h" #include "parser/smt/AntlrSmtParser.hpp" #include "parser/smt/AntlrSmtLexer.hpp" +#include "parser/cvc/AntlrCvcParser.hpp" +#include "parser/cvc/AntlrCvcLexer.hpp" using namespace std; @@ -27,21 +29,25 @@ namespace CVC4 { namespace parser { Parser::Parser(ExprManager* em) : - d_expr_manager(em) { + d_expr_manager(em), d_done(false) { } -bool SmtParser::done() const { +void Parser::setDone(bool done) { + d_done = done; +} + +bool Parser::done() const { return d_done; } Command* SmtParser::parseNextCommand() throw (ParserException) { Command* cmd = 0; - if(!d_done) { + if(!done()) { try { cmd = d_antlr_parser->benchmark(); - d_done = true; + setDone(); } catch(antlr::ANTLRException& e) { - d_done = true; + setDone(); throw ParserException(e.toString()); } } @@ -50,11 +56,11 @@ Command* SmtParser::parseNextCommand() throw (ParserException) { Expr SmtParser::parseNextExpression() throw (ParserException) { Expr result; - if (!d_done) { + if (!done()) { try { result = d_antlr_parser->an_formula(); } catch(antlr::ANTLRException& e) { - d_done = true; + setDone(); throw ParserException(e.toString()); } } @@ -67,14 +73,14 @@ SmtParser::~SmtParser() { } SmtParser::SmtParser(ExprManager* em, istream& input) : - Parser(em), d_done(false) { + Parser(em) { d_antlr_lexer = new AntlrSmtLexer(input); d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer); d_antlr_parser->setExpressionManager(d_expr_manager); } SmtParser::SmtParser(ExprManager*em, const char* file_name) : - Parser(em), d_done(false), d_input(file_name) { + Parser(em), d_input(file_name) { d_antlr_lexer = new AntlrSmtLexer(d_input); d_antlr_lexer->setFilename(file_name); d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer); @@ -82,6 +88,58 @@ SmtParser::SmtParser(ExprManager*em, const char* file_name) : d_antlr_parser->setFilename(file_name); } +Command* CvcParser::parseNextCommand() throw (ParserException) { + Command* cmd = 0; + if(!done()) { + try { + cmd = d_antlr_parser->command(); + if (cmd == 0) { + setDone(); + cmd = new EmptyCommand("EOF"); + } + } catch(antlr::ANTLRException& e) { + setDone(); + throw ParserException(e.toString()); + } + } + return cmd; +} + +Expr CvcParser::parseNextExpression() throw (ParserException) { + Expr result; + if (!done()) { + try { + result = d_antlr_parser->formula(); + } catch(antlr::ANTLRException& e) { + setDone(); + throw ParserException(e.toString()); + } + } + return result; +} + +CvcParser::~CvcParser() { + delete d_antlr_parser; + delete d_antlr_lexer; +} + +CvcParser::CvcParser(ExprManager* em, istream& input) : + Parser(em) { + d_antlr_lexer = new AntlrCvcLexer(input); + d_antlr_parser = new AntlrCvcParser(*d_antlr_lexer); + d_antlr_parser->setExpressionManager(d_expr_manager); +} + +CvcParser::CvcParser(ExprManager*em, const char* file_name) : + Parser(em), d_input(file_name) { + d_antlr_lexer = new AntlrCvcLexer(d_input); + d_antlr_lexer->setFilename(file_name); + d_antlr_parser = new AntlrCvcParser(*d_antlr_lexer); + d_antlr_parser->setExpressionManager(d_expr_manager); + d_antlr_parser->setFilename(file_name); +} + + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/parser.h b/src/parser/parser.h index d0ef3776a..dbdca4af8 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -30,6 +30,8 @@ namespace parser { class AntlrSmtLexer; class AntlrSmtParser; +class AntlrCvcLexer; +class AntlrCvcParser; /** * The parser. @@ -49,7 +51,6 @@ public: */ virtual ~Parser() { } - ; /** * Parse the next command of the input @@ -64,13 +65,19 @@ public: /** * Check if we are done -- either the end of input has been reached. */ - virtual bool done() const = 0; + bool done() const; protected: + /** Sets the done flag */ + void setDone(bool done = true); + /** Expression manager the parser will be using */ ExprManager* d_expr_manager; + /** Are we done */ + bool d_done; + }; // end of class Parser class CVC4_PUBLIC SmtParser : public Parser { @@ -112,12 +119,6 @@ public: */ Expr parseNextExpression() throw (ParserException); - /** - * Check if we are done with the stream, i.e. EOF has been reached, or the - * whole SMT benchmark has been parsed. - */ - bool done() const; - protected: /** The ANTLR smt lexer */ @@ -126,13 +127,62 @@ protected: /** The ANTLR smt parser */ AntlrSmtParser* d_antlr_parser; - /** Are we done */ - bool d_done; + /** The file stream we might be using */ + std::ifstream d_input; +}; + +class CVC4_PUBLIC CvcParser : public Parser { + +public: + + /** + * Construct the parser that uses the given expression manager and parses + * from the given input stream. + * @param em the expression manager to use + * @param input the input stream to parse + */ + CvcParser(ExprManager* em, std::istream& input); + + /** + * Construct the parser that uses the given expression manager and parses + * from the file. + * @param em the expression manager to use + * @param file_name the file to parse + */ + CvcParser(ExprManager* em, const char* file_name); + + /** + * Destructor. + */ + ~CvcParser(); + + /** + * Parses the next command. By default, the SMTLIB parser produces one + * CommandSequence command. If parsing is successful, we should be done + * after the first call to this command. + * @return the CommandSequence command that includes the whole benchmark + */ + Command* parseNextCommand() throw (ParserException); + + /** + * Parses the next complete expression of the stream. + * @return the expression parsed + */ + Expr parseNextExpression() throw (ParserException); + +protected: + + /** The ANTLR smt lexer */ + AntlrCvcLexer* d_antlr_lexer; + + /** The ANTLR smt parser */ + AntlrCvcParser* d_antlr_parser; /** The file stream we might be using */ std::ifstream d_input; }; + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/util/assert.h b/src/util/assert.h index 4a164716c..8fd970c6c 100644 --- a/src/util/assert.h +++ b/src/util/assert.h @@ -57,17 +57,17 @@ public: inline void AssertImpl(const char* info, bool cond, std::string msg) { if(EXPECT_FALSE( ! cond )) - throw new AssertionException(std::string(info) + "\n" + msg); + throw AssertionException(std::string(info) + "\n" + msg); } inline void AssertImpl(const char* info, bool cond, const char* msg) { if(EXPECT_FALSE( ! cond )) - throw new AssertionException(std::string(info) + "\n" + msg); + throw AssertionException(std::string(info) + "\n" + msg); } inline void AssertImpl(const char* info, bool cond) { if(EXPECT_FALSE( ! cond )) - throw new AssertionException(info); + throw AssertionException(info); } #ifdef __GNUC__ @@ -77,15 +77,15 @@ inline void UnreachableImpl(const char* info) __attribute__ ((noreturn)); #endif /* __GNUC__ */ inline void UnreachableImpl(const char* info, std::string msg) { - throw new UnreachableCodeException(std::string(info) + "\n" + msg); + throw UnreachableCodeException(std::string(info) + "\n" + msg); } inline void UnreachableImpl(const char* info, const char* msg) { - throw new UnreachableCodeException(std::string(info) + "\n" + msg); + throw UnreachableCodeException(std::string(info) + "\n" + msg); } inline void UnreachableImpl(const char* info) { - throw new UnreachableCodeException(info); + throw UnreachableCodeException(info); } #ifdef __GNUC__ @@ -95,15 +95,15 @@ inline void UnhandledImpl(const char* info) __attribute__ ((noreturn)); #endif /* __GNUC__ */ inline void UnhandledImpl(const char* info, std::string msg) { - throw new UnhandledCaseException(std::string(info) + "\n" + msg); + throw UnhandledCaseException(std::string(info) + "\n" + msg); } inline void UnhandledImpl(const char* info, const char* msg) { - throw new UnhandledCaseException(std::string(info) + "\n" + msg); + throw UnhandledCaseException(std::string(info) + "\n" + msg); } inline void UnhandledImpl(const char* info) { - throw new UnhandledCaseException(info); + throw UnhandledCaseException(info); } }/* CVC4 namespace */ diff --git a/src/util/command.cpp b/src/util/command.cpp index e38695b46..961104585 100644 --- a/src/util/command.cpp +++ b/src/util/command.cpp @@ -19,7 +19,8 @@ ostream& operator<<(ostream& out, const CVC4::Command& c) { namespace CVC4 { -EmptyCommand::EmptyCommand() { +EmptyCommand::EmptyCommand(std::string name) : + d_name(name) { } void EmptyCommand::invoke(SmtEngine* smt_engine) { @@ -77,7 +78,7 @@ void CommandSequence::addCommand(Command* cmd) { using namespace std; void EmptyCommand::toString(ostream& out) const { - out << "EmptyCommand"; + out << "EmptyCommand(" << d_name << ")"; } void AssertCommand::toString(ostream& out) const { diff --git a/src/util/command.h b/src/util/command.h index ce137896a..3d738ba45 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -38,9 +38,11 @@ public: class CVC4_PUBLIC EmptyCommand : public Command { public: - EmptyCommand(); + EmptyCommand(std::string name = ""); void invoke(CVC4::SmtEngine* smt_engine); void toString(std::ostream& out) const; +private: + std::string d_name; };/* class EmptyCommand */ |