summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/Assert.h10
-rw-r--r--src/util/command.cpp141
-rw-r--r--src/util/command.h198
-rw-r--r--src/util/output.cpp2
-rw-r--r--src/util/output.h35
-rw-r--r--src/util/result.h66
6 files changed, 298 insertions, 154 deletions
diff --git a/src/util/Assert.h b/src/util/Assert.h
index d8e881613..fa05ecaa5 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -17,6 +17,7 @@
#define __CVC4__ASSERT_H
#include <string>
+#include <sstream>
#include <cstdio>
#include <cstdarg>
#include "util/exception.h"
@@ -35,9 +36,11 @@ protected:
construct(header, extra, function, file, line, fmt, args);
va_end(args);
}
+
void construct(const char* header, const char* extra,
const char* function, const char* file,
unsigned line, const char* fmt, va_list args);
+
void construct(const char* header, const char* extra,
const char* function, const char* file,
unsigned line);
@@ -99,11 +102,14 @@ public:
va_end(args);
}
+ template <class T>
UnhandledCaseException(const char* function, const char* file,
- unsigned line, int theCase) :
+ unsigned line, T theCase) :
UnreachableCodeException() {
+ std::stringstream sb;
+ sb << theCase;
construct("Unhandled case encountered",
- NULL, function, file, line, "The case was: %d", theCase);
+ NULL, function, file, line, "The case was: %s", sb.str().c_str());
}
UnhandledCaseException(const char* function, const char* file,
diff --git a/src/util/command.cpp b/src/util/command.cpp
index 90204a63f..f5a694a73 100644
--- a/src/util/command.cpp
+++ b/src/util/command.cpp
@@ -10,30 +10,16 @@
** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** [[ Add file-specific comments here ]]
+ ** Implementation of command objects.
**/
-/*
- * command.cpp
- *
- * Created on: Nov 25, 2009
- * Author: dejan
- */
-
-#include <sstream>
#include "util/command.h"
-#include "util/Assert.h"
#include "smt/smt_engine.h"
using namespace std;
namespace CVC4 {
-ostream& operator<<(ostream& out, const Command& c) {
- c.toStream(out);
- return out;
-}
-
ostream& operator<<(ostream& out, const Command* c) {
if (c == NULL) {
out << "null";
@@ -43,99 +29,35 @@ ostream& operator<<(ostream& out, const Command* c) {
return out;
}
-std::string Command::toString() const {
- stringstream ss;
- toStream(ss);
- return ss.str();
-}
-
-EmptyCommand::EmptyCommand(string name) :
- d_name(name) {
-}
-
-void EmptyCommand::invoke(SmtEngine* smt_engine) {
-}
-
-AssertCommand::AssertCommand(const BoolExpr& e) :
- d_expr(e) {
-}
-
-void AssertCommand::invoke(SmtEngine* smt_engine) {
- smt_engine->assertFormula(d_expr);
-}
-
-CheckSatCommand::CheckSatCommand() {
-}
-
-CheckSatCommand::CheckSatCommand(const BoolExpr& e) :
- d_expr(e) {
-}
-
-void CheckSatCommand::invoke(SmtEngine* smt_engine) {
- smt_engine->checkSat(d_expr);
-}
-
-QueryCommand::QueryCommand(const BoolExpr& e) :
- d_expr(e) {
-}
-
-void QueryCommand::invoke(CVC4::SmtEngine* smt_engine) {
- smt_engine->query(d_expr);
-}
-
-CommandSequence::CommandSequence() :
- d_last_index(0) {
-}
-
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);
- delete d_command_sequence[d_last_index];
+ for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
+ delete d_commandSequence[i];
}
}
-void CommandSequence::addCommand(Command* cmd) {
- d_command_sequence.push_back(cmd);
-}
-
-void EmptyCommand::toStream(ostream& out) const {
- out << "EmptyCommand(" << d_name << ")";
-}
-
-void AssertCommand::toStream(ostream& out) const {
- out << "Assert(" << d_expr << ")";
+void CommandSequence::invoke(SmtEngine* smtEngine) {
+ for(; d_index < d_commandSequence.size(); ++d_index) {
+ d_commandSequence[d_index]->invoke(smtEngine);
+ delete d_commandSequence[d_index];
+ }
}
void CheckSatCommand::toStream(ostream& out) const {
- if(d_expr.isNull())
+ if(d_expr.isNull()) {
out << "CheckSat()";
- else
+ } else {
out << "CheckSat(" << d_expr << ")";
-}
-
-void QueryCommand::toStream(ostream& out) const {
- out << "Query(";
- d_expr.printAst(out, 0);
- out << ")";
+ }
}
void CommandSequence::toStream(ostream& out) const {
out << "CommandSequence[" << endl;
- for(unsigned i = d_last_index; i < d_command_sequence.size(); ++i) {
- out << *d_command_sequence[i] << endl;
+ for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
+ out << *d_commandSequence[i] << endl;
}
out << "]";
}
-DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids) :
- d_declaredSymbols(ids) {
-}
-
void DeclarationCommand::toStream(std::ostream& out) const {
out << "Declare(";
bool first = true;
@@ -149,41 +71,4 @@ void DeclarationCommand::toStream(std::ostream& out) const {
out << ")";
}
-SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) :
- d_status(status) {
-}
-
-void SetBenchmarkStatusCommand::invoke(SmtEngine* smt) {
- // TODO: something to be done with the status
-}
-
-void SetBenchmarkStatusCommand::toStream(std::ostream& out) const {
- out << "SetBenchmarkStatus(";
- switch(d_status) {
- case SMT_SATISFIABLE:
- out << "sat";
- break;
- case SMT_UNSATISFIABLE:
- out << "unsat";
- break;
- case SMT_UNKNOWN:
- out << "unknown";
- break;
- default:
- Unhandled("Unknown benchmark status");
- }
- out << ")";
-}
-
-SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(string logic) : d_logic(logic)
- {}
-
-void SetBenchmarkLogicCommand::invoke(SmtEngine* smt) {
- // TODO: something to be done with the logic
-}
-
-void SetBenchmarkLogicCommand::toStream(std::ostream& out) const {
- out << "SetBenchmarkLogic(" << d_logic << ")";
-}
-
}/* CVC4 namespace */
diff --git a/src/util/command.h b/src/util/command.h
index 57edfea01..15104a5ea 100644
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -10,26 +10,30 @@
** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** Implementation of the command pattern on SmtEngines. Generated by
- ** the parser.
+ ** Implementation of the command pattern on SmtEngines. Command
+ ** objects are generated by the parser (typically) to implement the
+ ** commands in parsed input (see Parser::parseNextCommand()), or by
+ ** client code.
**/
#ifndef __CVC4__COMMAND_H
#define __CVC4__COMMAND_H
#include <iostream>
+#include <sstream>
+#include <string>
+#include <vector>
#include "cvc4_config.h"
#include "expr/expr.h"
+#include "util/result.h"
namespace CVC4 {
- class SmtEngine;
- class Command;
-}/* CVC4 namespace */
-namespace CVC4 {
+class SmtEngine;
+class Command;
-std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC;
class CVC4_PUBLIC Command {
@@ -49,7 +53,6 @@ private:
std::string d_name;
};/* class EmptyCommand */
-
class CVC4_PUBLIC AssertCommand : public Command {
public:
AssertCommand(const BoolExpr& e);
@@ -59,7 +62,6 @@ protected:
BoolExpr d_expr;
};/* class AssertCommand */
-
class CVC4_PUBLIC DeclarationCommand : public EmptyCommand {
public:
DeclarationCommand(const std::vector<std::string>& ids);
@@ -73,22 +75,24 @@ public:
CheckSatCommand();
CheckSatCommand(const BoolExpr& e);
void invoke(SmtEngine* smt);
+ Result getResult();
void toStream(std::ostream& out) const;
protected:
BoolExpr d_expr;
+ Result d_result;
};/* class CheckSatCommand */
-
class CVC4_PUBLIC QueryCommand : public Command {
public:
QueryCommand(const BoolExpr& e);
void invoke(SmtEngine* smt);
+ Result getResult();
void toStream(std::ostream& out) const;
protected:
BoolExpr d_expr;
+ Result d_result;
};/* class QueryCommand */
-
class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
public:
/** The status an SMT benchmark can have */
@@ -105,7 +109,11 @@ public:
void toStream(std::ostream& out) const;
protected:
BenchmarkStatus d_status;
-};/* class QueryCommand */
+};/* class SetBenchmarkStatusCommand */
+
+inline std::ostream& operator<<(std::ostream& out,
+ SetBenchmarkStatusCommand::BenchmarkStatus bs)
+ CVC4_PUBLIC;
class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
public:
@@ -114,9 +122,7 @@ public:
void toStream(std::ostream& out) const;
protected:
std::string d_logic;
-};/* class QueryCommand */
-
-
+};/* class SetBenchmarkLogicCommand */
class CVC4_PUBLIC CommandSequence : public Command {
public:
@@ -125,13 +131,171 @@ public:
void invoke(SmtEngine* smt);
void addCommand(Command* cmd);
void toStream(std::ostream& out) const;
+
+ typedef std::vector<Command*>::iterator iterator;
+ typedef std::vector<Command*>::const_iterator const_iterator;
+
+ const_iterator begin() const { return d_commandSequence.begin(); }
+ const_iterator end() const { return d_commandSequence.end(); }
+
+ iterator begin() { return d_commandSequence.begin(); }
+ iterator end() { return d_commandSequence.end(); }
+
private:
/** All the commands to be executed (in sequence) */
- std::vector<Command*> d_command_sequence;
+ std::vector<Command*> d_commandSequence;
/** Next command to be executed */
- unsigned int d_last_index;
+ unsigned int d_index;
};/* class CommandSequence */
}/* CVC4 namespace */
+/* =========== inline function definitions =========== */
+
+#include "smt/smt_engine.h"
+
+namespace CVC4 {
+
+inline std::ostream& operator<<(std::ostream& out, const Command& c) {
+ c.toStream(out);
+ return out;
+}
+
+/* class Command */
+
+inline std::string Command::toString() const {
+ std::stringstream ss;
+ toStream(ss);
+ return ss.str();
+}
+
+/* class EmptyCommand */
+
+inline EmptyCommand::EmptyCommand(std::string name) :
+ d_name(name) {
+}
+
+inline void EmptyCommand::invoke(SmtEngine* smt_engine) {
+}
+
+inline void EmptyCommand::toStream(std::ostream& out) const {
+ out << "EmptyCommand(" << d_name << ")";
+}
+
+/* class AssertCommand */
+
+inline AssertCommand::AssertCommand(const BoolExpr& e) :
+ d_expr(e) {
+}
+
+inline void AssertCommand::invoke(SmtEngine* smt_engine) {
+ smt_engine->assertFormula(d_expr);
+}
+
+inline void AssertCommand::toStream(std::ostream& out) const {
+ out << "Assert(" << d_expr << ")";
+}
+
+/* class CheckSatCommand */
+
+inline CheckSatCommand::CheckSatCommand() {
+}
+
+inline CheckSatCommand::CheckSatCommand(const BoolExpr& e) :
+ d_expr(e) {
+}
+
+inline void CheckSatCommand::invoke(SmtEngine* smt_engine) {
+ d_result = smt_engine->checkSat(d_expr);
+}
+
+inline Result CheckSatCommand::getResult() {
+ return d_result;
+}
+
+/* class QueryCommand */
+
+inline QueryCommand::QueryCommand(const BoolExpr& e) :
+ d_expr(e) {
+}
+
+inline void QueryCommand::invoke(CVC4::SmtEngine* smt_engine) {
+ d_result = smt_engine->query(d_expr);
+}
+
+inline Result QueryCommand::getResult() {
+ return d_result;
+}
+
+inline void QueryCommand::toStream(std::ostream& out) const {
+ out << "Query(";
+ d_expr.printAst(out, 0);
+ out << ")";
+}
+
+/* class CommandSequence */
+
+inline CommandSequence::CommandSequence() :
+ d_index(0) {
+}
+
+inline void CommandSequence::addCommand(Command* cmd) {
+ d_commandSequence.push_back(cmd);
+}
+
+/* class DeclarationCommand */
+
+inline DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids) :
+ d_declaredSymbols(ids) {
+}
+
+/* class SetBenchmarkStatusCommand */
+
+inline SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus s) :
+ d_status(s) {
+}
+
+inline void SetBenchmarkStatusCommand::invoke(SmtEngine* smt) {
+ // FIXME: TODO: something to be done with the status
+}
+
+inline void SetBenchmarkStatusCommand::toStream(std::ostream& out) const {
+ out << "SetBenchmarkStatus(" << d_status << ")";
+}
+
+/* class SetBenchmarkLogicCommand */
+
+inline SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string l) :
+ d_logic(l) {
+}
+
+inline void SetBenchmarkLogicCommand::invoke(SmtEngine* smt) {
+ // FIXME: TODO: something to be done with the logic
+}
+
+inline void SetBenchmarkLogicCommand::toStream(std::ostream& out) const {
+ out << "SetBenchmarkLogic(" << d_logic << ")";
+}
+
+/* output stream insertion operator for benchmark statuses */
+inline std::ostream& operator<<(std::ostream& out,
+ SetBenchmarkStatusCommand::BenchmarkStatus bs) {
+ switch(bs) {
+
+ case SetBenchmarkStatusCommand::SMT_SATISFIABLE:
+ return out << "sat";
+
+ case SetBenchmarkStatusCommand::SMT_UNSATISFIABLE:
+ return out << "unsat";
+
+ case SetBenchmarkStatusCommand::SMT_UNKNOWN:
+ return out << "unknown";
+
+ default:
+ return out << "SetBenchmarkStatusCommand::[UNKNOWNSTATUS!]";
+ }
+}
+
+}/* CVC4 namespace */
+
#endif /* __CVC4__COMMAND_H */
diff --git a/src/util/output.cpp b/src/util/output.cpp
index 05c74918c..b42fc77be 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -20,6 +20,8 @@
namespace CVC4 {
+/* Definitions of the declared globals from output.h... */
+
null_streambuf null_sb;
std::ostream null_os(&null_sb);
diff --git a/src/util/output.h b/src/util/output.h
index c1e513703..6a6c76d83 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -28,14 +28,28 @@
namespace CVC4 {
+/**
+ * A utility class to provide (essentially) a "/dev/null" streambuf.
+ * If debugging support is compiled in, but debugging for
+ * e.g. "parser" is off, then Debug("parser") returns a stream
+ * attached to a null_streambuf instance so that output is directed to
+ * the bit bucket.
+ */
class null_streambuf : public std::streambuf {
public:
+ /* Overriding overflow() just ensures that EOF isn't returned on the
+ * stream. Perhaps this is not so critical, but recommended; this
+ * way the output stream looks like it's functioning, in a non-error
+ * state. */
int overflow(int c) { return c; }
};/* class null_streambuf */
+/** A null stream-buffer singleton */
extern null_streambuf null_sb;
+/** A null output stream singleton */
extern std::ostream null_os CVC4_PUBLIC;
+/** The debug output class */
class CVC4_PUBLIC DebugC {
std::set<std::string> d_tags;
std::ostream *d_os;
@@ -47,12 +61,9 @@ public:
void operator()(const char* tag, std::string);
void operator()(std::string tag, const char*);
void operator()(std::string tag, std::string);
- //void operator()(const char*);// Yeting option
- //void operator()(std::string);// Yeting option
static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
- // Yeting option not possible here
std::ostream& operator()(const char* tag) {
if(d_tags.find(std::string(tag)) != d_tags.end())
@@ -64,7 +75,11 @@ public:
return *d_os;
else return null_os;
}
- std::ostream& operator()();// Yeting option
+ /**
+ * The "Yeting option" - this allows use of Debug() without a tag
+ * for temporary (file-only) debugging.
+ */
+ std::ostream& operator()();
void on (const char* tag) { d_tags.insert(std::string(tag)); }
void on (std::string tag) { d_tags.insert(tag); }
@@ -74,8 +89,10 @@ public:
void setStream(std::ostream& os) { d_os = &os; }
};/* class Debug */
+/** The debug output singleton */
extern DebugC Debug CVC4_PUBLIC;
+/** The warning output class */
class CVC4_PUBLIC WarningC {
std::ostream *d_os;
@@ -92,8 +109,10 @@ public:
void setStream(std::ostream& os) { d_os = &os; }
};/* class Warning */
+/** The warning output singleton */
extern WarningC Warning CVC4_PUBLIC;
+/** The message output class */
class CVC4_PUBLIC MessageC {
std::ostream *d_os;
@@ -110,8 +129,10 @@ public:
void setStream(std::ostream& os) { d_os = &os; }
};/* class Message */
+/** The message output singleton */
extern MessageC Message CVC4_PUBLIC;
+/** The notice output class */
class CVC4_PUBLIC NoticeC {
std::ostream *d_os;
@@ -128,8 +149,10 @@ public:
void setStream(std::ostream& os) { d_os = &os; }
};/* class Notice */
+/** The notice output singleton */
extern NoticeC Notice CVC4_PUBLIC;
+/** The chat output class */
class CVC4_PUBLIC ChatC {
std::ostream *d_os;
@@ -146,8 +169,10 @@ public:
void setStream(std::ostream& os) { d_os = &os; }
};/* class Chat */
+/** The chat output singleton */
extern ChatC Chat CVC4_PUBLIC;
+/** The trace output class */
class CVC4_PUBLIC TraceC {
std::ostream *d_os;
std::set<std::string> d_tags;
@@ -161,6 +186,7 @@ public:
void operator()(std::string tag, std::string);
void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) {
+ // chop off output after 1024 bytes
char buf[1024];
va_list vl;
va_start(vl, fmt);
@@ -191,6 +217,7 @@ public:
void setStream(std::ostream& os) { d_os = &os; }
};/* class Trace */
+/** The trace output singleton */
extern TraceC Trace CVC4_PUBLIC;
}/* CVC4 namespace */
diff --git a/src/util/result.h b/src/util/result.h
index 87686d59c..d4980c776 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -16,6 +16,8 @@
#ifndef __CVC4__RESULT_H
#define __CVC4__RESULT_H
+#include "util/Assert.h"
+
namespace CVC4 {
// TODO: perhaps best to templatize Result on its Kind (SAT/Validity),
@@ -52,20 +54,78 @@ public:
private:
enum SAT d_sat;
enum Validity d_validity;
- enum { TYPE_SAT, TYPE_VALIDITY } d_which;
+ enum { TYPE_SAT, TYPE_VALIDITY, TYPE_NONE } d_which;
friend std::ostream& CVC4::operator<<(std::ostream& out, Result r);
public:
- 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) {}
+ Result() :
+ d_sat(SAT_UNKNOWN),
+ d_validity(VALIDITY_UNKNOWN),
+ d_which(TYPE_NONE) {
+ }
+ 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();
enum UnknownExplanation whyUnknown();
+ inline Result asSatisfiabilityResult() const;
+ inline Result asValidityResult() const;
+
};/* class Result */
+inline Result Result::asSatisfiabilityResult() const {
+ if(d_which == TYPE_SAT) {
+ return *this;
+ }
+
+ switch(d_validity) {
+
+ case INVALID:
+ return Result(SAT);
+
+ case VALID:
+ return Result(UNSAT);
+
+ case VALIDITY_UNKNOWN:
+ return Result(SAT_UNKNOWN);
+
+ default:
+ Unhandled(d_validity);
+ }
+}
+
+inline Result Result::asValidityResult() const {
+ if(d_which == TYPE_VALIDITY) {
+ return *this;
+ }
+
+ switch(d_sat) {
+
+ case SAT:
+ return Result(INVALID);
+
+ case UNSAT:
+ return Result(VALID);
+
+ case SAT_UNKNOWN:
+ return Result(VALIDITY_UNKNOWN);
+
+ default:
+ Unhandled(d_sat);
+ }
+}
+
inline std::ostream& operator<<(std::ostream& out, Result r) {
if(r.d_which == Result::TYPE_SAT) {
switch(r.d_sat) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback