summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Makefile.am6
-rw-r--r--src/expr/expr.cpp8
-rw-r--r--src/expr/expr.h57
-rw-r--r--src/expr/expr_builder.h29
-rw-r--r--src/expr/expr_manager.h49
-rw-r--r--src/expr/expr_value.cpp2
-rw-r--r--src/expr/expr_value.h6
-rw-r--r--src/expr/kind.h36
-rw-r--r--src/main/Makefile.am2
-rw-r--r--src/main/getopt.cpp2
-rw-r--r--src/main/main.cpp36
-rw-r--r--src/parser/Makefile.am6
-rw-r--r--src/parser/parser.cpp44
-rw-r--r--src/parser/parser.h107
-rw-r--r--src/parser/parser_state.cpp46
-rw-r--r--src/parser/parser_state.h384
-rw-r--r--src/parser/pl.ypp49
-rw-r--r--src/parser/pl_scanner.lpp27
-rw-r--r--src/parser/smtlib.ypp37
-rw-r--r--src/parser/smtlib_scanner.lpp10
-rw-r--r--src/smt/smt_engine.cpp47
-rw-r--r--src/smt/smt_engine.h11
-rw-r--r--src/util/command.cpp66
-rw-r--r--src/util/command.h158
-rw-r--r--src/util/output.h13
-rw-r--r--src/util/result.h24
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 <vector>
+#include <iostream>
#include <stdint.h>
#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 <vector>
+#include <cstdlib>
+
#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 <vector>
+#include <map>
+
#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<uint64_t, std::vector<Expr> > 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<Expr> v;
+ v.push_back(e);
+ d_hash.insert(std::make_pair(hash, v));
+ return e;
+ } else {
+ for(std::vector<Expr>::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<Expr> 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 <iostream>
+
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 <iostream>
-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 <string>
#include <iostream>
-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 <vector>
#include <iostream>
-#include "cvc4.h"
+#include <map>
+#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<CVC4::Expr>& 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<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 = &in; }
+
+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 */
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 <list>
#include <vector>
#include <string>
+#include <ostream>
+#include <sstream>
#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<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 {
- $$ = 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; res<size && buf[res] != 0; res++);
- if(res == size) PLerror("Lexer bug: overfilled the buffer");
+ 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';
@@ -74,8 +78,7 @@ static int PLinput(std::istream& is, char* buf, int size) {
}
// Redefine the input buffer function to read from an istream
-#define YY_INPUT(buf,result,max_size) \
- result = PLinput(*CVC4::parser::parserState->is, 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; }
<COMMENT>"\n" { BEGIN INITIAL; /* return to normal mode */
- CVC4::parser::parserState->lineNum++; }
+ CVC4::parser::_global_parser_state->increaseLineNumber(); }
<COMMENT>. { /* stay in comment mode */ }
<INITIAL>"\"" { 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 <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;
@@ -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 <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;
-}
+ 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<Expr>::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 <vector>
+
+#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<Expr> d_assertList;
+ std::vector<Expr> 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<Command*> d_command_sequence;
- /** Next command to be executed */
- unsigned int d_last_index;
-};
+#include <iostream>
+
+#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<Command*>::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<Command*> 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<std::string> 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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback