<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"/>
</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>
-#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
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
src/util/Makefile
src/context/Makefile
src/parser/Makefile
+ src/parser/cvc/Makefile
src/parser/smt/Makefile
src/theory/Makefile
test/Makefile
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();
}
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 \
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) {
}
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) {
}
}
-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);
}
*/
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
*/
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.
* 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;
--- /dev/null
+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
--- /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
+ 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
--- /dev/null
+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
--- /dev/null
+# 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:
#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;
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());
}
}
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());
}
}
}
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);
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 */
class AntlrSmtLexer;
class AntlrSmtParser;
+class AntlrCvcLexer;
+class AntlrCvcParser;
/**
* The parser.
*/
virtual ~Parser() {
}
- ;
/**
* Parse the next command of the input
/**
* 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 {
*/
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 */
/** 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 */
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__
#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__
#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 */
namespace CVC4 {
-EmptyCommand::EmptyCommand() {
+EmptyCommand::EmptyCommand(std::string name) :
+ d_name(name) {
}
void EmptyCommand::invoke(SmtEngine* smt_engine) {
using namespace std;
void EmptyCommand::toString(ostream& out) const {
- out << "EmptyCommand";
+ out << "EmptyCommand(" << d_name << ")";
}
void AssertCommand::toString(ostream& out) const {
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 */
projects / cvc5.git / commitdiff