diff options
31 files changed, 497 insertions, 1772 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" 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="true" 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"/> @@ -146,6 +146,8 @@ </storageModule> <storageModule moduleId="org.eclipse.cdt.core.externalSettings"/> <storageModule moduleId="org.eclipse.cdt.internal.ui.text.commentOwnerProjectMappings"/> +<storageModule moduleId="org.eclipse.cdt.core.language.mapping"/> +<storageModule moduleId="org.eclipse.cdt.make.core.buildtargets"/> </cconfiguration> </storageModule> <storageModule moduleId="cdtBuildSystem" version="4.0.0"> @@ -31,7 +31,7 @@ </dictionary> <dictionary> <key>org.eclipse.cdt.make.core.buildLocation</key> - <value>${workspace_loc:/cvc4/}</value> + <value>${workspace_loc/cvc4/}</value> </dictionary> <dictionary> <key>org.eclipse.cdt.make.core.cleanBuildTarget</key> diff --git a/configure.ac b/configure.ac index f4320aeb4..e6ad11733 100644 --- a/configure.ac +++ b/configure.ac @@ -257,17 +257,7 @@ AM_PROG_LEX AC_PROG_YACC # Check for ANTLR runantlr script (defined in config/antlr.m4) -AC_ARG_ENABLE(antlr, AS_HELP_STRING([--enable-antlr],[use Dejan's ANTLR parsers])) -AC_MSG_CHECKING([whether you want to use the ANTLR parsers]) -if test -z "${enable_antlr+set}"; then - enable_antlr=no -fi -AC_MSG_RESULT([$enable_antlr]) -AM_CONDITIONAL(USE_ANTLR, test "$enable_antlr" = yes) -if test "$enable_antlr" = yes; then - AC_PROG_ANTLR - AC_DEFINE(ANTLR_PARSERS, [], [whether we're using ANTLR parsers]) -fi +AC_PROG_ANTLR AC_CHECK_PROG(DOXYGEN, doxygen, doxygen, []) if test -z "$DOXYGEN"; then @@ -310,9 +300,8 @@ fi # Checks for libraries. AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmplib.org/])]) # Check for antlr C++ runtime (defined in config/antlr.m4) -if test "$enable_antlr" = yes; then - AC_LIB_ANTLR -fi +AC_LIB_ANTLR + # Checks for header files. AC_CHECK_HEADERS([getopt.h unistd.h]) @@ -398,7 +387,7 @@ CPPFLAGS : $CPPFLAGS CXXFLAGS : $CXXFLAGS LDFLAGS : $LDFLAGS -Using ANTLR parsers : $enable_antlr + Library releases : $CVC4_LIBRARY_RELEASE_CODE libcvc4 version : $CVC4_LIBRARY_VERSION libcvc4parser version: $CVC4_PARSER_LIBRARY_VERSION diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index 2e3d7a7e2..e88189bcc 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -18,7 +18,18 @@ using namespace CVC4::expr; namespace CVC4 { -Expr Expr::s_null(0); +ExprValue ExprValue::s_null; + +Expr Expr::s_null(&ExprValue::s_null); + +bool Expr::isNull() const { + return d_ev == &ExprValue::s_null; +} + +Expr::Expr() : + d_ev(&ExprValue::s_null) { + // No refcount needed +} Expr::Expr(ExprValue* ev) : d_ev(ev) { diff --git a/src/expr/expr.h b/src/expr/expr.h index 5a11e0fbd..0fcb5ea6a 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -60,6 +60,10 @@ class CVC4_PUBLIC Expr { friend class ExprManager; public: + + /** Default constructor, makes a null expression. */ + CVC4_PUBLIC Expr(); + CVC4_PUBLIC Expr(const Expr&); /** Destructor. Decrements the reference count and, if zero, @@ -103,6 +107,9 @@ public: inline iterator end() const; void toString(std::ostream&) const; + + bool isNull() const; + };/* class Expr */ }/* CVC4 namespace */ diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp index e24bb88b1..c511c580a 100644 --- a/src/expr/expr_value.cpp +++ b/src/expr/expr_value.cpp @@ -18,7 +18,11 @@ namespace CVC4 { -size_t ExprValue::next_id = 0; +ExprValue::ExprValue() : + d_id(0), d_rc(MAX_RC), d_kind(NULL_EXPR), d_nchildren(0) { +} + +size_t ExprValue::next_id = 1; uint64_t ExprValue::hash() const { uint64_t hash = d_kind; diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h index decd57045..6df7ad76f 100644 --- a/src/expr/expr_value.h +++ b/src/expr/expr_value.h @@ -34,13 +34,17 @@ namespace expr { * This is an ExprValue. */ class ExprValue { + + /** A convenient null-valued expression value */ + static ExprValue s_null; + /** Maximum reference count possible. Used for sticky * reference-counting. Should be (1 << num_bits(d_rc)) - 1 */ static const unsigned MAX_RC = 255; // this header fits into one 64-bit word - /** The ID */ + /** The ID (0 is reserved for the null value) */ unsigned d_id : 32; /** The expression's reference count. @see cvc4::Expr. */ @@ -65,6 +69,9 @@ class ExprValue { static size_t next_id; + /** Private default constructor for the null value. */ + ExprValue(); + public: /** Hash this expression. * @return the hash value of this expression. */ diff --git a/src/expr/kind.h b/src/expr/kind.h index 790fd644d..49321b47f 100644 --- a/src/expr/kind.h +++ b/src/expr/kind.h @@ -23,6 +23,8 @@ namespace CVC4 { enum Kind { /* undefined */ UNDEFINED_KIND = -1, + /** Null Kind */ + NULL_EXPR, /* built-ins */ EQUAL, @@ -57,6 +59,7 @@ inline std::ostream& operator<<(std::ostream& out, const CVC4::Kind& k) { switch(k) { case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break; + case NULL_EXPR: out << "NULL"; break; case EQUAL: out << "EQUAL"; break; case ITE: out << "ITE"; break; case SKOLEM: out << "SKOLEM"; break; diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index f60dd6e24..2daead11b 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -25,11 +25,9 @@ #include "util/exception.h" #include "usage.h" #include "about.h" -#include "parser/language.h" using namespace std; using namespace CVC4; -using namespace CVC4::parser; namespace CVC4 { namespace main { @@ -58,7 +56,7 @@ static struct option cmdlineOptions[] = { { "stats" , no_argument , NULL, STATS } }; -int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(Exception*) { +int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionException) { const char *progName = argv[0]; int c; @@ -89,19 +87,19 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(Exception*) { break; case 'L': - if(!strcmp(argv[optind], "cvc4") || !strcmp(argv[optind], "pl")) { - opts->lang = PL; + if(!strcmp(optarg, "cvc4") || !strcmp(optarg, "pl")) { + opts->lang = Options::LANG_CVC4; break; - } else if(!strcmp(argv[optind], "smtlib") || !strcmp(argv[optind], "smt")) { - opts->lang = SMTLIB; + } else if(!strcmp(optarg, "smtlib") || !strcmp(optarg, "smt")) { + opts->lang = Options::LANG_SMTLIB; break; - } else if(!strcmp(argv[optind], "auto")) { - opts->lang = AUTO; + } else if(!strcmp(optarg, "auto")) { + opts->lang = Options::LANG_AUTO; break; } - if(strcmp(argv[optind], "help")) - throw new OptionException(string("unknown language for --lang: `") + argv[optind] + "'. Try --lang help."); + if(strcmp(optarg, "help")) + throw OptionException(string("unknown language for --lang: `") + argv[optind] + "'. Try --lang help."); fputs(lang_help, stdout); exit(1); @@ -114,17 +112,17 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(Exception*) { // silences CVC4 (except "sat" or "unsat" or "unknown", forces smtlib input) opts->smtcomp_mode = true; opts->verbosity = -1; - opts->lang = SMTLIB; + opts->lang = Options::LANG_SMTLIB; break; case '?': - throw new OptionException(string("can't understand option: `") + argv[optind] + "'"); + throw OptionException(string("can't understand option: `") + argv[optind] + "'"); case ':': - throw new OptionException(string("option `") + argv[optind] + "' missing its required argument"); + throw OptionException(string("option `") + argv[optind] + "' missing its required argument"); default: - throw new OptionException(string("can't understand option: `") + argv[optind] + "'"); + throw OptionException(string("can't understand option: `") + argv[optind] + "'"); } } diff --git a/src/main/main.cpp b/src/main/main.cpp index 323a989c8..b7833e3ca 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -12,25 +12,15 @@ #include <iostream> #include <fstream> -#include <cstdio> #include <cstdlib> -#include <cerrno> #include <new> -#include <exception> -#include <unistd.h> -#include <string.h> -#include <stdint.h> -#include <time.h> #include "config.h" #include "main.h" #include "usage.h" #include "parser/parser.h" #include "expr/expr_manager.h" -#include "expr/expr.h" -#include "expr/kind.h" #include "smt/smt_engine.h" -#include "parser/language.h" #include "util/command.h" using namespace std; @@ -39,74 +29,79 @@ using namespace CVC4::parser; using namespace CVC4::main; int main(int argc, char *argv[]) { - struct Options opts; + + struct Options options; try { + + // Initialize the signal handlers cvc4_init(); - int firstArgIndex = parseOptions(argc, argv, &opts); + // Parse the options + int firstArgIndex = parseOptions(argc, argv, &options); - istream *in; - ifstream infile; - Language lang = PL; + // If in competition mode, we flush the stdout immediately + if(options.smtcomp_mode) + cout << unitbuf; - if(firstArgIndex >= argc) { - in = &cin; - } else if(argc > firstArgIndex + 1) { + // We only accept one input file + if(argc > firstArgIndex + 1) throw new Exception("Too many input files specified."); - } else { - in = &infile; - if(strlen(argv[firstArgIndex]) >= 4 && - !strcmp(argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4, ".smt")) - lang = SMTLIB; - infile.open(argv[firstArgIndex], ifstream::in); - - if(!infile) { - throw new Exception(string("Could not open input file `") + - argv[firstArgIndex] + "' for reading: " + - strerror(errno)); - } + + // Create the expression manager + ExprManager exprMgr; + // Create the SmtEngine + SmtEngine smt(&exprMgr, &options); + + // If no file supplied we read from standard input + bool inputFromStdin = firstArgIndex >= argc; + + // Create the parser + Parser* parser; + switch(options.lang) { + case Options::LANG_SMTLIB: + if(inputFromStdin) + parser = new SmtParser(&exprMgr, cin); + else + parser = new SmtParser(&exprMgr, argv[firstArgIndex]); + break; + default: + cerr << "Language" << options.lang << "not supported yet." << endl; + abort(); } - ExprManager *exprMgr = new ExprManager; - SmtEngine smt(exprMgr, &opts); - Parser parser(&smt, exprMgr, lang, *in, &opts); - while(!parser.done()) { - Command *cmd = parser.parseNextCommand(opts.verbosity > 1); - if(opts.verbosity > 0) { - cout << "invoking cmd: "; - cout << cmd << endl; - } + // Parse the and execute commands until we are done + while(!parser->done()) { + // Parse the next command + Command *cmd = parser->parseNextCommand(); if(cmd) { - if(opts.verbosity >= 0) - cout << cmd->invoke(&smt) << endl; + if(options.verbosity > 0) + cout << "Invoking: " << *cmd << endl; + cmd->invoke(&smt); delete cmd; } } - } catch(CVC4::main::OptionException* e) { - if(opts.smtcomp_mode) { - printf("unknown"); - fflush(stdout); - } - fprintf(stderr, "CVC4 Error:\n%s\n\n", e->toString().c_str()); - printf(usage, opts.binary_name.c_str()); + + // Remove the parser + delete parser; + } catch(OptionException& e) { + if(options.smtcomp_mode) + cout << "unknown" << endl; + cerr << "CVC4 Error:" << endl << e << endl; + printf(usage, options.binary_name.c_str()); abort(); - } catch(CVC4::Exception* e) { - if(opts.smtcomp_mode) { - printf("unknown"); - fflush(stdout); - } - fprintf(stderr, "CVC4 Error:\n%s\n", e->toString().c_str()); + } catch(CVC4::Exception& e) { + if(options.smtcomp_mode) + cout << "unknown" << endl; + cerr << "CVC4 Error:" << endl << e << endl; abort(); } catch(bad_alloc) { - if(opts.smtcomp_mode) { - printf("unknown"); - fflush(stdout); - } - fprintf(stderr, "CVC4 ran out of memory.\n"); + if(options.smtcomp_mode) + cout << "unknown" << endl; + cerr << "CVC4 ran out of memory." << endl; abort(); } catch(...) { - fprintf(stderr, "CVC4 threw an exception of unknown type.\n"); + cerr << "CVC4 threw an exception of unknown type." << endl; abort(); } diff --git a/src/main/main.h b/src/main/main.h index 5e0c68053..60817d976 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -28,7 +28,7 @@ public: OptionException(const std::string& s) throw() : CVC4::Exception("Error in option parsing: " + s) {} };/* class OptionException */ -int parseOptions(int argc, char** argv, CVC4::Options*) throw(CVC4::Exception*); +int parseOptions(int argc, char** argv, CVC4::Options*) throw(OptionException); void cvc4_init() throw(); }/* CVC4::main namespace */ diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 7e3cee751..3c2bfc8ab 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -15,62 +15,22 @@ LIBCVC4PARSER_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@ LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@ -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_CVC4PARSERLIB -if USE_ANTLR - SUBDIRS = smt - INCLUDES += $(ANTLR_INCLUDES) -endif +SUBDIRS = smt -lib_LTLIBRARIES = libcvc4parser.la - -libcvc4parser_la_LDFLAGS = -version-info $(LIBCVC4PARSER_VERSION) -release $(LIBCVC4PARSER_RELEASE) - -if USE_ANTLR - libcvc4parser_la_LDFLAGS += $(ANTLR_LDFLAGS) -endif +nobase_lib_LTLIBRARIES = libcvc4parser.la +libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) libcvc4parser_la_LIBADD = \ - ../libcvc4.la + @builddir@/smt/libparsersmt.la libcvc4parser_la_SOURCES = \ + parser.h \ parser.cpp \ - parser_state.cpp \ - symbol_table.cpp \ - pl_scanner.lpp \ - pl.ypp \ - smtlib_scanner.lpp \ - smtlib.ypp - -if USE_ANTLR - libcvc4parser_la_SOURCES += \ - antlr_parser.cpp \ - antlr_parser.h -endif USE_ANTLR - -BUILT_SOURCES = \ - pl_scanner.cpp \ - pl.cpp \ - pl.hpp \ - smtlib_scanner.cpp \ - smtlib.cpp \ - smtlib.hpp - -# produce headers too -AM_YFLAGS = -d - -pl_scanner.cpp: pl_scanner.lpp - $(LEX) $(AM_LFLAGS) $(LFLAGS) -P PL -o $@ $< -smtlib_scanner.cpp: smtlib_scanner.lpp - $(LEX) $(AM_LFLAGS) $(LFLAGS) -P smtlib -o $@ $< - -pl_scanner.o: pl.hpp -pl.cpp: pl.ypp - $(YACC) $(AM_YFLAGS) $(YFLAGS) -p PL -o $@ $< - + symbol_table.h \ + antlr_parser.h \ + antlr_parser.cpp -smtlib_scanner.o: smtlib.hpp -smtlib.cpp: smtlib.ypp - $(YACC) $(AM_YFLAGS) $(YFLAGS) -p smtlib -o $@ $< diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index c1cd85731..c4e6eef19 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -5,6 +5,8 @@ * Author: dejan */ +#include <iostream> + #include "antlr_parser.h" #include "expr/expr_manager.h" @@ -24,7 +26,8 @@ ostream& operator <<(ostream& out, AntlrParser::BenchmarkStatus status) { out << "unknown"; break; default: - CVC4::UnhandledImpl("Unhandled ostream case for AntlrParser::BenchmarkStatus"); + CVC4::UnhandledImpl( + "Unhandled ostream case for AntlrParser::BenchmarkStatus"); } return out; } @@ -42,8 +45,7 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) : } Expr AntlrParser::getVariable(std::string var_name) { - cout << "getVariable(" << var_name << ")" << endl; - return d_expr_manager->mkExpr(VARIABLE); + return d_var_symbol_table.getObject(var_name); } Expr AntlrParser::getTrueExpr() const { @@ -55,21 +57,37 @@ Expr AntlrParser::getFalseExpr() const { } 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; + 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::setBenchmarkStatus(BenchmarkStatus status) { - cout << "setBenchmarkStatus()" << endl; d_benchmark_status = status; } void AntlrParser::addExtraSorts(std::vector<std::string>& extra_sorts) { - cout << "addExtraSorts()" << endl; +} + +void AntlrParser::setExpressionManager(ExprManager* em) { + d_expr_manager = em; +} + +bool AntlrParser::isDeclared(string name, SymbolType type) { + switch(type) { + case SYM_VARIABLE: + return d_var_symbol_table.isBound(name); + default: + Unhandled("Unhandled symbol 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()); } diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index 967721d26..31310da30 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -13,10 +13,13 @@ #include <iostream> #include <antlr/LLkParser.hpp> +#include <antlr/SemanticException.hpp> + #include "expr/expr.h" #include "expr/expr_manager.h" #include "util/command.h" #include "util/assert.h" +#include "parser/symbol_table.h" namespace CVC4 { @@ -42,6 +45,12 @@ public: SMT_UNKNOWN }; + /** + * Set's the expression manager to use when creating/managing expression. + * @param expr_manager the expression manager + */ + void setExpressionManager(ExprManager* expr_manager); + protected: /** @@ -72,6 +81,11 @@ protected: AntlrParser(antlr::TokenStream& lexer, int k); /** + * Renames the antlr semantic expression to a given message. + */ + void rethrow(antlr::SemanticException& e, std::string msg) throw (antlr::SemanticException); + + /** * Returns a variable, given a name and a type. * @param var_name the name of the variable * @return the variable expression @@ -79,6 +93,24 @@ protected: Expr getVariable(std::string var_name); /** + * Types of symbols. + */ + enum SymbolType { + /** Variables */ + SYM_VARIABLE, + /** Predicates */ + SYM_PREDICATE, + /** Functions */ + SYM_FUNCTION + }; + + /** + * Checks if the variable has been declared. + * @param the variable name + */ + bool isDeclared(std::string var_name, SymbolType type = SYM_VARIABLE); + + /** * Returns the true expression. * @return the true expression */ @@ -122,17 +154,6 @@ protected: */ 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 */ @@ -140,12 +161,17 @@ private: /** The expression manager */ ExprManager* d_expr_manager; + + /** The symbol table lookup */ + SymbolTable<Expr> d_var_symbol_table; }; -std::ostream& operator << (std::ostream& out, AntlrParser::BenchmarkStatus status); +} } +namespace std { +ostream& operator<<(ostream& out, CVC4::parser::AntlrParser::BenchmarkStatus status); } #endif /* CVC4_PARSER_H_ */ diff --git a/src/parser/language.h b/src/parser/language.h deleted file mode 100644 index 7ea6547cd..000000000 --- a/src/parser/language.h +++ /dev/null @@ -1,31 +0,0 @@ -/********************* -*- C++ -*- */ -/** language.h - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** Input languages. - **/ - -#ifndef __CVC4__PARSER__LANGUAGE_H -#define __CVC4__PARSER__LANGUAGE_H - -#include "util/exception.h" -#include "parser/language.h" - -namespace CVC4 { -namespace parser { - -enum Language { - AUTO = 0, - PL, - SMTLIB, -};/* enum Language */ - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__PARSER__LANGUAGE_H */ diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index cd03f21f2..b9091668e 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -11,49 +11,75 @@ **/ #include <iostream> +#include <fstream> -#include "cvc4_config.h" -#include "parser/parser.h" +#include "parser.h" #include "util/command.h" #include "util/assert.h" -#include "parser/parser_state.h" -#include "parser/parser_exception.h" - -int CVC4_PUBLIC smtlibparse(); -int CVC4_PUBLIC PLparse(); -extern "C" int smtlibdebug, PLdebug; +#include "parser_exception.h" +#include "parser/antlr_parser.h" +#include "parser/smt/AntlrSmtParser.hpp" +#include "parser/smt/AntlrSmtLexer.hpp" using namespace std; -using namespace CVC4; namespace CVC4 { namespace parser { -ParserState CVC4_PUBLIC *_global_parser_state = 0; +Parser::Parser(ExprManager* em) : + d_expr_manager(em) { +} -bool Parser::done() const { - return _global_parser_state->done(); +bool SmtParser::done() const { + return d_done; +} + +Command* SmtParser::parseNextCommand() throw (ParserException) { + Command* cmd = 0; + if(!d_done) { + try { + cmd = d_antlr_parser->benchmark(); + d_done = true; + } catch(antlr::ANTLRException& e) { + d_done = true; + throw ParserException(e.toString()); + } + } + return cmd; } -Command* Parser::parseNextCommand(bool verbose) { - switch(d_lang) { - case PL: - PLdebug = verbose; - PLparse(); - cout << "getting command" << endl; - return _global_parser_state->getCommand(); - case SMTLIB: - smtlibdebug = verbose; - smtlibparse(); - return _global_parser_state->getCommand(); - default: - Unhandled(); +Expr SmtParser::parseNextExpression() throw (ParserException) { + Expr result; + if (!d_done) { + try { + result = d_antlr_parser->an_formula(); + } catch(antlr::ANTLRException& e) { + d_done = true; + throw ParserException(e.toString()); + } } - return new EmptyCommand; + return result; +} + +SmtParser::~SmtParser() { + delete d_antlr_parser; + delete d_antlr_lexer; +} + +SmtParser::SmtParser(ExprManager* em, istream& input) : + Parser(em), d_done(false) { + d_antlr_lexer = new AntlrSmtLexer(input); + d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer); + d_antlr_parser->setExpressionManager(d_expr_manager); } -Parser::~Parser() { - //delete d_data; +SmtParser::SmtParser(ExprManager*em, const char* file_name) : + Parser(em), d_done(false), 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->setExpressionManager(d_expr_manager); + d_antlr_parser->setFilename(file_name); } }/* CVC4::parser namespace */ diff --git a/src/parser/parser.h b/src/parser/parser.h index 411e7760c..d0ef3776a 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -15,9 +15,9 @@ #include <string> #include <iostream> - -#include "parser/language.h" -#include "parser/parser_state.h" +#include <fstream> +#include "cvc4_config.h" +#include "parser_exception.h" namespace CVC4 { @@ -25,74 +25,113 @@ namespace CVC4 { class Expr; class Command; class ExprManager; -class SmtEngine; -class Options; namespace parser { -/** - * The global pointer to ParserTemp. Each instance of class Parser sets this pointer - * before any calls to the lexer. We do it this way because flex and bison use global - * vars, and we want each Parser object to appear independent. - */ -extern ParserState CVC4_PUBLIC *_global_parser_state; +class AntlrSmtLexer; +class AntlrSmtParser; /** * The parser. */ class CVC4_PUBLIC Parser { - private: - /** Internal parser state we are keeping */ - //ParserState* d_data; +public: + + /** + * Construct the parser that uses the given expression manager. + * @param em the expression manager. + */ + Parser(ExprManager* em); + + /** + * Destructor. + */ + virtual ~Parser() { + } + ; + + /** + * Parse the next command of the input + */ + virtual Command* parseNextCommand() throw (ParserException) = 0; + + /** + * Parse the next expression of the stream + */ + virtual Expr parseNextExpression() throw (ParserException) = 0; + + /** + * Check if we are done -- either the end of input has been reached. + */ + virtual bool done() const = 0; - /** Initialize the parser */ - void initParser(); +protected: - /** Remove the parser components */ - void deleteParser(); + /** Expression manager the parser will be using */ + ExprManager* d_expr_manager; - Language d_lang; - std::istream &d_in; - Options *d_opts; +}; // end of class Parser - public: +class CVC4_PUBLIC SmtParser : public Parser { + +public: /** - * Constructor for parsing out of a file. + * 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 + */ + SmtParser(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 lang the language syntax to use * @param file_name the file to parse */ - Parser(SmtEngine* smt, ExprManager* em, Language lang, std::istream& in, Options* opts) : - d_lang(lang), d_in(in), d_opts(opts) { - _global_parser_state = new ParserState(smt, em); - _global_parser_state->setInputStream(in); - } + SmtParser(ExprManager* em, const char* file_name); /** * Destructor. */ - ~Parser(); + ~SmtParser(); - /** Parse a command */ - Command* parseNextCommand(bool verbose = false); + /** + * 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); - /** Parse an expression of the stream */ - Expr parseNextExpression(); + /** + * Parses the next complete expression of the stream. + * @return the expression parsed + */ + Expr parseNextExpression() throw (ParserException); - // Check if we are done (end of input has been reached) + /** + * 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; - // The same check can be done by using the class Parser's value as a Boolean - operator bool() const { return done(); } +protected: - /** Prints the location to the output stream */ - void printLocation(std::ostream& out) const; + /** The ANTLR smt lexer */ + AntlrSmtLexer* d_antlr_lexer; - /** Reset any local data */ - void reset(); -}; // end of class Parser + /** 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; +}; }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp deleted file mode 100644 index db64107e1..000000000 --- a/src/parser/parser_state.cpp +++ /dev/null @@ -1,64 +0,0 @@ -/* - * parser_state.cpp - * - * Created on: Nov 20, 2009 - * Author: dejan - */ - -#include "parser_state.h" -#include "parser_exception.h" -#include <sstream> - -using namespace std; - -namespace CVC4 { -namespace parser { - -int ParserState::read(char* buffer, int size) { - if (d_input_stream) { - // Read the characters and count them in result - d_input_stream->read(buffer, size); - return d_input_stream->gcount(); - } else return 0; -} - -int ParserState::parseError(const std::string& s) { - throw new ParserException(s); -} - -string ParserState::getNextUniqueID() { - ostringstream ss; - ss << d_uid++; - return ss.str(); -} - -string ParserState::getCurrentPrompt() const { - return d_prompt; -} - -void ParserState::setPromptMain() { - d_prompt = d_prompt_main; -} - -void ParserState::setPromptNextLine() { - d_prompt = d_prompt_continue; -} - -void ParserState::increaseLineNumber() { - ++d_input_line; - if (d_interactive) { - std::cout << getCurrentPrompt(); - setPromptNextLine(); - } -} - -int ParserState::getLineNumber() const { - return d_input_line; -} - -std::string ParserState::getFileName() const { - return d_file_name; -} - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h deleted file mode 100644 index cb4ee6834..000000000 --- a/src/parser/parser_state.h +++ /dev/null @@ -1,258 +0,0 @@ -/********************* -*- C++ -*- */ -/** parser_state.h - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** Extra state of the parser shared by the lexer and parser. - ** - ** The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - **/ - -#ifndef __CVC4__PARSER__PARSER_STATE_H -#define __CVC4__PARSER__PARSER_STATE_H - -#include <vector> -#include <iostream> -#include <map> -#include "expr/expr.h" -#include "smt/smt_engine.h" - -namespace CVC4 { -namespace parser { - -/** - * The state of the parser. - */ -class ParserState { -public: - - /** Possible status values of a benchmark */ - enum BenchmarkStatus { - SATISFIABLE, - UNSATISFIABLE, - UNKNOWN - }; - - /** The default constructor. */ - ParserState(SmtEngine* smt, ExprManager* em) : d_uid(0), d_prompt_main("CVC>"), d_prompt_continue("- "), d_prompt("CVC"), d_expressionManager(em), d_smtEngine(smt), d_input_line(0), d_done(false) {} - - /** Parser error handling */ - int parseError(const std::string& s); - - /** Get the next uniqueID as a string */ - std::string getNextUniqueID(); - - /** Get the current prompt */ - std::string getCurrentPrompt() const; - - /** Set the prompt to the main one */ - void setPromptMain(); - - /** Set the prompt to the secondary one */ - void setPromptNextLine(); - - /** Increases the current line number */ - void increaseLineNumber(); - - /** Gets the line number */ - int getLineNumber() const; - - /** Gets the file we are parsing, if any */ - std::string getFileName() const; - - /** - * Are we done yet? - */ - bool done() const { return d_done; } - - /** - * We are done. - */ - void setDone() { d_done = true; } - - /** - * Parses the next chunk of input from the stream. Reads at most size characters - * from the input stream and copies them into the buffer. - * @param the buffer to put the read characters into - * @param size the max numer of character - */ - int read(char* buffer, int size); - - /** - * Makes room for a new string literal (empties the buffer). - */ - void newStringLiteral() { d_string_buffer.clear(); } - - /** - * Returns the current string literal. - */ - std::string getStringLiteral() const { return d_string_buffer; } - - /** - * Appends the first character of str to the string literal buffer. If - * is_escape is true, the first character should be '\' and second character - * is examined to determine the escaped character. - */ - void appendCharToStringLiteral(const char* str, bool is_escape = false) { - if(is_escape) { - // fixme - } else d_string_buffer += str[0]; - } - - /** - * Sets the name of the benchmark. - */ - void setBenchmarkName(const std::string bench_name) { d_benchmark_name = bench_name; } - - /** - * Returns the benchmark name. - */ - std::string getBenchmarkName() const { return d_benchmark_name; } - - /** - * Set the status of the parsed benchmark. - */ - void setBenchmarkStatus(BenchmarkStatus status) { d_status = status; } - - /** - * Get the status of the parsed benchmark. - */ - BenchmarkStatus getBenchmarkStatus() const { return d_status; } - - /** - * Set the logic of the benchmark. - */ - void setBenchmarkLogic(const std::string logic) { d_logic = logic; } - - /** - * Declare a unary predicate (Boolean variable). - */ - void declareNewPredicate(const std::string pred_name) { - d_preds.insert( make_pair(pred_name, d_expressionManager->mkExpr(VARIABLE)) ); - } - - /** - * Creates a new expression, given the kind and the children - */ - CVC4::Expr* newExpression(CVC4::Kind kind, std::vector<CVC4::Expr>& children) { - return new Expr(d_expressionManager->mkExpr(kind, children)); - } - - /** - * Returns a new TRUE Boolean constant. - */ - CVC4::Expr* getNewTrue() { return new Expr(d_expressionManager->mkExpr(TRUE)); } - - /** - * Returns a new TRUE Boolean constant. - */ - CVC4::Expr* getNewFalse() { return new Expr(d_expressionManager->mkExpr(FALSE)); } - - /** - * Returns a variable, given the name. - */ - CVC4::Expr* getNewVariableByName(const std::string var_name) const { - std::map<std::string, Expr>::const_iterator i = d_preds.find(var_name); - return (i == d_preds.end()) ? 0 : new Expr(i->second); - } - - /** - * Sets the command that is the result of the parser. - */ - void setCommand(CVC4::Command* cmd) { d_command = cmd; } - - /** - * Gets the command that is the result of the parser. - */ - CVC4::Command* getCommand() { return d_command; } - - /** - * Sets the interactive flag on/off. If on, every time we go to a new line - * (via increaseLineNumber()) the prompt will be printed to stdout. - */ - void setInteractive(bool interactive = true); - - /** - * Gets the value of the interactive flag. - */ - bool interactive() { return d_interactive; } - - /** - * Gets the SMT Engine - */ - CVC4::SmtEngine* getSmtEngine() { return d_smtEngine; } - - /** - * Sets the SMT Engine - */ - void setSmtEngine(CVC4::SmtEngine* smtEngine) { d_smtEngine = smtEngine; } - - /** - * Gets the Expression Manager - */ - CVC4::ExprManager* getExpressionManager() { return d_expressionManager; } - - /** - * Sets the Expression Manager - */ - void setExpressionManager(CVC4::ExprManager* exprMgr) { d_expressionManager = exprMgr; } - - /** - * Sets the input stream - */ - void setInputStream(std::istream& in) { d_input_stream = ∈ } - -private: - - /** Counter for uniqueID of bound variables */ - int d_uid; - /** The main prompt when running interactive */ - std::string d_prompt_main; - /** The interactive prompt in the middle of a multiline command */ - std::string d_prompt_continue; - /** The currently used prompt */ - std::string d_prompt; - /** The expression manager we will be using */ - ExprManager* d_expressionManager; - /** The smt engine we will be using */ - SmtEngine* d_smtEngine; - /** The stream we are reading off */ - std::istream* d_input_stream; - /** The current input line */ - unsigned d_input_line; - /** File we are parsing */ - std::string d_file_name; - /** Whether we are done or not */ - bool d_done; - /** Whether we are running in interactive mode */ - bool d_interactive; - - /** String to buffer the string literals */ - std::string d_string_buffer; - - /** The name of the benchmark if any */ - std::string d_benchmark_name; - - /** The benchmark's status */ - BenchmarkStatus d_status; - - /** The benchmark's logic */ - std::string d_logic; - - /** declared predicates */ - std::map<std::string, Expr> d_preds; - - /** result of parser */ - Command* d_command; -}; - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__PARSER__PARSER_STATE_H */ diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp deleted file mode 100644 index f0bc21942..000000000 --- a/src/parser/pl.ypp +++ /dev/null @@ -1,388 +0,0 @@ -%{/******************* -*- C++ -*- */ -/** pl.ypp - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** This file contains the bison code for the parser that reads in CVC - ** commands in the presentation language (hence "PL"). - **/ - -#define YYDEBUG 1 - -#include <list> -#include <vector> -#include <string> -#include <ostream> -#include <sstream> - -#include "smt/smt_engine.h" -#include "parser/parser_exception.h" -#include "parser/parser_state.h" -#include "expr/expr.h" -#include "expr/expr_builder.h" -#include "expr/expr_manager.h" -#include "util/command.h" -//#include "rational.h" - -// Exported shared data -namespace CVC4 { - namespace parser { - extern ParserState* _global_parser_state;; - }/* CVC4::parser namespace */ -}/* CVC4 namespace */ - -// Define shortcuts for various things -// #define TMP CVC4::parser::_global_parser_state -// #define EXPR CVC4::parser::_global_parser_state->expr -#define SMT_ENGINE (CVC4::parser::_global_parser_state->getSmtEngine()) -#define EXPR_MANAGER (CVC4::parser::_global_parser_state->getExpressionManager()) -// #define RAT(args) CVC4::newRational args - -// Suppress the bogus warning suppression in bison (it generates -// compile error) -#undef __GNUC_MINOR__ - -/* stuff that lives in PL.lex */ -extern int PLlex(void); - -int PLerror(const char *s) { - std::ostringstream ss; - ss << CVC4::parser::_global_parser_state->getFileName() << ":" - << CVC4::parser::_global_parser_state->getLineNumber() << ": " << s; - CVC4::parser::_global_parser_state->parseError(ss.str()); - return 0;// dead code; error() above throws an exception -} - -// make the entry point public -int CVC4_PUBLIC PLparse(void *YYPARSE_PARAM); - -#define YYLTYPE_IS_TRIVIAL 1 -#define YYMAXDEPTH 10485760 -/* Prefer YYERROR_VERBOSE over %error-verbose to avoid errors in older bison */ -#define YYERROR_VERBOSE 1 - -using namespace CVC4; - -%} - -%union { - std::string *str; - CVC4::Expr *expr; - CVC4::Command *cmd; - std::vector<CVC4::Expr> *vec; - std::list<std::string> *strlst; - int kind; -}; - - -%start cmd - // %start Query - -/* strings are for better error messages. - "_TOK" is so macros don't conflict with kind names */ - -%token DISTINCT_TOK "DISTINCT" -%token AND_TOK "AND" -%token ARRAY_TOK "ARRAY" -%token BOOLEAN_TOK "BOOLEAN" -%token DATATYPE_TOK "DATATYPE" -%token ELSE_TOK "ELSE" -%token ELSIF_TOK "ELSIF" -%token END_TOK "END" -%token ENDIF_TOK "ENDIF" -%token EXISTS_TOK "EXISTS" -%token FALSELIT_TOK "FALSE" -%token FORALL_TOK "FORALL" -%token IN_TOK "IN" -%token IF_TOK "IF" -%token LAMBDA_TOK "LAMBDA" -%token SIMULATE_TOK "SIMULATE" -%token LET_TOK "LET" -%token NOT_TOK "NOT" -%token IS_INTEGER_TOK "IS_INTEGER" -%token OF_TOK "OF" -%token OR_TOK "OR" -%token REAL_TOK "REAL" -%token INT_TOK "INT" -%token SUBTYPE_TOK "SUBTYPE" -%token BITVECTOR_TOK "BITVECTOR" -%token THEN_TOK "THEN" -%token TRUELIT_TOK "TRUE" -%token TYPE_TOK "TYPE" -%token WITH_TOK "WITH" -%token XOR_TOK "XOR" -%token TCC_TOK "TCC" -%token PATTERN_TOK "PATTERN" -%token '_' -%token DONE_TOK - -%token DOTDOT_TOK ".." -%token ASSIGN_TOK ":=" -%token NEQ_TOK "/=" -%token IMPLIES_TOK "=>" -%token IFF_TOK "<=>" -%token PLUS_TOK "+" -%token MINUS_TOK "-" -%token MULT_TOK "*" -%token POW_TOK "^" -%token DIV_TOK "/" -%token MOD_TOK "MOD" -%token INTDIV_TOK "DIV" -%token LT_TOK "<" -%token LE_TOK "<=" -%token GT_TOK ">" -%token GE_TOK ">=" -%token FLOOR_TOK "FLOOR" -%token LEFTSHIFT_TOK "<<" -%token RIGHTSHIFT_TOK ">>" -%token BVPLUS_TOK "BVPLUS" -%token BVSUB_TOK "BVSUB" -%token BVUDIV_TOK "BVUDIV" -%token BVSDIV_TOK "BVSDIV" -%token BVUREM_TOK "BVUREM" -%token BVSREM_TOK "BVSREM" -%token BVSMOD_TOK "BVSMOD" -%token BVSHL_TOK "BVSHL" -%token BVASHR_TOK "BVASHR" -%token BVLSHR_TOK "BVLSHR" -%token BVUMINUS_TOK "BVUMINUS" -%token BVMULT_TOK "BVMULT" -%token SQHASH_TOK "[#" -%token HASHSQ_TOK "#]" -%token PARENHASH_TOK "(#" -%token HASHPAREN_TOK "#)" -%token ARROW_TOK "->" -%token BVNEG_TOK "~" -%token BVAND_TOK "&" -%token MID_TOK "|" -%token BVXOR_TOK "BVXOR" -%token BVNAND_TOK "BVNAND" -%token BVNOR_TOK "BVNOR" -%token BVCOMP_TOK "BVCOMP" -%token BVXNOR_TOK "BVXNOR" -%token CONCAT_TOK "@" -%token BVTOINT_TOK "BVTOINT" -%token INTTOBV_TOK "INTTOBV" -%token BOOLEXTRACT_TOK "BOOLEXTRACT" -%token BVLT_TOK "BVLT" -%token BVGT_TOK "BVGT" -%token BVLE_TOK "BVLE" -%token BVGE_TOK "BVGE" -%token SX_TOK "SX" -%token BVZEROEXTEND_TOK "BVZEROEXTEND" -%token BVREPEAT_TOK "BVREPEAT" -%token BVROTL_TOK "BVROTL" -%token BVROTR_TOK "BVROTR" -%token BVSLT_TOK "BVSLT" -%token BVSGT_TOK "BVSGT" -%token BVSLE_TOK "BVSLE" -%token BVSGE_TOK "BVSGE" - - -/* commands given in prefix syntax */ -%token ARITH_VAR_ORDER_TOK "ARITH_VAR_ORDER" -%token ASSERT_TOK "ASSERT" -%token QUERY_TOK "QUERY" -%token CHECKSAT_TOK "CHECKSAT" -%token CONTINUE_TOK "CONTINUE" -%token RESTART_TOK "RESTART" -%token HELP_TOK "HELP" -%token DBG_TOK "DBG" -%token TRACE_TOK "TRACE" -%token UNTRACE_TOK "UNTRACE" -%token OPTION_TOK "OPTION" -%token TRANSFORM_TOK "TRANSFORM" -%token PRINT_TOK "PRINT" -%token PRINT_TYPE_TOK "PRINT_TYPE" -%token CALL_TOK "CALL" -%token ECHO_TOK "ECHO" -%token INCLUDE_TOK "INCLUDE" -%token DUMP_PROOF_TOK "DUMP_PROOF" -%token DUMP_ASSUMPTIONS_TOK "DUMP_ASSUMPTIONS" -%token DUMP_SIG_TOK "DUMP_SIG" -%token DUMP_TCC_TOK "DUMP_TCC" -%token DUMP_TCC_ASSUMPTIONS_TOK "DUMP_TCC_ASSUMPTIONS" -%token DUMP_TCC_PROOF_TOK "DUMP_TCC_PROOF" -%token DUMP_CLOSURE_TOK "DUMP_CLOSURE" -%token DUMP_CLOSURE_PROOF_TOK "DUMP_CLOSURE_PROOF" -%token WHERE_TOK "WHERE" -%token ASSERTIONS_TOK "ASSERTIONS" -%token ASSUMPTIONS_TOK "ASSUMPTIONS" -%token COUNTEREXAMPLE_TOK "COUNTEREXAMPLE" -%token COUNTERMODEL_TOK "COUNTERMODEL" -%token PUSH_TOK "PUSH" -%token POP_TOK "POP" -%token POPTO_TOK "POPTO" -%token PUSH_SCOPE_TOK "PUSH_SCOPE" -%token POP_SCOPE_TOK "POP_SCOPE" -%token POPTO_SCOPE_TOK "POPTO_SCOPE" -%token RESET_TOK "RESET" -%token CONTEXT_TOK "CONTEXT" -%token FORGET_TOK "FORGET" -%token GET_TYPE_TOK "GET_TYPE" -%token CHECK_TYPE_TOK "CHECK_TYPE" -%token GET_CHILD_TOK "GET_CHILD" -%token GET_OP_TOK "GET_OP" -%token SUBSTITUTE_TOK "SUBSTITUTE" - -%nonassoc ASSIGN_TOK IN_TOK -%nonassoc FORALL_TOK EXISTS_TOK -%left IFF_TOK -%right IMPLIES_TOK -%left OR_TOK XOR_TOK -%left AND_TOK -%left NOT_TOK - -%nonassoc '=' NEQ_TOK -%nonassoc LE_TOK LT_TOK GE_TOK GT_TOK FLOOR_TOK -%left PLUS_TOK MINUS_TOK -%left MULT_TOK INTDIV_TOK DIV_TOK MOD_TOK -%left POW_TOK -%left WITH_TOK -%left UMINUS_TOK -%left CONCAT_TOK -%left MID_TOK -%left BVAND_TOK -%left BVXOR_TOK -%left BVNAND_TOK -%left BVNOR_TOK BVCOMP_TOK -%left BVXNOR_TOK -%left BVNEG_TOK -%left BVUMINUS_TOK BVPLUS_TOK BVSUB_TOK -%left BVUDIV_TOK BVSDIV_TOK BVUREM_TOK BVSREM_TOK BVSMOD_TOK BVSHL_TOK BVASHR_TOK BVLSHR_TOK -%left SX_TOK BVZEROEXTEND_TOK BVREPEAT_TOK BVROTL_TOK BVROTR_TOK -%left LEFTSHIFT_TOK RIGHTSHIFT_TOK -%nonassoc BVLT_TOK BVLE_TOK BVGT_TOK BVGE_TOK -%nonassoc BVSLT_TOK BVSLE_TOK BVSGT_TOK BVSGE_TOK -%right IS_INTEGER_TOK -%left ARROW_TOK - -%nonassoc '[' -%nonassoc '{' '.' '(' -%nonassoc BITVECTOR_TOK - -// %type <vec> FieldDecls TypeList IDs reverseIDs SingleDataTypes Constructors -// %type <vec> LetDecls TypeLetDecls BoundVarDecls ElseRest VarDecls -// %type <vec> Exprs AndExpr OrExpr Pattern Patterns -// %type <vec> RecordEntries UpdatePosition Updates - -// %type <node> Type /* IndexType */ TypeNotIdentifier TypeDef -// %type <node> DataType SingleDataType Constructor -// %type <node> FunctionType RecordType Real Int BitvectorType -// %type <node> FieldDecl TupleType -// %type <node> ArrayType ScalarType SubType BasicType SubrangeType -// %type <node> LeftBound RightBound -%type <expr> Expr // Conditional UpdatePositionNode Update Lambda -// %type <node> QuantExpr ArrayLiteral RecordLiteral RecordEntry TupleLiteral -// %type <node> LetDecl LetExpr LetDeclsNode -// %type <node> TypeLetDecl TypeLetExpr TypeLetDeclsNode -// %type <node> BoundVarDecl BoundVarDeclNode VarDecl -// %type <node> ConstDecl TypeDecl -%type <strlst> IdentifierList // StringLiteral Numeral Binary Hex -%type <str> Identifier // Type - -%type <cmd> cmd /// Assert Query Help Dbg Trace Option -// %type <node> Transform Print Call Echo DumpCommand -// %type <node> Include Where Push Pop PopTo -// %type <node> Context Forget Get_Child Get_Op Get_Type Check_Type Substitute -// %type <node> other_cmd -// %type <node> Arith_Var_Order - -%token <str> ID_TOK STRINGLIT_TOK NUMERAL_TOK HEX_TOK BINARY_TOK - -%% - -cmd: - ASSERT_TOK Expr { - $$ = new AssertCommand(*$2); - CVC4::parser::_global_parser_state->setCommand($$); - delete $2; - } - | QUERY_TOK Expr { - $$ = new QueryCommand(*$2); - CVC4::parser::_global_parser_state->setCommand($$); - delete $2; - } - | CHECKSAT_TOK Expr { - $$ = new CheckSatCommand(*$2); - CVC4::parser::_global_parser_state->setCommand($$); - delete $2; - } - | CHECKSAT_TOK { - $$ = new CheckSatCommand(); - CVC4::parser::_global_parser_state->setCommand($$); - } - | IdentifierList ':' Type { // variable/constant declaration - // FIXME: assuming Type is BOOLEAN - for(std::list<std::string>::iterator i = $1->begin(); i != $1->end(); ++i) - CVC4::parser::_global_parser_state->declareNewPredicate(*i); - delete $1; - CVC4::parser::_global_parser_state->setCommand(new EmptyCommand()); - } - | DONE_TOK { - CVC4::parser::_global_parser_state->setCommand(new EmptyCommand()); - CVC4::parser::_global_parser_state->setDone(); - YYACCEPT; - } - -Expr: - Identifier { - $$ = CVC4::parser::_global_parser_state->getNewVariableByName(*$1); - delete $1; - } - | TRUELIT_TOK { - $$ = new Expr(EXPR_MANAGER->mkExpr(TRUE)); - } - | FALSELIT_TOK { - $$ = new Expr(EXPR_MANAGER->mkExpr(FALSE)); - } - | Expr OR_TOK Expr { - $$ = new Expr(EXPR_MANAGER->mkExpr(OR, *$1, *$3)); - delete $1; - delete $3; - } - | Expr AND_TOK Expr { - $$ = new Expr(EXPR_MANAGER->mkExpr(AND, *$1, *$3)); - delete $1; - delete $3; - } - | Expr IMPLIES_TOK Expr { - $$ = new Expr(EXPR_MANAGER->mkExpr(IMPLIES, *$1, *$3)); - delete $1; - delete $3; - } - | Expr IFF_TOK Expr { - $$ = new Expr(EXPR_MANAGER->mkExpr(IFF, *$1, *$3)); - delete $1; - delete $3; - } - | NOT_TOK Expr { - $$ = new Expr(EXPR_MANAGER->mkExpr(NOT, *$2)); - delete $2; - } ; - -IdentifierList: - Identifier { - $$ = new std::list<std::string>; - $$->push_front(*$1); - delete $1; - } - | Identifier ',' IdentifierList { - $3->push_front(*$1); - $$ = $3; - delete $1; - } - -Identifier: - ID_TOK { - $$ = $1; - } - -Type: - BOOLEAN_TOK - -%% diff --git a/src/parser/pl_scanner.lpp b/src/parser/pl_scanner.lpp deleted file mode 100644 index b7b27c4b0..000000000 --- a/src/parser/pl_scanner.lpp +++ /dev/null @@ -1,313 +0,0 @@ -/********************* -*- C++ -*- */ -/** pl_scanner.lpp - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** CVC4 presentation language lexer. - **/ - -%option interactive -%option noyywrap -%option nounput -%option noreject -%option noyymore -%option yylineno -%option prefix="PL" - -%{ - -#include <list> -#include <vector> -#include <iostream> - -#include "expr/expr_manager.h" /* for the benefit of parsePL_defs.h */ -#include "util/command.h" -#include "parser/parser_state.h" -#include "parser/pl.hpp" -#include "util/debug.h" - -namespace CVC4 { - namespace parser { - extern ParserState* _global_parser_state; - }/* CVC4::parser namespace */ -}/* CVC4 namespace */ - -extern int PL_inputLine; -extern char *PLtext; - -extern int PLerror(const char *msg); - -static int PLinput(std::istream& is, char* buf, int size) { - int res; - if(is) { - // If interactive, read line by line; otherwise read as much as we - // can gobble - if(CVC4::parser::_global_parser_state->interactive()) { - // Print the current prompt - std::cout << CVC4::parser::_global_parser_state->getCurrentPrompt() << std::flush; - // Set the prompt to "middle of the command" one - CVC4::parser::_global_parser_state->setPromptNextLine(); - // Read the line - is.getline(buf, size - 1); - } else // Set the terminator char to 0 - is.getline(buf, size - 1, 0); - // If failbit is set, but eof is not, it means the line simply - // didn't fit; so we clear the state and keep on reading. - bool partialStr = is.fail() && !is.eof(); - if(partialStr) - is.clear(); - - for(res = 0; res < size && buf[res] != 0; ++res) - ; - - if(res == size) - PLerror("Lexer bug: overfilled the buffer"); - - if(!partialStr) { // Insert \n into the buffer - buf[res++] = '\n'; - buf[res] = '\0'; - } - } else { - res = YY_NULL; - } - return res; -} - -// Redefine the input buffer function to read from an istream -#define YY_INPUT(buffer, result, max_size) result = CVC4::parser::_global_parser_state->read(buffer, max_size); - -int PL_bufSize() { return YY_BUF_SIZE; } -YY_BUFFER_STATE PL_buf_state() { return YY_CURRENT_BUFFER; } - -/* some wrappers for methods that need to refer to a struct. - These are used by CVC4::Parser. */ -void *PL_createBuffer(int sz) { - return (void *)PL_create_buffer(NULL, sz); -} -void PL_deleteBuffer(void *buf_state) { - PL_delete_buffer((struct yy_buffer_state *)buf_state); -} -void PL_switchToBuffer(void *buf_state) { - PL_switch_to_buffer((struct yy_buffer_state *)buf_state); -} -void *PL_bufState() { - return (void *)PL_buf_state(); -} - -void PL_setInteractive(bool is_interactive) { - yy_set_interactive(is_interactive); -} - -// File-static (local to this file) variables and functions -static std::string _string_lit; - - static char escapeChar(char c) { - switch(c) { - case 'n': return '\n'; - case 't': return '\t'; - default: return c; - } - } - -// for now, we don't have subranges. -// -// ".." { return DOTDOT_TOK; } -/*OPCHAR (['!#?\_$&\|\\@])*/ - -%} - -%x COMMENT -%x STRING_LITERAL - -LETTER ([a-zA-Z]) -HEX ([0-9a-fA-F]) -BITS ([0-1]) -DIGIT ([0-9]) -OPCHAR (['?\_$~]) -ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) - -%% - -[\n] { CVC4::parser::_global_parser_state->increaseLineNumber(); } - -[ \t\r\f] { /* skip whitespace */ } - -0bin{BITS}+ {PLlval.str = new std::string(PLtext+4);return BINARY_TOK; - } -0hex{HEX}+ {PLlval.str = new std::string(PLtext+4);return HEX_TOK; - } -{DIGIT}+ {PLlval.str = new std::string(PLtext);return NUMERAL_TOK; - } - -"%" { BEGIN COMMENT; } -<COMMENT>"\n" { BEGIN INITIAL; /* return to normal mode */ - CVC4::parser::_global_parser_state->increaseLineNumber(); } -<COMMENT>. { /* stay in comment mode */ } - -<INITIAL>"\"" { BEGIN STRING_LITERAL; - _string_lit.erase(_string_lit.begin(), - _string_lit.end()); } -<STRING_LITERAL>"\\". { /* escape characters (like \n or \") */ - _string_lit.insert(_string_lit.end(), - escapeChar(PLtext[1])); } -<STRING_LITERAL>"\"" { BEGIN INITIAL; /* return to normal mode */ - PLlval.str = new std::string(_string_lit); - return STRINGLIT_TOK; } -<STRING_LITERAL>. { _string_lit.insert(_string_lit.end(),*PLtext); } - -[()[\]{},.;:'!#?_=] { return PLtext[0]; } - -".." { return DOTDOT_TOK; } -":=" { return ASSIGN_TOK; } -"/=" { return NEQ_TOK; } -"=>" { return IMPLIES_TOK; } -"<=>" { return IFF_TOK; } -"+" { return PLUS_TOK; } -"-" { return MINUS_TOK; } -"*" { return MULT_TOK; } -"^" { return POW_TOK; } -"/" { return DIV_TOK; } -"MOD" { return MOD_TOK; } -"DIV" { return INTDIV_TOK; } -"<" { return LT_TOK; } -"<=" { return LE_TOK; } -">" { return GT_TOK; } -">=" { return GE_TOK; } -"FLOOR" { return FLOOR_TOK; } - -"[#" { return SQHASH_TOK; } -"#]" { return HASHSQ_TOK; } -"(#" { return PARENHASH_TOK; } -"#)" { return HASHPAREN_TOK; } -"->" { return ARROW_TOK; } -"ARROW" { return ARROW_TOK; } -"@" { return CONCAT_TOK;} -"~" { return BVNEG_TOK;} -"&" { return BVAND_TOK;} -"|" { return MID_TOK;} -"BVXOR" { return BVXOR_TOK;} -"BVNAND" { return BVNAND_TOK;} -"BVNOR" { return BVNOR_TOK;} -"BVCOMP" { return BVCOMP_TOK;} -"BVXNOR" { return BVXNOR_TOK;} -"<<" { return LEFTSHIFT_TOK;} -">>" { return RIGHTSHIFT_TOK;} -"BVSLT" { return BVSLT_TOK;} -"BVSGT" { return BVSGT_TOK;} -"BVSLE" { return BVSLE_TOK;} -"BVSGE" { return BVSGE_TOK;} -"SX" { return SX_TOK;} -"BVZEROEXTEND" { return BVZEROEXTEND_TOK;} -"BVREPEAT" { return BVREPEAT_TOK;} -"BVROTL" { return BVROTL_TOK;} -"BVROTR" { return BVROTR_TOK;} -"BVLT" { return BVLT_TOK;} -"BVGT" { return BVGT_TOK;} -"BVLE" { return BVLE_TOK;} -"BVGE" { return BVGE_TOK;} - -"DISTINCT" { return DISTINCT_TOK; } -"BVTOINT" { return BVTOINT_TOK;} -"INTTOBV" { return INTTOBV_TOK;} -"BOOLEXTRACT" { return BOOLEXTRACT_TOK;} -"BVPLUS" { return BVPLUS_TOK;} -"BVUDIV" { return BVUDIV_TOK;} -"BVSDIV" { return BVSDIV_TOK;} -"BVUREM" { return BVUREM_TOK;} -"BVSREM" { return BVSREM_TOK;} -"BVSMOD" { return BVSMOD_TOK;} -"BVSHL" { return BVSHL_TOK;} -"BVASHR" { return BVASHR_TOK;} -"BVLSHR" { return BVLSHR_TOK;} -"BVSUB" { return BVSUB_TOK;} -"BVUMINUS" { return BVUMINUS_TOK;} -"BVMULT" { return BVMULT_TOK;} -"AND" { return AND_TOK; } -"ARRAY" { return ARRAY_TOK; } -"BOOLEAN" { return BOOLEAN_TOK; } -"DATATYPE" { return DATATYPE_TOK; } -"ELSE" { return ELSE_TOK; } -"ELSIF" { return ELSIF_TOK; } -"END" { return END_TOK; } -"ENDIF" { return ENDIF_TOK; } -"EXISTS" { return EXISTS_TOK; } -"FALSE" { return FALSELIT_TOK; } -"FORALL" { return FORALL_TOK; } -"IF" { return IF_TOK; } -"IN" { return IN_TOK; } -"LAMBDA" { return LAMBDA_TOK; } -"SIMULATE" { return SIMULATE_TOK; } -"LET" { return LET_TOK; } -"NOT" { return NOT_TOK; } -"IS_INTEGER" { return IS_INTEGER_TOK; } -"OF" { return OF_TOK; } -"OR" { return OR_TOK; } -"REAL" { return REAL_TOK; } -"INT" { return INT_TOK;} -"SUBTYPE" { return SUBTYPE_TOK;} -"BITVECTOR" { return BITVECTOR_TOK;} - -"THEN" { return THEN_TOK; } -"TRUE" { return TRUELIT_TOK; } -"TYPE" { return TYPE_TOK; } -"WITH" { return WITH_TOK; } -"XOR" { return XOR_TOK; } -"TCC" { return TCC_TOK; } -"PATTERN" { return PATTERN_TOK; } - -"ARITH_VAR_ORDER" { return ARITH_VAR_ORDER_TOK; } -"ASSERT" { return ASSERT_TOK; } -"QUERY" { return QUERY_TOK; } -"CHECKSAT" { return CHECKSAT_TOK; } -"CONTINUE" { return CONTINUE_TOK; } -"RESTART" { return RESTART_TOK; } -"DBG" { return DBG_TOK; } -"TRACE" { return TRACE_TOK; } -"UNTRACE" { return UNTRACE_TOK; } -"OPTION" { return OPTION_TOK; } -"HELP" { return HELP_TOK; } -"TRANSFORM" { return TRANSFORM_TOK; } -"PRINT" { return PRINT_TOK; } -"PRINT_TYPE" { return PRINT_TYPE_TOK; } -"CALL" { return CALL_TOK; } -"ECHO" { return ECHO_TOK; } -"INCLUDE" { return INCLUDE_TOK; } -"DUMP_ASSUMPTIONS" { return DUMP_ASSUMPTIONS_TOK; } -"DUMP_PROOF" { return DUMP_PROOF_TOK; } -"DUMP_SIG" { return DUMP_SIG_TOK; } -"DUMP_TCC" { return DUMP_TCC_TOK; } -"DUMP_TCC_ASSUMPTIONS" { return DUMP_TCC_ASSUMPTIONS_TOK; } -"DUMP_TCC_PROOF" { return DUMP_TCC_PROOF_TOK; } -"DUMP_CLOSURE" { return DUMP_CLOSURE_TOK; } -"DUMP_CLOSURE_PROOF" { return DUMP_CLOSURE_PROOF_TOK; } -"WHERE" { return WHERE_TOK; } -"ASSERTIONS" { return ASSERTIONS_TOK; } -"ASSUMPTIONS" { return ASSUMPTIONS_TOK; } -"COUNTEREXAMPLE" { return COUNTEREXAMPLE_TOK; } -"COUNTERMODEL" { return COUNTERMODEL_TOK; } -"PUSH" { return PUSH_TOK; } -"POP" { return POP_TOK; } -"POPTO" { return POPTO_TOK; } -"PUSH_SCOPE" { return PUSH_SCOPE_TOK; } -"POP_SCOPE" { return POP_SCOPE_TOK; } -"POPTO_SCOPE" { return POPTO_SCOPE_TOK; } -"RESET" { return RESET_TOK; } -"CONTEXT" { return CONTEXT_TOK; } -"FORGET" { return FORGET_TOK; } -"GET_TYPE" { return GET_TYPE_TOK; } -"CHECK_TYPE" { return CHECK_TYPE_TOK; } -"GET_CHILD" { return GET_CHILD_TOK; } -"GET_OP" { return GET_OP_TOK; } -"SUBSTITUTE" { return SUBSTITUTE_TOK; } - -(({LETTER})|(_)({ANYTHING}))({ANYTHING})* { PLlval.str = new std::string(PLtext); return ID_TOK; } - -<<EOF>> { return DONE_TOK; } - -. { PLerror("Illegal input character."); } -%% - diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am index acb95849f..59782de7e 100644 --- a/src/parser/smt/Makefile.am +++ b/src/parser/smt/Makefile.am @@ -1,4 +1,4 @@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. AM_CXXFLAGS = -Wall -fvisibility=hidden AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB @@ -7,19 +7,22 @@ noinst_LTLIBRARIES = libparsersmt.la libparsersmt_la_SOURCES = \ SmtLexer.g \ SmtParser.g \ - SmtLexer.hpp \ - SmtLexer.cpp \ - SmtParser.hpp \ - SmtParser.cpp + AntlrSmtLexer.hpp \ + AntlrSmtLexer.cpp \ + AntlrSmtParser.hpp \ + AntlrSmtParser.cpp BUILT_SOURCES = \ - SmtLexer.hpp \ - SmtLexer.cpp \ - SmtParser.hpp \ - SmtParser.cpp + AntlrSmtLexer.hpp \ + AntlrSmtLexer.cpp \ + AntlrSmtParser.hpp \ + AntlrSmtParser.cpp -SmtLexer.cpp SmtLexer.hpp: SmtLexer.g + +AntlrSmtLexer.hpp: SmtLexer.g +AntlrSmtLexer.cpp: SmtLexer.g $(ANTLR) @srcdir@/SmtLexer.g -SmtParser.cpp SmtParser.hpp: SmtParser.g +AntlrSmtParser.hpp: SmtParser.g AntlrSmtLexer.cpp +AntlrSmtParser.cpp: SmtParser.g AntlrSmtLexer.cpp $(ANTLR) @srcdir@/SmtParser.g diff --git a/src/parser/smt/SmtLexer.g b/src/parser/smt/SmtLexer.g index 6af685016..3d9a84f06 100644 --- a/src/parser/smt/SmtLexer.g +++ b/src/parser/smt/SmtLexer.g @@ -1,15 +1,15 @@ 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 + namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace } /** - * SmtLexer class is a stream tokenizer (lexer) for the SMT-LIB benchmark + * AntlrSmtLexer class is a stream tokenizer (lexer) for the SMT-LIB benchmark * language. */ -class SmtLexer extends Lexer; +class AntlrSmtLexer extends Lexer; options { exportVocab = SmtVocabulary; // Name of the shared token vocabulary @@ -144,7 +144,7 @@ NUMERAL options { paraphrase = "a numeral"; } ; /** - * Matches an double quoted string literal. No quote-escaping is supported inside. + * Matches a double quoted string literal. No quote-escaping is supported inside. */ STRING_LITERAL options { paraphrase = "a string literal"; } : '\"' (~('\"'))* '\"' diff --git a/src/parser/smt/SmtParser.g b/src/parser/smt/SmtParser.g index f06951907..f68d783bc 100644 --- a/src/parser/smt/SmtParser.g +++ b/src/parser/smt/SmtParser.g @@ -12,18 +12,18 @@ 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 + namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace } /** - * SmtParser class is the parser for the SMT-LIB files. + * AntlrSmtParser class is the parser for the SMT-LIB files. */ -class SmtParser extends Parser("AntlrParser"); +class AntlrSmtParser extends Parser("AntlrParser"); options { genHashLines = true; // Include line number information - importVocab = SmtVocabulary; // Export the common vocabulary + importVocab = SmtVocabulary; // Import the common vocabulary defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions k = 2; } @@ -64,7 +64,10 @@ prop_atom returns [CVC4::Expr atom] { std::string p; } - : p = pred_symb { atom = getVariable(p, boolType()); } + : p = pred_symb {isDeclared(p, SYM_VARIABLE)}? { atom = getVariable(p); } + exception catch [antlr::SemanticException ex] { + rethrow(ex, "Undeclared variable " + p); + } | TRUE { atom = getTrueExpr(); } | FALSE { atom = getFalseExpr(); } ; @@ -134,7 +137,7 @@ sort_symbs[std::vector<std::string>& sorts] /** * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'. */ -status returns [ SmtParser::BenchmarkStatus status ] +status returns [ AntlrParser::BenchmarkStatus status ] : SAT { status = SMT_SATISFIABLE; } | UNSAT { status = SMT_UNSATISFIABLE; } | UNKNOWN { status = SMT_UNKNOWN; } @@ -143,9 +146,8 @@ status returns [ SmtParser::BenchmarkStatus status ] /** * Matches a benchmark attribute, sucha as ':logic', ':formula', etc. */ -bench_attribute returns [ Command* smt_command ] +bench_attribute returns [ Command* smt_command = 0] { - smt_command = 0; BenchmarkStatus b_status = SMT_UNKNOWN; Expr formula; vector<string> sorts; @@ -167,15 +169,12 @@ bench_attributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence() { Command* cmd; } - : (cmd = bench_attribute { cmd_seq->addCommand(cmd); } )+ + : (cmd = bench_attribute { if (cmd) 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); } +benchmark returns [Command* cmd] + : LPAREN BENCHMARK IDENTIFIER cmd = bench_attributes RPAREN ; diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp deleted file mode 100644 index 1210d8817..000000000 --- a/src/parser/smtlib.ypp +++ /dev/null @@ -1,225 +0,0 @@ -%{/********************* -*- C++ -*- */ -/** smtlib.ypp - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** This file contains the bison code for the parser that reads in CVC - ** commands in SMT-LIB language. - **/ - -#define YYDEBUG 1 - -#include <string> -#include <ostream> -#include <sstream> - -#include "parser_state.h" -#include "smt/smt_engine.h" -#include "util/command.h" -#include "smtlib.hpp" - -// Exported shared data -namespace CVC4 { -namespace parser { - extern ParserState* _global_parser_state; -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ - -using namespace std; -using namespace CVC4; -using namespace CVC4::parser; - -// Suppress the bogus warning suppression in bison (it generates compile error) -#undef __GNUC_MINOR__ - -/** stuff that lives in smtlib_scanner.lpp */ -extern int smtliblex(void); - -/** Error call */ -int smtliberror(const char *s) { - std::ostringstream ss; - ss << CVC4::parser::_global_parser_state->getFileName() << ":" - << CVC4::parser::_global_parser_state->getLineNumber() << ": " << s; - CVC4::parser::_global_parser_state->parseError(ss.str()); - return 0;// dead code; error() above throws an exception -} - -// make the entry point public -int CVC4_PUBLIC smtlibparse(void *YYPARSE_PARAM); - -#define YYLTYPE_IS_TRIVIAL 1 -#define YYMAXDEPTH 10485760 - -%} - -%union { - - std::string *p_string; - std::vector<std::string> *p_string_vector; - - CVC4::Expr *p_expression; - std::vector<CVC4::Expr> *p_expression_vector; - - CVC4::Command *p_command; - CVC4::CommandSequence *p_command_sequence; - - CVC4::parser::ParserState::BenchmarkStatus d_bench_status; - - CVC4::Kind d_kind; - -}; - -%token <p_string> NUMERAL_TOK -%token <p_string> SYM_TOK -%token <p_string> STRING_TOK -%token <p_string> USER_VAL_TOK - -%token TRUE_TOK -%token FALSE_TOK -%token ITE_TOK -%token NOT_TOK -%token IMPLIES_TOK -%token IF_THEN_ELSE_TOK -%token AND_TOK -%token OR_TOK -%token XOR_TOK -%token IFF_TOK -%token LET_TOK -%token FLET_TOK -%token NOTES_TOK -%token LOGIC_TOK -%token SAT_TOK -%token UNSAT_TOK -%token UNKNOWN_TOK -%token ASSUMPTION_TOK -%token FORMULA_TOK -%token STATUS_TOK -%token BENCHMARK_TOK -%token EXTRASORTS_TOK -%token EXTRAFUNS_TOK -%token EXTRAPREDS_TOK -%token DISTINCT_TOK -%token COLON_TOK -%token LBRACKET_TOK -%token RBRACKET_TOK -%token LPAREN_TOK -%token RPAREN_TOK -%token DOLLAR_TOK -%token QUESTION_TOK - -%token EOF_TOK - -%type <p_string> bench_name logic_name pred_symb attribute user_value -%type <d_bench_status> status -%type <p_expression> an_formula an_atom prop_atom -%type <p_expression_vector> an_formulas; -%type <d_kind> connective; -%type <p_command> bench_attribute -%type <p_command_sequence> bench_attributes - -%start benchmark - -%% - -benchmark: - LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK { - _global_parser_state->setBenchmarkName(*$3); - _global_parser_state->setCommand($4); - _global_parser_state->setDone(); - YYACCEPT; - } - | EOF_TOK { - _global_parser_state->setCommand(new EmptyCommand()); - _global_parser_state->setDone(); - YYACCEPT; - } -; - -bench_name: SYM_TOK; - -bench_attributes: - bench_attribute { $$ = new CommandSequence($1); } - | bench_attributes bench_attribute { $$ = $1; $$->addCommand($2); } -; - -bench_attribute: - COLON_TOK FORMULA_TOK an_formula { $$ = new CheckSatCommand(*$3); delete $3; } - | COLON_TOK STATUS_TOK status { $$ = new EmptyCommand(); _global_parser_state->setBenchmarkStatus($3); } - | COLON_TOK LOGIC_TOK logic_name { $$ = new EmptyCommand(); _global_parser_state->setBenchmarkLogic(*$3); delete $3; } - | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK { $$ = new EmptyCommand(); } - | annotation { $$ = new EmptyCommand(); } -; - -logic_name: SYM_TOK; - -status: - SAT_TOK { $$ = ParserState::SATISFIABLE; } - | UNSAT_TOK { $$ = ParserState::UNSATISFIABLE; } - | UNKNOWN_TOK { $$ = ParserState::UNKNOWN; } -; - -pred_symb_decls: - pred_symb_decl - | pred_symb_decls pred_symb_decl -; - -pred_symb_decl: - LPAREN_TOK pred_sig annotations RPAREN_TOK - | LPAREN_TOK pred_sig RPAREN_TOK -; - -pred_sig: - pred_symb { _global_parser_state->declareNewPredicate(*$1); delete $1; } -; - -an_formulas: - an_formula { $$ = new vector<Expr>; $$->push_back(*$1); delete $1; } - | an_formulas an_formula { $$ = $1; $$->push_back(*$2); delete $2; } -; - -an_formula: - an_atom - | LPAREN_TOK connective an_formulas RPAREN_TOK { $$ = _global_parser_state->newExpression($2, *$3); std::cout << "we have an expr: " << *$$ << std::endl; delete $3; } -; - -connective: - NOT_TOK { $$ = NOT; } - | IMPLIES_TOK { $$ = IMPLIES; } - | IF_THEN_ELSE_TOK { $$ = ITE; } - | AND_TOK { $$ = AND; } - | OR_TOK { $$ = OR; } - | XOR_TOK { $$ = XOR; } - | IFF_TOK { $$ = IFF; } -; - -an_atom: prop_atom; - -prop_atom: - TRUE_TOK { $$ = _global_parser_state->getNewTrue(); } - | FALSE_TOK { $$ = _global_parser_state->getNewFalse(); } - | pred_symb { $$ = _global_parser_state->getNewVariableByName(*$1); delete $1; } -; - -annotations: - annotation - | annotations annotation - ; - -annotation: - attribute { delete $1; } - | attribute user_value { delete $1; delete $2; } - ; - -user_value: USER_VAL_TOK; - -pred_symb: SYM_TOK; - -attribute: - COLON_TOK SYM_TOK { $$ = $2; } - ; - -%% diff --git a/src/parser/smtlib_scanner.lpp b/src/parser/smtlib_scanner.lpp deleted file mode 100644 index e9a58b1a9..000000000 --- a/src/parser/smtlib_scanner.lpp +++ /dev/null @@ -1,125 +0,0 @@ -/********************* -*- C++ -*- */ -/** smtlib_scanner.lpp - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** Lexer for smtlib format. - **/ - -%option interactive -%option noyywrap -%option nounput -%option noreject -%option noyymore -%option yylineno -%option prefix="smtlib" - -%{ - -#include <iostream> -#include "parser_state.h" -#include "smt/smt_engine.h" -#include "util/command.h" -#include "smtlib.hpp" - -namespace CVC4 { - namespace parser { - extern ParserState* _global_parser_state; - } -} - -using CVC4::parser::_global_parser_state; - -extern char *smtlibtext; - - -// Redefine the input buffer function to read from an istream -#define YY_INPUT(buffer,result,max_size) result = _global_parser_state->read(buffer, max_size); - -%} - -%x COMMENT -%x STRING_LITERAL - //%x SYM_TOK -%x USER_VALUE - -LETTER ([a-zA-Z]) -DIGIT ([0-9]) -OPCHAR (['\.\_]) -IDCHAR ({LETTER}|{DIGIT}|{OPCHAR}) - -%% - -[\n] { _global_parser_state->increaseLineNumber(); } -[ \t\r\f] { /* skip whitespace */ } - -{DIGIT}+"\."{DIGIT}+ { smtliblval.p_string = new std::string(smtlibtext); return NUMERAL_TOK; } -{DIGIT}+ { smtliblval.p_string = new std::string(smtlibtext); return NUMERAL_TOK; } - -";" { BEGIN COMMENT; } -<COMMENT>"\n" { BEGIN INITIAL; _global_parser_state->increaseLineNumber(); } -<COMMENT>. { /* stay in comment mode */ } - -"\"" { BEGIN STRING_LITERAL; _global_parser_state->newStringLiteral(); } -<STRING_LITERAL>"\\". { _global_parser_state->appendCharToStringLiteral(smtlibtext, true); } -<STRING_LITERAL>"\"" { BEGIN INITIAL; - /* return to normal mode */ - smtliblval.p_string = new std::string(_global_parser_state->getStringLiteral()); - return STRING_TOK; - } -<STRING_LITERAL>. { _global_parser_state->appendCharToStringLiteral(smtlibtext, false); } - -"{" { BEGIN USER_VALUE; _global_parser_state->newStringLiteral(); } -<USER_VALUE>"\\"[{}] { _global_parser_state->appendCharToStringLiteral(smtlibtext, true); } -<USER_VALUE>"}" { BEGIN INITIAL; - /* return to normal mode */ - smtliblval.p_string = new std::string(_global_parser_state->getStringLiteral()); - return USER_VAL_TOK; - } -<USER_VALUE>. { _global_parser_state->appendCharToStringLiteral(smtlibtext, false); } - - -"true" { return TRUE_TOK; } -"false" { return FALSE_TOK; } -"ite" { return ITE_TOK; } -"not" { return NOT_TOK; } -"implies" { return IMPLIES_TOK; } -"if_then_else" { return IF_THEN_ELSE_TOK; } -"and" { return AND_TOK; } -"or" { return OR_TOK; } -"xor" { return XOR_TOK; } -"iff" { return IFF_TOK; } -"let" { return LET_TOK; } -"flet" { return FLET_TOK; } -"notes" { return NOTES_TOK; } -"logic" { return LOGIC_TOK; } -"sat" { return SAT_TOK; } -"unsat" { return UNSAT_TOK; } -"unknown" { return UNKNOWN_TOK; } -"assumption" { return ASSUMPTION_TOK; } -"formula" { return FORMULA_TOK; } -"status" { return STATUS_TOK; } -"benchmark" { return BENCHMARK_TOK; } -"extrasorts" { return EXTRASORTS_TOK; } -"extrafuns" { return EXTRAFUNS_TOK; } -"extrapreds" { return EXTRAPREDS_TOK; } -"distinct" { return DISTINCT_TOK; } -":" { return COLON_TOK; } -"\[" { return LBRACKET_TOK; } -"\]" { return RBRACKET_TOK; } -"(" { return LPAREN_TOK; } -")" { return RPAREN_TOK; } -"$" { return DOLLAR_TOK; } -"?" { return QUESTION_TOK; } - -({LETTER})({IDCHAR})* { smtliblval.p_string = new std::string(smtlibtext); return SYM_TOK; } - -<<EOF>> { return EOF_TOK; } - -. { _global_parser_state->parseError("Illegal input character."); } - -%% diff --git a/src/parser/symbol_table.cpp b/src/parser/symbol_table.cpp deleted file mode 100644 index 296c07731..000000000 --- a/src/parser/symbol_table.cpp +++ /dev/null @@ -1,37 +0,0 @@ -/********************* -*- C++ -*- */ -/** symbol_table.cpp - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - **/ - -#include <string> -#include <list> -#include <vector> - -#include "expr/expr.h" -#include "parser/symbol_table.h" - -namespace CVC4 { -namespace parser { - -void SymbolTable::defineVar(const std::string, const void*) throw() { - -} - -void SymbolTable::defineVarList(const std::list<std::string>*, const void*) throw() { -} - -void SymbolTable::defineVarList(const std::vector<std::string>*, const void*) throw() { -} - -// Type& SymbolTable::lookupType(const std::string&); -Expr& SymbolTable::lookupVar(const std::string*) throw() { -} - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h index 9135343f5..3b08aa5f5 100644 --- a/src/parser/symbol_table.h +++ b/src/parser/symbol_table.h @@ -10,25 +10,84 @@ **/ #include <string> -#include <list> -#include <vector> +#include <stack> +#include <ext/hash_map> #include "expr/expr.h" +namespace __gnu_cxx { +template<> + struct hash<std::string> { + size_t operator()(const std::string& str) const { + return hash<const char*> ()(str.c_str()); + } + }; +} + namespace CVC4 { namespace parser { -class SymbolTable { -public: - // FIXME: No definitions for Type yet - // void defineType(const std::string&, const Type&); - void defineVar(const std::string, const void*) throw(); - void defineVarList(const std::list<std::string>*, const void*) throw(); - void defineVarList(const std::vector<std::string>*, const void*) throw(); - - // Type& lookupType(const std::string&); - Expr& lookupVar(const std::string*) throw(); -}; +/** + * Generic symbol table for looking up variables by name. + */ +template<typename ObjectType> + class SymbolTable { + + private: + + /** The name to expression bindings */ + typedef __gnu_cxx ::hash_map<std::string, std::stack<ObjectType> > + LookupTable; + /** The table iterator */ + typedef typename LookupTable::iterator table_iterator; + /** The table iterator */ + typedef typename LookupTable::const_iterator const_table_iterator; + + /** Bindings for the names */ + LookupTable d_name_bindings; + + public: + + /** + * Bind the name of the variable to the given expression. If the variable + * has been bind before, this will redefine it until its undefined. + */ + void bindName(const std::string name, const ObjectType& obj) throw () { + d_name_bindings[name].push(obj); + } + + /** + * Unbinds the last binding of the name to the expression. + */ + void unbindName(const std::string name) throw () { + table_iterator find = d_name_bindings.find(name); + if(find != d_name_bindings.end()) { + find->second.pop(); + if(find->second.empty()) { + d_name_bindings.erase(find); + } + } + } + + /** + * Returns the last binding expression of the name. + */ + ObjectType getObject(const std::string name) throw () { + ObjectType result; + table_iterator find = d_name_bindings.find(name); + if(find != d_name_bindings.end()) + result = find->second.top(); + return result; + } + + /** + * Returns true is name is bound to an expression. + */ + bool isBound(const std::string name) const throw () { + const_table_iterator find = d_name_bindings.find(name); + return (find != d_name_bindings.end()); + } + }; }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/util/command.cpp b/src/util/command.cpp index 9e541574a..e38695b46 100644 --- a/src/util/command.cpp +++ b/src/util/command.cpp @@ -7,71 +7,99 @@ #include "util/command.h" #include "smt/smt_engine.h" +#include "expr/expr.h" #include "util/result.h" +namespace std { +ostream& operator<<(ostream& out, const CVC4::Command& c) { + c.toString(out); + return out; +} +} + namespace CVC4 { EmptyCommand::EmptyCommand() { } -Result EmptyCommand::invoke(SmtEngine* smt_engine) { - return Result::VALIDITY_UNKNOWN; +void EmptyCommand::invoke(SmtEngine* smt_engine) { } AssertCommand::AssertCommand(const Expr& e) : d_expr(e) { } -Result AssertCommand::invoke(SmtEngine* smt_engine) { - return smt_engine->assert(d_expr); +void AssertCommand::invoke(SmtEngine* smt_engine) { + smt_engine->assert(d_expr); } -CheckSatCommand::CheckSatCommand() : - d_expr(Expr::null()) { +CheckSatCommand::CheckSatCommand() { } CheckSatCommand::CheckSatCommand(const Expr& e) : d_expr(e) { } -Result CheckSatCommand::invoke(SmtEngine* smt_engine) { - return smt_engine->checkSat(d_expr); +void CheckSatCommand::invoke(SmtEngine* smt_engine) { + smt_engine->checkSat(d_expr); } QueryCommand::QueryCommand(const Expr& e) : d_expr(e) { } -Result QueryCommand::invoke(CVC4::SmtEngine* smt_engine) { - return smt_engine->query(d_expr); +void QueryCommand::invoke(CVC4::SmtEngine* smt_engine) { + smt_engine->query(d_expr); } CommandSequence::CommandSequence() : d_last_index(0) { } -CommandSequence::CommandSequence(Command* cmd) : - d_last_index(0) { - addCommand(cmd); -} - - CommandSequence::~CommandSequence() { for(unsigned i = d_last_index; i < d_command_sequence.size(); ++i) delete d_command_sequence[i]; } -Result CommandSequence::invoke(SmtEngine* smt_engine) { - Result r = Result::VALIDITY_UNKNOWN; +void CommandSequence::invoke(SmtEngine* smt_engine) { for(; d_last_index < d_command_sequence.size(); ++d_last_index) { - r = d_command_sequence[d_last_index]->invoke(smt_engine); + d_command_sequence[d_last_index]->invoke(smt_engine); delete d_command_sequence[d_last_index]; } - return r; } void CommandSequence::addCommand(Command* cmd) { d_command_sequence.push_back(cmd); } +// Printout methods + +using namespace std; + +void EmptyCommand::toString(ostream& out) const { + out << "EmptyCommand"; +} + +void AssertCommand::toString(ostream& out) const { + out << "Assert(" << d_expr << ")"; +} + +void CheckSatCommand::toString(ostream& out) const { + if(d_expr.isNull()) + out << "CheckSat()"; + else + out << "CheckSat(" << d_expr << ")"; +} + +void QueryCommand::toString(ostream& out) const { + out << "Query(" << d_expr << ")"; +} + +void CommandSequence::toString(ostream& out) const { + out << "CommandSequence[" << endl; + for(unsigned i = d_last_index; i < d_command_sequence.size(); ++i) + out << *d_command_sequence[i] << endl; + out << "]"; +} + }/* CVC4 namespace */ diff --git a/src/util/command.h b/src/util/command.h index c65429fdb..ce137896a 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -16,7 +16,6 @@ #include "cvc4_config.h" #include "expr/expr.h" -#include "util/result.h" namespace CVC4 { class SmtEngine; @@ -25,15 +24,14 @@ namespace CVC4 { }/* CVC4 namespace */ namespace std { -inline std::ostream& operator<<(std::ostream&, const CVC4::Command*) CVC4_PUBLIC; -inline std::ostream& operator<<(std::ostream&, CVC4::Expr) CVC4_PUBLIC; + std::ostream& operator<<(std::ostream&, const CVC4::Command&) CVC4_PUBLIC; } namespace CVC4 { class CVC4_PUBLIC Command { public: - virtual Result invoke(CVC4::SmtEngine* smt_engine) = 0; + virtual void invoke(CVC4::SmtEngine* smt_engine) = 0; virtual ~Command() {}; virtual void toString(std::ostream&) const = 0; };/* class Command */ @@ -41,8 +39,8 @@ public: class CVC4_PUBLIC EmptyCommand : public Command { public: EmptyCommand(); - Result invoke(CVC4::SmtEngine* smt_engine); - void toString(std::ostream& out) const { out << "EmptyCommand"; } + void invoke(CVC4::SmtEngine* smt_engine); + void toString(std::ostream& out) const; };/* class EmptyCommand */ @@ -51,8 +49,8 @@ protected: Expr d_expr; public: AssertCommand(const Expr& e); - Result invoke(CVC4::SmtEngine* smt_engine); - void toString(std::ostream& out) const { out << "Assert(" << d_expr << ")"; } + void invoke(CVC4::SmtEngine* smt_engine); + void toString(std::ostream& out) const; };/* class AssertCommand */ @@ -60,8 +58,8 @@ class CVC4_PUBLIC CheckSatCommand : public Command { public: CheckSatCommand(); CheckSatCommand(const Expr& e); - Result invoke(SmtEngine* smt); - void toString(std::ostream& out) const { out << "CheckSat(" << d_expr << ")"; } + void invoke(SmtEngine* smt); + void toString(std::ostream& out) const; protected: Expr d_expr; };/* class CheckSatCommand */ @@ -70,8 +68,8 @@ protected: class CVC4_PUBLIC QueryCommand : public Command { public: QueryCommand(const Expr& e); - Result invoke(SmtEngine* smt); - void toString(std::ostream& out) const { out << "Query(" << d_expr << ")"; } + void invoke(SmtEngine* smt); + void toString(std::ostream& out) const; protected: Expr d_expr; };/* class QueryCommand */ @@ -80,21 +78,10 @@ protected: class CVC4_PUBLIC CommandSequence : public Command { public: CommandSequence(); - CommandSequence(Command* cmd); ~CommandSequence(); - Result invoke(SmtEngine* smt); + void invoke(SmtEngine* smt); void addCommand(Command* cmd); - void toString(std::ostream& out) const { - out << "CommandSequence("; - for(std::vector<Command*>::const_iterator i = d_command_sequence.begin(); - i != d_command_sequence.end(); - ++i) { - out << *i; - if(i != d_command_sequence.end()) - out << " ; "; - } - out << ")"; - } + void toString(std::ostream& out) const; private: /** All the commands to be executed (in sequence) */ std::vector<Command*> d_command_sequence; @@ -104,11 +91,4 @@ private: }/* CVC4 namespace */ -inline std::ostream& std::operator<<(std::ostream& out, const CVC4::Command* c) { - if(c) - c->toString(out); - else out << "(null)"; - return out; -} - #endif /* __CVC4__COMMAND_H */ diff --git a/src/util/options.h b/src/util/options.h index 54b4e2f9b..8d2d113a2 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -18,6 +18,7 @@ namespace CVC4 { struct Options { + std::string binary_name; bool smtcomp_mode; @@ -33,7 +34,18 @@ struct Options { /* with 3, the solver is slowed down by all the scrolling */ int verbosity; - std::string lang; + /** The input language option */ + enum InputLanguage { + /** The SMTLIB input language */ + LANG_SMTLIB, + /** The CVC4 input language */ + LANG_CVC4, + /** Auto-detect the language */ + LANG_AUTO + }; + + /** The input language */ + InputLanguage lang; Options() : binary_name(), smtcomp_mode(false), @@ -41,7 +53,7 @@ struct Options { out(0), err(0), verbosity(0), - lang() + lang(LANG_AUTO) {} };/* struct Options */ |