diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-03 22:20:25 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-03 22:20:25 +0000 |
commit | 64d530e5b9096e66398f92d93cf7bc4268df0e70 (patch) | |
tree | 189d63541053faca0c778b0c92d84db8d2b1e0ff /src/util | |
parent | 842fd54de1da122f4c7274796550c2fe21c11db2 (diff) |
Addressed many of the concerns of bug 10 (build system code review).
Some parts split into other bugs: 19, 20, 21.
Addressed concerns of bug 11 (util package code review).
Slight parser source file modifications: file comments, #included
headers in generated parsers/lexers
Added CVC4::Result propagation back through
MiniSat->PropEngine->SmtEngine->main(). Silenced MiniSat when
verbosity is not requested.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Assert.h | 10 | ||||
-rw-r--r-- | src/util/command.cpp | 141 | ||||
-rw-r--r-- | src/util/command.h | 198 | ||||
-rw-r--r-- | src/util/output.cpp | 2 | ||||
-rw-r--r-- | src/util/output.h | 35 | ||||
-rw-r--r-- | src/util/result.h | 66 |
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) { |