From 2a1ac62e56d43893c59c4c2d91bcaca0dd7ce417 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 25 Nov 2009 00:42:52 +0000 Subject: [PATCH] additional work on parser hookup, configuration + build --- Makefile.am | 5 ++ configure.ac | 24 +++++++--- src/include/cvc4.h | 2 +- src/main/main.cpp | 3 -- src/parser/Makefile.am | 18 ++++---- src/parser/parser.cpp | 86 +++++++++++++++++++++++++++++++---- src/parser/parser.h | 66 +++++++++++++-------------- src/parser/parser_exception.h | 25 +++++----- src/parser/parser_state.cpp | 25 ++++++++++ src/parser/parser_state.h | 52 +++++++++++---------- src/parser/pl.ypp | 3 +- src/parser/symbol_table.cpp | 37 +++++++++++++++ src/parser/symbol_table.h | 17 +++---- src/smt/smt_engine.cpp | 9 ++++ src/smt/smt_engine.h | 11 ++++- src/util/Makefile.am | 3 +- src/util/assert.h | 35 ++++++++++++-- src/util/command.cpp | 18 ++++++++ src/util/command.h | 29 ++++++++---- src/util/exception.h | 22 ++++++--- 20 files changed, 357 insertions(+), 133 deletions(-) create mode 100644 src/parser/parser_state.cpp create mode 100644 src/parser/symbol_table.cpp create mode 100644 src/util/command.cpp diff --git a/Makefile.am b/Makefile.am index b3e12c811..02d9e1bea 100644 --- a/Makefile.am +++ b/Makefile.am @@ -5,3 +5,8 @@ ACLOCAL_AMFLAGS = -I config SUBDIRS = src test doc contrib +.PHONY: production debug default competition +production: ; @srcdir@/configure --with-build=production && $(MAKE) +debug: ; @srcdir@/configure --with-build=debug && $(MAKE) +default: ; @srcdir@/configure --with-build=default && $(MAKE) +competition:; @srcdir@/configure --with-build=competition && $(MAKE) diff --git a/configure.ac b/configure.ac index 0aba48aa3..168f80320 100644 --- a/configure.ac +++ b/configure.ac @@ -11,9 +11,15 @@ AC_CONFIG_HEADERS([config.h]) # keep track of whether the user set these (check here, because # autoconf might set a default later) +AC_MSG_CHECKING([for user CPPFLAGS]) if test -z "${CPPFLAGS+set}"; then user_cppflags=no; else user_cppflags=yes; fi +AC_MSG_RESULT([${CPPFLAGS-none}]) +AC_MSG_CHECKING([for user CXXFLAGS]) if test -z "${CXXFLAGS+set}"; then user_cxxflags=no; else user_cxxflags=yes; fi +AC_MSG_RESULT([${CXXFLAGS-none}]) +AC_MSG_CHECKING([for user LDFLAGS]) if test -z "${LDFLAGS+set}" ; then user_ldflags=no ; else user_ldflags=yes ; fi +AC_MSG_RESULT([${LDFLAGS-none}]) LT_INIT @@ -209,6 +215,16 @@ AC_TYPE_SIZE_T # Prepare configure output +if test "$user_cppflags" = no; then + CPPFLAGS="$CVC4CPPFLAGS" +fi +if test "$user_cxxflags" = no; then + CXXFLAGS="$CVC4CXXFLAGS" +fi +if test "$user_ldflags" = no; then + LDFLAGS="$CVC4LDFLAGS" +fi + AC_CONFIG_FILES([ Makefile contrib/Makefile @@ -251,7 +267,7 @@ LDFLAGS : $LDFLAGS Now just type make, followed by make check or make install, as you like. -You can also use 'make build_profile' to reconfigure for a different profile. +You can use 'make ' to reconfig/build a different profile. Build profiles: production optimized default competition EOF @@ -262,8 +278,6 @@ if test "$user_cppflags" = yes; then AC_MSG_WARN([To support your options to configure, I would like to set CPPFLAGS to:]) AC_MSG_WARN([ $CVC4CPPFLAGS]) AC_MSG_WARN([]) -else - CPPFLAGS="$CVC4CPPFLAGS" fi if test "$user_cxxflags" = yes; then AC_MSG_WARN([]) @@ -271,8 +285,6 @@ if test "$user_cxxflags" = yes; then AC_MSG_WARN([To support your options to configure, I would like to set CXXFLAGS to:]) AC_MSG_WARN([ $CVC4CXXFLAGS]) AC_MSG_WARN([]) -else - CXXFLAGS="$CVC4CXXFLAGS" fi if test "$user_ldflags" = yes; then AC_MSG_WARN([]) @@ -280,8 +292,6 @@ if test "$user_ldflags" = yes; then AC_MSG_WARN([To support your options to configure, I would like to set LDFLAGS to:]) AC_MSG_WARN([ $CVC4LDFLAGS]) AC_MSG_WARN([]) -else - LDFLAGS="$CVC4LDFLAGS" fi non_standard= diff --git a/src/include/cvc4.h b/src/include/cvc4.h index 5d33fa838..bbaffabb0 100644 --- a/src/include/cvc4.h +++ b/src/include/cvc4.h @@ -67,7 +67,7 @@ public: /* * Construct an SmtEngine with the given expression manager and user options. */ - SmtEngine(ExprManager*, Options*); + SmtEngine(ExprManager*, Options*) throw(); /** * Execute a command. diff --git a/src/main/main.cpp b/src/main/main.cpp index 1fc616fe6..58d86a42d 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -71,9 +71,6 @@ int main(int argc, char *argv[]) { cmd->invoke(); delete cmd; } - - if(infile) - infile.close(); } catch(CVC4::main::OptionException* e) { if(opts.smtcomp_mode) { printf("unknown"); diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 7965b88f9..8d8730d68 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -5,19 +5,21 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libparser.la libparser_la_SOURCES = \ + parser.cpp \ + parser_state.cpp \ + symbol_table.cpp \ pl_scanner.lpp \ - pl.ypp # \ - # smtlib_scanner.lpp \ - # smtlib.ypp \ - # parser.cpp + pl.ypp +# smtlib_scanner.lpp \ +# smtlib.ypp BUILT_SOURCES = \ pl_scanner.cpp \ pl.cpp \ - pl.hpp # \ - # smtlib_scanner.cpp \ - # smtlib.cpp \ - # smtlib.hpp + pl.hpp \ + smtlib_scanner.cpp \ + smtlib.cpp \ + smtlib.hpp # produce headers too AM_YFLAGS = -d diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 89170beeb..42ff506fa 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -8,19 +8,87 @@ ** information. ** ** Parser implementation. - ** - ** The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University **/ -#include "parser.h" -#include "parser_temp.h" -#include "parser_exception.h" +#include "parser/parser.h" +#include "parser/parser_state.h" +#include "parser/parser_exception.h" +#include "parser/pl.hpp" +//#include "parser/smtlib.hpp" + +// The communication entry points of the actual parsers + +// for presentation language (PL.y and PL.lex) +extern int PLparse(); +extern void *PL_createBuffer(int); +extern void PL_deleteBuffer(void *); +extern void PL_switchToBuffer(void *); +extern int PL_bufSize(); +extern void *PL_bufState(); +void PL_setInteractive(bool); + +// for smtlib language (smtlib.y and smtlib.lex) +extern int smtlibparse(); +extern void *smtlib_createBuffer(int); +extern void smtlib_deleteBuffer(void *); +extern void smtlib_switchToBuffer(void *); +extern int smtlib_bufSize(); +extern void *smtlibBufState(); +void smtlib_setInteractive(bool); namespace CVC4 { +namespace parser { -ParserTemp *parserTemp; +ParserState *parserState; -}/* CVC4 namespace */ +Parser::Parser(CVC4::SmtEngine* smt, Language lang, std::istream& is, CVC4::Options* opts, bool interactive) throw() + : d_smt(smt), + d_is(is), + d_opts(opts), + d_lang(lang), + d_interactive(interactive), + d_buffer(0) { + + parserState->lineNum = 1; + switch(d_lang) { + case PL: + d_buffer = ::PL_createBuffer(::PL_bufSize()); + break; + case SMTLIB: + //d_buffer = ::smtlib_createBuffer(::smtlib_bufSize()); + break; + default: + Unhandled(); + } +} +Parser::~Parser() throw() { + switch(d_lang) { + case PL: + ::PL_deleteBuffer(d_buffer); + break; + case SMTLIB: + //::smtlib_deleteBuffer(d_buffer); + break; + default: + Unhandled(); + } +} + +CVC4::Command* Parser::next() throw() { + return 0; +} + +bool Parser::done() const throw() { + return false; +} + +void Parser::printLocation(std::ostream & out) const throw() { +} + +void Parser::reset() throw() { +} + + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/parser.h b/src/parser/parser.h index 73565b8c4..8103238b3 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -13,47 +13,45 @@ #ifndef __CVC4__PARSER__PARSER_H #define __CVC4__PARSER__PARSER_H +#include + #include "util/exception.h" #include "parser/language.h" +#include "parser/parser_state.h" #include "util/command.h" +#include "util/options.h" +#include "expr/expr.h" +#include "smt/smt_engine.h" +#include "util/assert.h" namespace CVC4 { namespace parser { - class Expr; - - // Internal parser state and other data - class ParserData; - - class Parser { - private: - ParserData* d_data; - // Internal methods for constructing and destroying the actual parser - void initParser(); - void deleteParser(); - public: - // Constructors - Parser(CVC4::SmtEngine* smt, Language lang, std::istream& is, Options* opts, bool interactive = false); - // Destructor - ~Parser(); - // Read the next command. - CVC4::Command* next(); - // Check if we are done (end of input has been reached) - bool done() const; - // The same check can be done by using the class Parser's value as - // a Boolean - operator bool() const { return done(); } - void printLocation(std::ostream & out) const; - // Reset any local data that depends on validity checker - void reset(); - }; // end of class 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. - class ParserTemp; - extern ParserTemp* parserTemp; +class Parser { + + CVC4::SmtEngine *d_smt; + std::istream &d_is; + CVC4::Options *d_opts; + Language d_lang; + bool d_interactive; + void *d_buffer; + +public: + // Constructors + Parser(CVC4::SmtEngine* smt, Language lang, std::istream& is, CVC4::Options* opts, bool interactive = false) throw(); + // Destructor + ~Parser() throw(); + // Read the next command. + CVC4::Command* next() throw(); + // Check if we are done (end of input has been reached) + bool done() const throw(); + // The same check can be done by using the class Parser's value as + // a Boolean + operator bool() const throw() { return done(); } + void printLocation(std::ostream & out) const throw(); + // Reset any local data that depends on SmtEngine + void reset() throw(); +}; // end of class Parser }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index 89490fad8..b2cf8bc55 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -14,24 +14,25 @@ #define __CVC4__PARSER__PARSER_EXCEPTION_H #include "util/exception.h" +#include "cvc4_config.h" #include #include namespace CVC4 { namespace parser { - class ParserException: public Exception { - public: - // Constructors - ParserException() { } - ParserException(const std::string& msg): Exception(msg) { } - ParserException(const char* msg): Exception(msg) { } - // Destructor - virtual ~ParserException() { } - virtual std::string toString() const { - return "Parse Error: " + d_msg; - } - }; // end of class ParserException +class CVC4_PUBLIC ParserException: public Exception { +public: + // Constructors + ParserException() { } + ParserException(const std::string& msg): Exception(msg) { } + ParserException(const char* msg): Exception(msg) { } + // Destructor + virtual ~ParserException() { } + virtual std::string toString() const { + return "Parse Error: " + d_msg; + } +}; // end of class ParserException }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp new file mode 100644 index 000000000..654fbfe32 --- /dev/null +++ b/src/parser/parser_state.cpp @@ -0,0 +1,25 @@ +/********************* -*- C++ -*- */ +/** parser_state.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. + ** + ** Parser state implementation. + **/ + +#include +#include "parser/parser_state.h" +#include "parser/parser_exception.h" + +namespace CVC4 { +namespace parser { + +void ParserState::error(const std::string& s) throw(ParserException*) { + throw new ParserException(s); +} + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h index 0fbedb958..2bcc08bef 100644 --- a/src/parser/parser_state.h +++ b/src/parser/parser_state.h @@ -22,6 +22,7 @@ #include "expr/expr.h" #include "expr/expr_manager.h" #include "parser/symbol_table.h" +#include "parser/parser_exception.h" #include "util/exception.h" namespace CVC4 { @@ -41,8 +42,8 @@ private: // The currently used prompt std::string prompt; public: - SmtEngine* smtEngine; - ExprManager* exprManager; + CVC4::SmtEngine* smtEngine; + CVC4::ExprManager* exprManager; SymbolTable* symbolTable; std::istream* is; // The current input line @@ -50,7 +51,7 @@ public: // File name std::string fileName; // The last parsed Expr - Expr expr; + CVC4::Expr expr; // Whether we are done or not bool done; // Whether we are running interactive @@ -64,37 +65,38 @@ public: // Did we encounter a formula query (smtlib) bool queryParsed; // Default constructor - ParserState() : d_uid(0), - prompt1("CVC> "), - prompt2("- "), - prompt("CVC> "), - smtEngine(0), - exprManager(0), - symbolTable(0), - is(0), - lineNum(1), - fileName(), - expr(Expr::null()), - done(false), - interactive(false), - arrFlag(false), - bvFlag(false), - bvSize(0), - queryParsed(false) { } + ParserState() throw() + : d_uid(0), + prompt1("CVC> "), + prompt2("- "), + prompt("CVC> "), + smtEngine(0), + exprManager(0), + symbolTable(0), + is(0), + lineNum(1), + fileName(), + expr(CVC4::Expr::null()), + done(false), + interactive(false), + arrFlag(false), + bvFlag(false), + bvSize(0), + queryParsed(false) { } // Parser error handling (implemented in parser.cpp) - int error(const std::string& s); + void error(const std::string& s) throw(ParserException*) __attribute__((noreturn)); // Get the next uniqueID as a string - std::string uniqueID() { + std::string uniqueID() throw() { std::ostringstream ss; ss << d_uid++; return ss.str(); } // Get the current prompt - std::string getPrompt() { return prompt; } + std::string getPrompt() throw() { return prompt; } // Set the prompt to the main one - void setPrompt1() { prompt = prompt1; } + void setPrompt1() throw() { prompt = prompt1; } // Set the prompt to the secondary one - void setPrompt2() { prompt = prompt2; } + void setPrompt2() throw() { prompt = prompt2; } }; }/* CVC4::parser namespace */ diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp index 20687b783..a4aa7ef70 100644 --- a/src/parser/pl.ypp +++ b/src/parser/pl.ypp @@ -54,7 +54,8 @@ int PLerror(const char *s) std::ostringstream ss; ss << CVC4::parser::parserState->fileName << ":" << CVC4::parser::parserState->lineNum << ": " << s; - return CVC4::parser::parserState->error(ss.str()); + CVC4::parser::parserState->error(ss.str()); + return 0;// dead code; error() above throws an exception } #define YYLTYPE_IS_TRIVIAL 1 diff --git a/src/parser/symbol_table.cpp b/src/parser/symbol_table.cpp new file mode 100644 index 000000000..296c07731 --- /dev/null +++ b/src/parser/symbol_table.cpp @@ -0,0 +1,37 @@ +/********************* -*- 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 +#include +#include + +#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*, const void*) throw() { +} + +void SymbolTable::defineVarList(const std::vector*, 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 3339ab67a..9135343f5 100644 --- a/src/parser/symbol_table.h +++ b/src/parser/symbol_table.h @@ -7,11 +7,6 @@ ** 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 **/ #include @@ -21,17 +16,19 @@ #include "expr/expr.h" 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*); - void defineVarList(const std::list*, const void*); - void defineVarList(const std::vector*, const void*); + void defineVar(const std::string, const void*) throw(); + void defineVarList(const std::list*, const void*) throw(); + void defineVarList(const std::vector*, const void*) throw(); // Type& lookupType(const std::string&); - Expr& lookupVar(const std::string*); + Expr& lookupVar(const std::string*) throw(); }; -} +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f6b81465b..f9ebc713d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -10,8 +10,17 @@ **/ #include "smt/smt_engine.h" +#include "util/exception.h" +#include "util/command.h" namespace CVC4 { +void doCommand(Command* c) { + if(c->getSmtEngine() != this) + throw new IllegalArgumentException("SmtEngine does not match Command"); + + c->invoke(); +} + }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 149de058e..af2f45c23 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -15,7 +15,6 @@ #include #include "expr/expr.h" #include "expr/expr_manager.h" -#include "util/command.h" #include "util/result.h" #include "util/model.h" #include "util/options.h" @@ -26,6 +25,8 @@ namespace CVC4 { +class Command; + // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the // hood): use a type parameter and have check() delegate, or subclass // SmtEngine and override check()? @@ -84,7 +85,7 @@ public: /* * Construct an SmtEngine with the given expression manager and user options. */ - SmtEngine(ExprManager* em, Options* opts) : d_em(em), d_opts(opts) {} + SmtEngine(ExprManager* em, Options* opts) throw() : d_em(em), d_opts(opts) {} /** * Execute a command. @@ -105,6 +106,12 @@ public: */ Result query(Expr); + /** + * Add a formula to the current context and call check(). Returns + * true iff consistent. + */ + Result checkSat(Expr); + /** * Simplify a formula without doing "much" work. Requires assist * from the SAT Engine. diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 4fe483c98..c70553c3e 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -4,4 +4,5 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libutil.la -libutil_la_SOURCES = +libutil_la_SOURCES = \ + command.cpp diff --git a/src/util/assert.h b/src/util/assert.h index 6691c1b04..4a164716c 100644 --- a/src/util/assert.h +++ b/src/util/assert.h @@ -20,20 +20,27 @@ namespace CVC4 { -class AssertionException : public Exception { +class CVC4_PUBLIC AssertionException : public Exception { public: AssertionException() : Exception() {} AssertionException(std::string msg) : Exception(msg) {} AssertionException(const char* msg) : Exception(msg) {} };/* class AssertionException */ -class UnreachableCodeException : public AssertionException { +class CVC4_PUBLIC UnreachableCodeException : public AssertionException { public: UnreachableCodeException() : AssertionException() {} UnreachableCodeException(std::string msg) : AssertionException(msg) {} UnreachableCodeException(const char* msg) : AssertionException(msg) {} };/* class UnreachableCodeException */ +class CVC4_PUBLIC UnhandledCaseException : public UnreachableCodeException { +public: + UnhandledCaseException() : UnreachableCodeException() {} + UnhandledCaseException(std::string msg) : UnreachableCodeException(msg) {} + UnhandledCaseException(const char* msg) : UnreachableCodeException(msg) {} +};/* class UnhandledCaseException */ + #ifdef CVC4_ASSERTIONS # define Assert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg) #else /* ! CVC4_ASSERTIONS */ @@ -41,10 +48,12 @@ public: #endif /* CVC4_ASSERTIONS */ #define AlwaysAssert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg) -#define Unreachable(cond, msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, __builtin_expect((cond), 1), ## msg) +#define Unreachable(msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, ## msg) +#define Unhandled(msg...) __CVC4_UNHANDLEDGLUE("Hit an unhandled case at " __FILE__ ":", __LINE__, ## msg) #define __CVC4_ASSERTGLUE(str1, line, str2, cond, msg...) AssertImpl(str1 #line str2, cond, ## msg) -#define __CVC4_UNREACHABLEGLUE(str, line, cond, msg...) AssertImpl(str #line, cond, ## msg) +#define __CVC4_UNREACHABLEGLUE(str, line, msg...) UnreachableImpl(str #line, ## msg) +#define __CVC4_UNHANDLEDGLUE(str, line, msg...) UnhandledImpl(str #line, ## msg) inline void AssertImpl(const char* info, bool cond, std::string msg) { if(EXPECT_FALSE( ! cond )) @@ -79,6 +88,24 @@ inline void UnreachableImpl(const char* info) { throw new UnreachableCodeException(info); } +#ifdef __GNUC__ +inline void UnhandledImpl(const char* info, std::string msg) __attribute__ ((noreturn)); +inline void UnhandledImpl(const char* info, const char* msg) __attribute__ ((noreturn)); +inline void UnhandledImpl(const char* info) __attribute__ ((noreturn)); +#endif /* __GNUC__ */ + +inline void UnhandledImpl(const char* info, std::string msg) { + throw new UnhandledCaseException(std::string(info) + "\n" + msg); +} + +inline void UnhandledImpl(const char* info, const char* msg) { + throw new UnhandledCaseException(std::string(info) + "\n" + msg); +} + +inline void UnhandledImpl(const char* info) { + throw new UnhandledCaseException(info); +} + }/* CVC4 namespace */ #endif /* __CVC4__ASSERT_H */ diff --git a/src/util/command.cpp b/src/util/command.cpp new file mode 100644 index 000000000..db03a9189 --- /dev/null +++ b/src/util/command.cpp @@ -0,0 +1,18 @@ +/********************* -*- C++ -*- */ +/** command.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 "util/command.h" +#include "smt/smt_engine.h" + +namespace CVC4 { + + +}/* CVC4 namespace */ diff --git a/src/util/command.h b/src/util/command.h index 976e2b3d7..6de87c9f2 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -13,39 +13,48 @@ #define __CVC4__COMMAND_H #include "expr/expr.h" +#include "smt/smt_engine.h" namespace CVC4 { -class SmtEngine; - class Command { +protected: SmtEngine* d_smt; public: Command(CVC4::SmtEngine* smt) : d_smt(smt) {} + SmtEngine* getSmtEngine() { return d_smt; } virtual void invoke() = 0; }; class AssertCommand : public Command { +protected: + Expr d_expr; + public: - AssertCommand(const Expr&); - void invoke() { } + AssertCommand(CVC4::SmtEngine* smt, const Expr& e) : Command(smt), d_expr(e) {} + void invoke() { d_smt->assert(d_expr); } }; class CheckSatCommand : public Command { +protected: + Expr d_expr; + public: - CheckSatCommand(void); - CheckSatCommand(const Expr&); - void invoke() { } + CheckSatCommand(CVC4::SmtEngine* smt) : Command(smt), d_expr(Expr::null()) {} + CheckSatCommand(CVC4::SmtEngine* smt, const Expr& e) : Command(smt), d_expr(e) {} + void invoke() { d_smt->checkSat(d_expr); } }; class QueryCommand : public Command { +protected: + Expr d_expr; + public: - QueryCommand(const Expr&); - void invoke() { } + QueryCommand(CVC4::SmtEngine* smt, const Expr& e) : Command(smt), d_expr(e) {} + void invoke() { d_smt->query(d_expr); } }; - }/* CVC4 namespace */ #endif /* __CVC4__COMMAND_H */ diff --git a/src/util/exception.h b/src/util/exception.h index e3b8f2293..76eabe67e 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -15,19 +15,20 @@ #include #include +#include "cvc4_config.h" namespace CVC4 { -class Exception { +class CVC4_PUBLIC Exception { protected: std::string d_msg; public: // Constructors - Exception(): d_msg("Unknown exception") { } - Exception(const std::string& msg): d_msg(msg) { } - Exception(const char* msg): d_msg(msg) { } + Exception() : d_msg("Unknown exception") {} + Exception(const std::string& msg) : d_msg(msg) {} + Exception(const char* msg) : d_msg(msg) {} // Destructor - virtual ~Exception() { } + virtual ~Exception() {} // NON-VIRTUAL METHODs for setting and printing the error message void setMessage(const std::string& msg) { d_msg = msg; } // Printing: feel free to redefine toString(). When inherited, @@ -36,13 +37,22 @@ public: virtual std::string toString() const { return d_msg; } // No need to overload operator<< for the inherited classes friend std::ostream& operator<<(std::ostream& os, const Exception& e); +};/* class Exception */ + + +class CVC4_PUBLIC IllegalArgumentException : public Exception { +public: + IllegalArgumentException() : Exception("Illegal argument to method or function") {} + IllegalArgumentException(const std::string& msg) : Exception(msg) {} + IllegalArgumentException(const char* msg) : Exception(msg) {} +};/* class IllegalArgumentException */ -}; // end of class Exception inline std::ostream& operator<<(std::ostream& os, const Exception& e) { return os << e.toString(); } + }/* CVC4 namespace */ #endif /* __CVC4__EXCEPTION_H */ -- 2.30.2