From 7fb54afe126e5045fc6c5553c1aff3c3f73509aa Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 3 Dec 2009 14:59:30 +0000 Subject: [PATCH] parsing/expr/command/result/various other fixes --- src/Makefile.am | 6 +- src/expr/expr.cpp | 8 +- src/expr/expr.h | 57 ++++- src/expr/expr_builder.h | 29 ++- src/expr/expr_manager.h | 49 ++++- src/expr/expr_value.cpp | 2 + src/expr/expr_value.h | 6 + src/expr/kind.h | 36 ++++ src/main/Makefile.am | 2 +- src/main/getopt.cpp | 2 +- src/main/main.cpp | 36 ++-- src/parser/Makefile.am | 6 +- src/parser/parser.cpp | 44 +++- src/parser/parser.h | 107 +++++----- src/parser/parser_state.cpp | 46 ++-- src/parser/parser_state.h | 384 ++++++++++++++++++++-------------- src/parser/pl.ypp | 49 +++-- src/parser/pl_scanner.lpp | 27 +-- src/parser/smtlib.ypp | 37 +++- src/parser/smtlib_scanner.lpp | 10 +- src/smt/smt_engine.cpp | 47 ++++- src/smt/smt_engine.h | 11 +- src/util/command.cpp | 66 +++--- src/util/command.h | 158 ++++++++------ src/util/output.h | 13 +- src/util/result.h | 24 ++- 26 files changed, 838 insertions(+), 424 deletions(-) diff --git a/src/Makefile.am b/src/Makefile.am index ca22263fd..b79eddf8b 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -21,9 +21,13 @@ publicheaders = \ include/cvc4_config.h \ include/cvc4_expr.h -install-data-local: +install-data-local: $(publicheaders) $(mkinstalldirs) $(DESTDIR)$(includedir)/cvc4; \ @for f in $(publicheaders); do echo $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4" $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4" done + +include/cvc4.h: smt/smt_engine.h + @srcdir@/headergen.pl $< $@ +include/cvc4_expr.h: expr/expr.h diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index f94a3c438..2e3d7a7e2 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -22,16 +22,18 @@ Expr Expr::s_null(0); Expr::Expr(ExprValue* ev) : d_ev(ev) { - d_ev->inc(); + if(d_ev != 0) + d_ev->inc(); } Expr::Expr(const Expr& e) { - if((d_ev = e.d_ev)) + if((d_ev = e.d_ev) && d_ev != 0) d_ev->inc(); } Expr::~Expr() { - d_ev->dec(); + if(d_ev) + d_ev->dec(); } Expr& Expr::operator=(const Expr& e) { diff --git a/src/expr/expr.h b/src/expr/expr.h index 19f02650e..5a11e0fbd 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -14,12 +14,23 @@ #define __CVC4__EXPR_H #include +#include #include #include "cvc4_config.h" #include "expr/kind.h" namespace CVC4 { + class Expr; +}/* CVC4 namespace */ + +namespace std { +inline std::ostream& operator<<(std::ostream&, CVC4::Expr) CVC4_PUBLIC; +} + +namespace CVC4 { + +class ExprManager; namespace expr { class ExprValue; @@ -45,10 +56,8 @@ class CVC4_PUBLIC Expr { * Increments the reference count. */ explicit Expr(ExprValue*); - typedef Expr* iterator; - typedef Expr const* const_iterator; - friend class ExprBuilder; + friend class ExprManager; public: CVC4_PUBLIC Expr(const Expr&); @@ -81,20 +90,62 @@ public: inline Kind getKind() const; + inline size_t numChildren() const; + static Expr null() { return s_null; } + typedef Expr* iterator; + typedef Expr const* const_iterator; + + inline iterator begin(); + inline iterator end(); + inline iterator begin() const; + inline iterator end() const; + + void toString(std::ostream&) const; };/* class Expr */ }/* CVC4 namespace */ #include "expr/expr_value.h" +inline std::ostream& std::operator<<(std::ostream& out, CVC4::Expr e) { + e.toString(out); + return out; +} + namespace CVC4 { inline Kind Expr::getKind() const { return Kind(d_ev->d_kind); } +inline void Expr::toString(std::ostream& out) const { + if(d_ev) + d_ev->toString(out); + else out << "null"; +} + +inline Expr::iterator Expr::begin() { + return d_ev->begin(); +} + +inline Expr::iterator Expr::end() { + return d_ev->end(); +} + +inline Expr::iterator Expr::begin() const { + return d_ev->begin(); +} + +inline Expr::iterator Expr::end() const { + return d_ev->end(); +} + +inline size_t Expr::numChildren() const { + return d_ev->d_nchildren; +} + }/* CVC4 namespace */ #endif /* __CVC4__EXPR_H */ diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h index 13f196dd0..5c6019de1 100644 --- a/src/expr/expr_builder.h +++ b/src/expr/expr_builder.h @@ -13,6 +13,8 @@ #define __CVC4__EXPR_BUILDER_H #include +#include + #include "expr_manager.h" #include "kind.h" @@ -48,6 +50,14 @@ class ExprBuilder { typedef ExprValue** ev_iterator; typedef ExprValue const** const_ev_iterator; + ev_iterator ev_begin() { + return d_children.u_arr; + } + + ev_iterator ev_end() { + return d_children.u_arr + d_nchildren; + } + ExprBuilder& reset(const ExprValue*); public: @@ -188,8 +198,23 @@ inline ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& e // not const inline ExprBuilder::operator Expr() { - // FIXME - return Expr::s_null; + uint64_t hash = d_kind; + + for(ev_iterator i = ev_begin(); i != ev_end(); ++i) + hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->hash(); + + void *space = std::malloc(sizeof(ExprValue) + d_nchildren * sizeof(Expr)); + ExprValue *ev = new (space) ExprValue; + size_t nc = 0; + for(ev_iterator i = ev_begin(); i != ev_end(); ++i) + ev->d_children[nc++] = Expr(*i); + ev->d_nchildren = d_nchildren; + ev->d_kind = d_kind; + ev->d_id = ExprValue::next_id++; + ev->d_rc = 0; + Expr e(ev); + + return d_em->lookup(hash, e); } inline AndExprBuilder ExprBuilder::operator&&(Expr e) { diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index e3fbd91bf..ee18ddc01 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -13,14 +13,61 @@ #define __CVC4__EXPR_MANAGER_H #include +#include + #include "expr/expr.h" #include "kind.h" namespace CVC4 { -class ExprManager { +namespace expr { + class ExprBuilder; +}/* CVC4::expr namespace */ + +class CVC4_PUBLIC ExprManager { static __thread ExprManager* s_current; + friend class CVC4::ExprBuilder; + + typedef std::map > hash_t; + hash_t d_hash; + + Expr lookup(uint64_t hash, const Expr& e) { + hash_t::iterator i = d_hash.find(hash); + if(i == d_hash.end()) { + // insert + std::vector v; + v.push_back(e); + d_hash.insert(std::make_pair(hash, v)); + return e; + } else { + for(std::vector::iterator j = i->second.begin(); j != i->second.end(); ++j) { + if(e.getKind() != j->getKind()) + continue; + + if(e.numChildren() != j->numChildren()) + continue; + + Expr::iterator c1 = e.begin(); + Expr::iterator c2 = j->begin(); + while(c1 != e.end() && c2 != j->end()) { + if(c1->d_ev != c2->d_ev) + break; + } + + if(c1 != e.end() || c2 != j->end()) + continue; + + return *j; + } + // didn't find it, insert + std::vector v; + v.push_back(e); + d_hash.insert(std::make_pair(hash, v)); + return e; + } + } + public: static ExprManager* currentEM() { return s_current; } diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp index fa5628e26..e24bb88b1 100644 --- a/src/expr/expr_value.cpp +++ b/src/expr/expr_value.cpp @@ -18,6 +18,8 @@ namespace CVC4 { +size_t ExprValue::next_id = 0; + uint64_t ExprValue::hash() const { uint64_t hash = d_kind; diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h index 0b97dfdae..decd57045 100644 --- a/src/expr/expr_value.h +++ b/src/expr/expr_value.h @@ -63,6 +63,8 @@ class ExprValue { ExprValue* inc(); ExprValue* dec(); + static size_t next_id; + public: /** Hash this expression. * @return the hash value of this expression. */ @@ -82,6 +84,10 @@ public: const_iterator end() const; const_iterator rbegin() const; const_iterator rend() const; + + void toString(std::ostream& out) { + out << Kind(d_kind); + } }; }/* CVC4::expr namespace */ diff --git a/src/expr/kind.h b/src/expr/kind.h index db25d914e..790fd644d 100644 --- a/src/expr/kind.h +++ b/src/expr/kind.h @@ -12,6 +12,8 @@ #ifndef __CVC4__KIND_H #define __CVC4__KIND_H +#include + namespace CVC4 { // TODO: create this file (?) from theory solver headers so that we @@ -49,4 +51,38 @@ enum Kind { }/* CVC4 namespace */ +inline std::ostream& operator<<(std::ostream&, const CVC4::Kind&) CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& out, const CVC4::Kind& k) { + using namespace CVC4; + + switch(k) { + case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break; + case EQUAL: out << "EQUAL"; break; + case ITE: out << "ITE"; break; + case SKOLEM: out << "SKOLEM"; break; + case VARIABLE: out << "VARIABLE"; break; + + /* propositional connectives */ + case FALSE: out << "FALSE"; break; + case TRUE: out << "TRUE"; break; + + case NOT: out << "NOT"; break; + + case AND: out << "AND"; break; + case IFF: out << "IFF"; break; + case IMPLIES: out << "IMPLIES"; break; + case OR: out << "OR"; break; + case XOR: out << "XOR"; break; + + /* from arith */ + case PLUS: out << "PLUS"; break; + case MINUS: out << "MINUS"; break; + case MULT: out << "MULT"; break; + + default: out << "UNKNOWNKIND!"; break; + } + + return out; +} + #endif /* __CVC4__KIND_H */ diff --git a/src/main/Makefile.am b/src/main/Makefile.am index dddfb3219..36e4c0342 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -10,5 +10,5 @@ cvc4_SOURCES = \ util.cpp cvc4_LDADD = \ - ../parser/libparser.la \ + ../parser/libcvc4parser.la \ ../libcvc4.la diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 5af3b5d21..f60dd6e24 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -68,7 +68,7 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(Exception*) { progName = x + 1; opts->binary_name = string(progName); - while((c = getopt_long(argc, argv, "+:hVvL:", cmdlineOptions, NULL)) != -1) { + while((c = getopt_long(argc, argv, "+:hVvqL:", cmdlineOptions, NULL)) != -1) { switch(c) { case 'h': diff --git a/src/main/main.cpp b/src/main/main.cpp index 58d86a42d..323a989c8 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -27,8 +27,11 @@ #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; @@ -53,23 +56,32 @@ int main(int argc, char *argv[]) { throw new Exception("Too many input files specified."); } else { in = &infile; - if(strlen(argv[firstArgIndex]) >= 4 && !strcmp(argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4, ".smt")) + 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)); - exit(1); + throw new Exception(string("Could not open input file `") + + argv[firstArgIndex] + "' for reading: " + + strerror(errno)); } } - ExprManager *exprMgr = new ExprManager(); + ExprManager *exprMgr = new ExprManager; SmtEngine smt(exprMgr, &opts); - Parser parser(&smt, lang, *in, &opts); + Parser parser(&smt, exprMgr, lang, *in, &opts); while(!parser.done()) { - Command *cmd = parser.next(); - cmd->invoke(); - delete cmd; + Command *cmd = parser.parseNextCommand(opts.verbosity > 1); + if(opts.verbosity > 0) { + cout << "invoking cmd: "; + cout << cmd << endl; + } + if(cmd) { + if(opts.verbosity >= 0) + cout << cmd->invoke(&smt) << endl; + delete cmd; + } } } catch(CVC4::main::OptionException* e) { if(opts.smtcomp_mode) { @@ -78,24 +90,24 @@ int main(int argc, char *argv[]) { } fprintf(stderr, "CVC4 Error:\n%s\n\n", e->toString().c_str()); printf(usage, opts.binary_name.c_str()); - exit(1); + abort(); } catch(CVC4::Exception* e) { if(opts.smtcomp_mode) { printf("unknown"); fflush(stdout); } fprintf(stderr, "CVC4 Error:\n%s\n", e->toString().c_str()); - exit(1); + abort(); } catch(bad_alloc) { if(opts.smtcomp_mode) { printf("unknown"); fflush(stdout); } fprintf(stderr, "CVC4 ran out of memory.\n"); - exit(1); + abort(); } catch(...) { fprintf(stderr, "CVC4 threw an exception of unknown type.\n"); - exit(1); + abort(); } return 0; diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 256ebef0e..800afc990 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -2,12 +2,14 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -I@builddir@ AM_CXXFLAGS = -Wall -fvisibility=hidden AM_CPPFLAGS = -D__BUILDING_CVC4LIB -noinst_LTLIBRARIES = libparser.la +nobase_lib_LTLIBRARIES = libcvc4parser.la -libparser_la_SOURCES = \ +libcvc4parser_la_SOURCES = \ parser.cpp \ parser_state.cpp \ symbol_table.cpp \ + pl_scanner.lpp \ + pl.ypp \ smtlib_scanner.lpp \ smtlib.ypp diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 1bf0341f2..89276872c 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -10,17 +10,51 @@ ** Parser implementation. **/ -#include "parser.h" -#include "parser_state.h" -#include "parser_exception.h" +#include -namespace CVC4 { +#include "parser/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; +using namespace std; +using namespace CVC4; + +namespace CVC4 { namespace parser { -ParserState *_global_parser_state; +ParserState CVC4_PUBLIC *_global_parser_state = 0; + +bool Parser::done() const { + return _global_parser_state->done(); +} + +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(); + } + return new EmptyCommand; +} +Parser::~Parser() { + //delete d_data; } +}/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/parser.h b/src/parser/parser.h index 765fb0553..411e7760c 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -16,83 +16,84 @@ #include #include -namespace CVC4 -{ -namespace parser -{ +#include "parser/language.h" +#include "parser/parser_state.h" + +namespace CVC4 { // Forward declarations class Expr; class Command; class ExprManager; -class ParserState; +class SmtEngine; +class Options; + +namespace parser { /** - * The 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 Parser -{ - private: +extern ParserState CVC4_PUBLIC *_global_parser_state; - /** Internal parser state we are keeping */ - ParserState* d_data; +/** + * The parser. + */ +class CVC4_PUBLIC Parser { + private: - /** Initialize the parser */ - void initParser(); + /** Internal parser state we are keeping */ + //ParserState* d_data; - /** Remove the parser components */ - void deleteParser(); + /** Initialize the parser */ + void initParser(); - public: + /** Remove the parser components */ + void deleteParser(); - /** The supported input languages */ - enum InputLanguage { - /** SMT-LIB language */ - INPUT_SMTLIB, - /** CVC language */ - INPUT_CVC - }; + Language d_lang; + std::istream &d_in; + Options *d_opts; - /** - * Constructor for parsing out of a file. - * @param em the expression manager to use - * @param lang the language syntax to use - * @param file_name the file to parse - */ - Parser(ExprManager* em, InputLanguage lang, const std::string& file_name); + public: - /** - * Destructor. - */ - ~Parser(); + /** + * Constructor for parsing out of a 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); + } - /** Parse a command */ - Command parseNextCommand(); + /** + * Destructor. + */ + ~Parser(); - /** Parse an expression of the stream */ - Expr parseNextExpression(); + /** Parse a command */ + Command* parseNextCommand(bool verbose = false); - // Check if we are done (end of input has been reached) - bool done() const; + /** Parse an expression of the stream */ + Expr parseNextExpression(); - // The same check can be done by using the class Parser's value as a Boolean - operator bool() const { return done(); } + // Check if we are done (end of input has been reached) + bool done() const; - /** Prints the location to the output stream */ - void printLocation(std::ostream& out) const; + // The same check can be done by using the class Parser's value as a Boolean + operator bool() const { return done(); } - /** Reset any local data */ - void reset(); + /** Prints the location to the output stream */ + void printLocation(std::ostream& out) const; + /** Reset any local data */ + 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. - */ -extern ParserState* _global_parser_state; - }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp index 25f1cfd78..db64107e1 100644 --- a/src/parser/parser_state.cpp +++ b/src/parser/parser_state.cpp @@ -11,14 +11,10 @@ using namespace std; -namespace CVC4 -{ +namespace CVC4 { +namespace parser { -namespace parser -{ - -int ParserState::read(char* buffer, int size) -{ +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); @@ -26,41 +22,29 @@ int ParserState::read(char* buffer, int size) } else return 0; } -ParserState::ParserState() : - d_uid(0), d_prompt_main("CVC>"), d_prompt_continue("- "), d_prompt("CVC"), d_input_line(0), d_done(false) -{ - -} - -int ParserState::parseError(const std::string& s) -{ +int ParserState::parseError(const std::string& s) { throw new ParserException(s); } -string ParserState::getNextUniqueID() -{ +string ParserState::getNextUniqueID() { ostringstream ss; ss << d_uid++; return ss.str(); } -string ParserState::getCurrentPrompt() const -{ +string ParserState::getCurrentPrompt() const { return d_prompt; } -void ParserState::setPromptMain() -{ +void ParserState::setPromptMain() { d_prompt = d_prompt_main; } -void ParserState::setPromptNextLine() -{ +void ParserState::setPromptNextLine() { d_prompt = d_prompt_continue; } -void ParserState::increaseLineNumber() -{ +void ParserState::increaseLineNumber() { ++d_input_line; if (d_interactive) { std::cout << getCurrentPrompt(); @@ -68,17 +52,13 @@ void ParserState::increaseLineNumber() } } -int ParserState::getLineNumber() const -{ +int ParserState::getLineNumber() const { return d_input_line; } -std::string ParserState::getFileName() const -{ +std::string ParserState::getFileName() const { return d_file_name; } -} // End namespace parser - -} // End namespace CVC3 - +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h index 8b18ff22f..cb4ee6834 100644 --- a/src/parser/parser_state.h +++ b/src/parser/parser_state.h @@ -19,169 +19,237 @@ #include #include -#include "cvc4.h" +#include +#include "expr/expr.h" +#include "smt/smt_engine.h" -namespace CVC4 -{ - -namespace parser -{ +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(); - - /** 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; - - /** - * 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(); - - /** - * Returns the current string literal. - */ - std::string getStringLiteral() const; - - /** - * 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); - - /** - * Sets the name of the benchmark. - */ - void setBenchmarkName(const std::string bench_name); - - /** - * Returns the benchmark name. - */ - std::string getBenchmarkName() const; - - /** - * Set the status of the parsed benchmark. - */ - void setBenchmarkStatus(BenchmarkStatus status); - - /** - * Get the status of the parsed benchmark. - */ - BenchmarkStatus getBenchmarkStatus() const; - - /** - * Set the logic of the benchmark. - */ - void setBenchmarkLogic(const std::string logic); - - /** - * Declare a unary predicate (Boolean variable). - */ - void declareNewPredicate(const std::string pred_name); - - /** - * Creates a new expression, given the kind and the children - */ - CVC4::Expr* newExpression(CVC4::Kind kind, std::vector& children); - - /** - * Returns a new TRUE Boolean constant. - */ - CVC4::Expr* getNewTrue() const; - - /** - * Returns a new TRUE Boolean constant. - */ - CVC4::Expr* getNewFalse() const; - - /** - * Retruns a variable, given the name. - */ - CVC4::Expr* getNewVariableByName(const std::string var_name) const; - - /** - * Sets the command that is the result of the parser. - */ - void setCommand(CVC4::Command* cmd); - - /** - * 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); - - 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_expression_manager; - /** 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; +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& 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::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 d_preds; + + /** result of parser */ + Command* d_command; }; }/* CVC4::parser namespace */ diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp index 2668eabb8..f0bc21942 100644 --- a/src/parser/pl.ypp +++ b/src/parser/pl.ypp @@ -1,4 +1,4 @@ -/********************* -*- C++ -*- */ +%{/******************* -*- C++ -*- */ /** pl.ypp ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) @@ -11,12 +11,13 @@ ** commands in the presentation language (hence "PL"). **/ -%{ - +#define YYDEBUG 1 #include #include #include +#include +#include #include "smt/smt_engine.h" #include "parser/parser_exception.h" @@ -30,16 +31,15 @@ // Exported shared data namespace CVC4 { namespace parser { - extern ParserState* parserState; + extern ParserState* _global_parser_state;; }/* CVC4::parser namespace */ -}/* CVC4 hnamespace */ +}/* CVC4 namespace */ // Define shortcuts for various things -// #define TMP CVC4::parser::parserState -// #define EXPR CVC4::parser::parserState->expr -#define SMT_ENGINE (CVC4::parser::parserState->smtEngine) -#define EXPR_MANAGER (CVC4::parser::parserState->exprManager) -#define SYMBOL_TABLE (CVC4::parser::parserState->symbolTable) +// #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 @@ -49,15 +49,17 @@ namespace CVC4 { /* stuff that lives in PL.lex */ extern int PLlex(void); -int PLerror(const char *s) -{ +int PLerror(const char *s) { std::ostringstream ss; - ss << CVC4::parser::parserState->fileName << ":" << CVC4::parser::parserState->lineNum - << ": " << s; - CVC4::parser::parserState->error(ss.str()); + 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 */ @@ -297,27 +299,40 @@ using namespace CVC4; 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 - SYMBOL_TABLE->defineVarList($1, (const void *)0); + for(std::list::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 { - $$ = new Expr(SYMBOL_TABLE->lookupVar($1)); + $$ = CVC4::parser::_global_parser_state->getNewVariableByName(*$1); + delete $1; } | TRUELIT_TOK { $$ = new Expr(EXPR_MANAGER->mkExpr(TRUE)); diff --git a/src/parser/pl_scanner.lpp b/src/parser/pl_scanner.lpp index 3b0f79a42..b7b27c4b0 100644 --- a/src/parser/pl_scanner.lpp +++ b/src/parser/pl_scanner.lpp @@ -32,7 +32,7 @@ namespace CVC4 { namespace parser { - extern ParserState* parserState; + extern ParserState* _global_parser_state; }/* CVC4::parser namespace */ }/* CVC4 namespace */ @@ -46,23 +46,27 @@ static int PLinput(std::istream& is, char* buf, int size) { if(is) { // If interactive, read line by line; otherwise read as much as we // can gobble - if(CVC4::parser::parserState->interactive) { + if(CVC4::parser::_global_parser_state->interactive()) { // Print the current prompt - std::cout << CVC4::parser::parserState->getPrompt() << std::flush; + std::cout << CVC4::parser::_global_parser_state->getCurrentPrompt() << std::flush; // Set the prompt to "middle of the command" one - CVC4::parser::parserState->setPrompt2(); + CVC4::parser::_global_parser_state->setPromptNextLine(); // Read the line - is.getline(buf, size-1); + is.getline(buf, size - 1); } else // Set the terminator char to 0 - is.getline(buf, size-1, 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; resis, buf, max_size); +#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; } @@ -129,7 +132,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) %% -[\n] { CVC4::parser::parserState->lineNum++; } +[\n] { CVC4::parser::_global_parser_state->increaseLineNumber(); } [ \t\r\f] { /* skip whitespace */ } @@ -142,7 +145,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) "%" { BEGIN COMMENT; } "\n" { BEGIN INITIAL; /* return to normal mode */ - CVC4::parser::parserState->lineNum++; } + CVC4::parser::_global_parser_state->increaseLineNumber(); } . { /* stay in comment mode */ } "\"" { BEGIN STRING_LITERAL; diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp index b1aeaa570..1210d8817 100644 --- a/src/parser/smtlib.ypp +++ b/src/parser/smtlib.ypp @@ -11,15 +11,23 @@ ** commands in SMT-LIB language. **/ -#include "cvc4.h" +#define YYDEBUG 1 + +#include +#include +#include + #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; @@ -32,7 +40,16 @@ using namespace CVC4::parser; extern int smtliblex(void); /** Error call */ -int smtliberror(const char *s) { return _global_parser_state->parseError(s); } +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 @@ -112,8 +129,14 @@ benchmark: LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK { _global_parser_state->setBenchmarkName(*$3); _global_parser_state->setCommand($4); - } - | EOF_TOK { _global_parser_state->setCommand(new EmptyCommand()); } + _global_parser_state->setDone(); + YYACCEPT; + } + | EOF_TOK { + _global_parser_state->setCommand(new EmptyCommand()); + _global_parser_state->setDone(); + YYACCEPT; + } ; bench_name: SYM_TOK; @@ -160,7 +183,7 @@ an_formulas: an_formula: an_atom - | LPAREN_TOK connective an_formulas RPAREN_TOK { $$ = _global_parser_state->newExpression($2, *$3); delete $3; } + | LPAREN_TOK connective an_formulas RPAREN_TOK { $$ = _global_parser_state->newExpression($2, *$3); std::cout << "we have an expr: " << *$$ << std::endl; delete $3; } ; connective: diff --git a/src/parser/smtlib_scanner.lpp b/src/parser/smtlib_scanner.lpp index 70026bd4c..e9a58b1a9 100644 --- a/src/parser/smtlib_scanner.lpp +++ b/src/parser/smtlib_scanner.lpp @@ -22,12 +22,14 @@ #include #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; -} + namespace parser { + extern ParserState* _global_parser_state; + } } using CVC4::parser::_global_parser_state; @@ -42,7 +44,7 @@ extern char *smtlibtext; %x COMMENT %x STRING_LITERAL -%x SYM_TOK + //%x SYM_TOK %x USER_VALUE LETTER ([a-zA-Z]) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f9ebc713d..05ee12462 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -15,12 +15,51 @@ namespace CVC4 { -void doCommand(Command* c) { - if(c->getSmtEngine() != this) - throw new IllegalArgumentException("SmtEngine does not match Command"); +void SmtEngine::doCommand(Command* c) { + c->invoke(this); +} + +Expr SmtEngine::preprocess(Expr e) { + return e; +} + +void SmtEngine::processAssertionList() { + for(std::vector::iterator i = d_assertions.begin(); + i != d_assertions.end(); + ++i) + ;//d_expr = d_expr.isNull() ? *i : d_expr.andExpr(*i); +} + +Result SmtEngine::check() { + processAssertionList(); + return Result(Result::VALIDITY_UNKNOWN); +} - c->invoke(); +Result SmtEngine::quickCheck() { + processAssertionList(); + return Result(Result::VALIDITY_UNKNOWN); } +void SmtEngine::addFormula(Expr e) { + d_assertions.push_back(e); +} + +Result SmtEngine::checkSat(Expr e) { + e = preprocess(e); + addFormula(e); + return check(); +} + +Result SmtEngine::query(Expr e) { + e = preprocess(e); + addFormula(e); + return check(); +} + +Result SmtEngine::assert(Expr e) { + e = preprocess(e); + addFormula(e); + return quickCheck(); +} }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index af2f45c23..3e33cc8af 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -13,6 +13,8 @@ #define __CVC4__SMT_ENGINE_H #include + +#include "cvc4_config.h" #include "expr/expr.h" #include "expr/expr_manager.h" #include "util/result.h" @@ -41,7 +43,7 @@ class Command; class SmtEngine { /** Current set of assertions. */ // TODO: make context-aware to handle user-level push/pop. - std::vector d_assertList; + std::vector d_assertions; /** Our expression manager */ ExprManager *d_em; @@ -49,13 +51,16 @@ class SmtEngine { /** User-level options */ Options *d_opts; + /** Expression built-up for handing off to the propagation engine */ + Expr d_expr; + /** * Pre-process an Expr. This is expected to be highly-variable, * with a lot of "source-level configurability" to add multiple * passes over the Expr. TODO: may need to specify a LEVEL of * preprocessing (certain contexts need more/less ?). */ - void preprocess(Expr); + Expr preprocess(Expr); /** * Adds a formula to the current context. @@ -85,7 +90,7 @@ public: /* * Construct an SmtEngine with the given expression manager and user options. */ - SmtEngine(ExprManager* em, Options* opts) throw() : d_em(em), d_opts(opts) {} + SmtEngine(ExprManager* em, Options* opts) throw() : d_em(em), d_opts(opts), d_expr(Expr::null()) {} /** * Execute a command. diff --git a/src/util/command.cpp b/src/util/command.cpp index 35db79a0d..9e541574a 100644 --- a/src/util/command.cpp +++ b/src/util/command.cpp @@ -5,73 +5,73 @@ * Author: dejan */ -#include "command.h" +#include "util/command.h" +#include "smt/smt_engine.h" +#include "util/result.h" -using namespace CVC4; +namespace CVC4 { -void EmptyCommand::invoke(SmtEngine* smt_engine) { } +EmptyCommand::EmptyCommand() { +} + +Result EmptyCommand::invoke(SmtEngine* smt_engine) { + return Result::VALIDITY_UNKNOWN; +} AssertCommand::AssertCommand(const Expr& e) : - d_expr(e) -{ + d_expr(e) { } -void AssertCommand::invoke(SmtEngine* smt_engine) -{ - smt_engine->assert(d_expr); +Result AssertCommand::invoke(SmtEngine* smt_engine) { + return smt_engine->assert(d_expr); } -CheckSatCommand::CheckSatCommand() -{ +CheckSatCommand::CheckSatCommand() : + d_expr(Expr::null()) { } CheckSatCommand::CheckSatCommand(const Expr& e) : - d_expr(e) -{ + d_expr(e) { } -void CheckSatCommand::invoke(SmtEngine* smt_engine) -{ - smt_engine->checkSat(d_expr); +Result CheckSatCommand::invoke(SmtEngine* smt_engine) { + return smt_engine->checkSat(d_expr); } QueryCommand::QueryCommand(const Expr& e) : - d_expr(e) -{ + d_expr(e) { } -void QueryCommand::invoke(CVC4::SmtEngine* smt_engine) -{ - smt_engine->query(d_expr); +Result QueryCommand::invoke(CVC4::SmtEngine* smt_engine) { + return smt_engine->query(d_expr); } CommandSequence::CommandSequence() : - d_last_index(0) -{ + d_last_index(0) { } CommandSequence::CommandSequence(Command* cmd) : - d_last_index(0) -{ + d_last_index(0) { addCommand(cmd); } -CommandSequence::~CommandSequence() -{ - for (unsigned i = d_last_index; i < d_command_sequence.size(); i++) +CommandSequence::~CommandSequence() { + for(unsigned i = d_last_index; i < d_command_sequence.size(); ++i) delete d_command_sequence[i]; } -void CommandSequence::invoke(SmtEngine* smt_engine) -{ - for (; d_last_index < d_command_sequence.size(); d_last_index++) { - d_command_sequence[d_last_index]->invoke(smt_engine); +Result CommandSequence::invoke(SmtEngine* smt_engine) { + Result r = Result::VALIDITY_UNKNOWN; + for(; d_last_index < d_command_sequence.size(); ++d_last_index) { + r = d_command_sequence[d_last_index]->invoke(smt_engine); delete d_command_sequence[d_last_index]; } + return r; } -void CommandSequence::addCommand(Command* cmd) -{ +void CommandSequence::addCommand(Command* cmd) { d_command_sequence.push_back(cmd); } + +}/* CVC4 namespace */ diff --git a/src/util/command.h b/src/util/command.h index c6778f34a..c65429fdb 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -12,69 +12,103 @@ #ifndef __CVC4__COMMAND_H #define __CVC4__COMMAND_H -#include "cvc4.h" - -namespace CVC4 -{ - -class SmtEngine; - -class Command -{ - public: - virtual void invoke(CVC4::SmtEngine* smt_engine) = 0; - virtual ~Command() {}; -}; - -class EmptyCommand : public Command -{ - public: - virtual void invoke(CVC4::SmtEngine* smt_engine); -}; - -class AssertCommand: public Command -{ - public: - AssertCommand(const Expr& e); - void invoke(CVC4::SmtEngine* smt_engine); - protected: - Expr d_expr; -}; - -class CheckSatCommand: public Command -{ - public: - CheckSatCommand(); - CheckSatCommand(const Expr& e); - void invoke(CVC4::SmtEngine* smt); - protected: - Expr d_expr; -}; - -class QueryCommand: public Command -{ - public: - QueryCommand(const Expr& e); - void invoke(CVC4::SmtEngine* smt); - protected: - Expr d_expr; -}; - -class CommandSequence: public Command -{ - public: - CommandSequence(); - CommandSequence(Command* cmd); - ~CommandSequence(); - void invoke(CVC4::SmtEngine* smt); - void addCommand(Command* cmd); - private: - /** All the commands to be executed (in sequence) */ - std::vector d_command_sequence; - /** Next command to be executed */ - unsigned int d_last_index; -}; +#include + +#include "cvc4_config.h" +#include "expr/expr.h" +#include "util/result.h" + +namespace CVC4 { + class SmtEngine; + class Command; + class Expr; +}/* 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; +} + +namespace CVC4 { + +class CVC4_PUBLIC Command { +public: + virtual Result 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"; } +};/* class EmptyCommand */ + + +class CVC4_PUBLIC AssertCommand : public Command { +protected: + Expr d_expr; +public: + AssertCommand(const Expr& e); + Result invoke(CVC4::SmtEngine* smt_engine); + void toString(std::ostream& out) const { out << "Assert(" << d_expr << ")"; } +};/* class AssertCommand */ + + +class CVC4_PUBLIC CheckSatCommand : public Command { +public: + CheckSatCommand(); + CheckSatCommand(const Expr& e); + Result invoke(SmtEngine* smt); + void toString(std::ostream& out) const { out << "CheckSat(" << d_expr << ")"; } +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 << ")"; } +protected: + Expr d_expr; +};/* class QueryCommand */ + + +class CVC4_PUBLIC CommandSequence : public Command { +public: + CommandSequence(); + CommandSequence(Command* cmd); + ~CommandSequence(); + Result invoke(SmtEngine* smt); + void addCommand(Command* cmd); + void toString(std::ostream& out) const { + out << "CommandSequence("; + for(std::vector::const_iterator i = d_command_sequence.begin(); + i != d_command_sequence.end(); + ++i) { + out << *i; + if(i != d_command_sequence.end()) + out << " ; "; + } + out << ")"; + } +private: + /** All the commands to be executed (in sequence) */ + std::vector d_command_sequence; + /** Next command to be executed */ + unsigned int d_last_index; +};/* class CommandSequence */ }/* CVC4 namespace */ +inline std::ostream& std::operator<<(std::ostream& out, const CVC4::Command* c) { + if(c) + c->toString(out); + else out << "(null)"; + return out; +} + #endif /* __CVC4__COMMAND_H */ diff --git a/src/util/output.h b/src/util/output.h index 4d3752849..21b7b6e4c 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -20,7 +20,6 @@ namespace CVC4 { - class Debug { std::set d_tags; std::ostream &d_out; @@ -30,19 +29,23 @@ public: static void operator()(const char* tag, std::string); static void operator()(string tag, const char*); static void operator()(string tag, std::string); + static void operator()(const char*);// Yeting option + static void operator()(std::string);// Yeting option static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); static void printf(const char* tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); static void printf(std::string tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); + // Yeting option not possible here static std::ostream& operator()(const char* tag); static std::ostream& operator()(std::string tag); + static std::ostream& operator()();// Yeting option - static void on (const char* tag) { d_tags.insert(std::string(tag)); }; - static void on (std::string tag) { d_tags.insert(tag); }; - static void off(const char* tag) { d_tags.erase (std::string(tag)); }; - static void off(std::string tag) { d_tags.erase (tag); }; + static void on (const char* tag) { d_tags.insert(std::string(tag)); } + static void on (std::string tag) { d_tags.insert(tag); } + static void off(const char* tag) { d_tags.erase (std::string(tag)); } + static void off(std::string tag) { d_tags.erase (tag); } static void setStream(std::ostream& os) { d_out = os; } };/* class Debug */ diff --git a/src/util/result.h b/src/util/result.h index 1e2b61738..8d9b93a1e 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -50,9 +50,11 @@ private: enum Validity d_validity; enum { TYPE_SAT, TYPE_VALIDITY } d_which; + friend std::ostream& CVC4::operator<<(std::ostream& out, Result r); + public: - Result(enum SAT); - Result(enum Validity); + Result(enum SAT s) : d_sat(s), d_validity(VALIDITY_UNKNOWN), d_which(TYPE_SAT) {} + Result(enum Validity v) : d_sat(SAT_UNKNOWN), d_validity(v), d_which(TYPE_VALIDITY) {} enum SAT isSAT(); enum Validity isValid(); @@ -60,6 +62,24 @@ public: };/* class Result */ +inline std::ostream& operator<<(std::ostream& out, Result r) { + if(r.d_which == Result::TYPE_SAT) { + switch(r.d_sat) { + case Result::UNSAT: out << "UNSAT"; break; + case Result::SAT: out << "SAT"; break; + case Result::SAT_UNKNOWN: out << "SAT_UNKNOWN"; break; + } + } else { + switch(r.d_validity) { + case Result::INVALID: out << "INVALID"; break; + case Result::VALID: out << "VALID"; break; + case Result::VALIDITY_UNKNOWN: out << "VALIDITY_UNKNOWN"; break; + } + } + + return out; +} + }/* CVC4 namespace */ #endif /* __CVC4__RESULT_H */ -- 2.30.2