<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"/>
</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">
</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>
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
# 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])
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
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) {
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,
inline iterator end() const;
void toString(std::ostream&) const;
+
+ bool isNull() const;
+
};/* class Expr */
}/* CVC4 namespace */
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;
* 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. */
static size_t next_id;
+ /** Private default constructor for the null value. */
+ ExprValue();
+
public:
/** Hash this expression.
* @return the hash value of this expression. */
enum Kind {
/* undefined */
UNDEFINED_KIND = -1,
+ /** Null Kind */
+ NULL_EXPR,
/* built-ins */
EQUAL,
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;
#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 {
{ "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;
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);
// 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] + "'");
}
}
#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;
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();
}
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 */
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 $@ $<
* Author: dejan
*/
+#include <iostream>
+
#include "antlr_parser.h"
#include "expr/expr_manager.h"
out << "unknown";
break;
default:
- CVC4::UnhandledImpl("Unhandled ostream case for AntlrParser::BenchmarkStatus");
+ CVC4::UnhandledImpl(
+ "Unhandled ostream case for AntlrParser::BenchmarkStatus");
}
return out;
}
}
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 {
}
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());
}
#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 {
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:
/**
*/
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
*/
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
*/
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 */
/** 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_ */
+++ /dev/null
-/********************* -*- 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 */
**/
#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 */
#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 {
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 */
+++ /dev/null
-/*
- * 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 */
+++ /dev/null
-/********************* -*- 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 */
+++ /dev/null
-%{/******************* -*- 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
-
-%%
+++ /dev/null
-/********************* -*- 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."); }
-%%
-
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
AM_CXXFLAGS = -Wall -fvisibility=hidden
AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
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
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
;
/**
- * 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"; }
: '\"' (~('\"'))* '\"'
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;
}
{
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(); }
;
/**
* 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; }
/**
* 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;
{
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
;
+++ /dev/null
-%{/********************* -*- 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; }
- ;
-
-%%
+++ /dev/null
-/********************* -*- 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."); }
-
-%%
+++ /dev/null
-/********************* -*- 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 */
**/
#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 */
#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 */
#include "cvc4_config.h"
#include "expr/expr.h"
-#include "util/result.h"
namespace CVC4 {
class SmtEngine;
}/* 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 */
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 */
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 */
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 */
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 */
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;
}/* 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 */
namespace CVC4 {
struct Options {
+
std::string binary_name;
bool smtcomp_mode;
/* 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),
out(0),
err(0),
verbosity(0),
- lang()
+ lang(LANG_AUTO)
{}
};/* struct Options */
projects / cvc5.git / commitdiff