diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/command.cpp | 2 | ||||
-rw-r--r-- | src/printer/printer.cpp | 35 | ||||
-rw-r--r-- | src/printer/printer.h | 10 | ||||
-rw-r--r-- | src/util/result.cpp | 34 | ||||
-rw-r--r-- | src/util/result.h | 13 |
5 files changed, 57 insertions, 37 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 7dd9df69a..78d04f000 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -1100,7 +1100,7 @@ std::ostream& operator<<(std::ostream& out, return out << "unknown"; default: - return out << "SetBenchmarkStatusCommand::[UNKNOWNSTATUS!]"; + return out << "BenchmarkStatus::[UNKNOWNSTATUS!]"; } } diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index e3b2ed796..cde063584 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -48,7 +48,40 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() { default: Unhandled(lang); } - }/* Printer::makePrinter() */ +void Printer::toStream(std::ostream& out, const Result& r) const throw() { + if(r.getType() == Result::TYPE_SAT) { + switch(r.isSat()) { + case Result::UNSAT: + out << "unsat"; + break; + case Result::SAT: + out << "sat"; + break; + case Result::SAT_UNKNOWN: + out << "unknown"; + if(r.whyUnknown() != Result::UNKNOWN_REASON) { + out << " (" << r.whyUnknown() << ")"; + } + break; + } + } else { + switch(r.isValid()) { + case Result::INVALID: + out << "invalid"; + break; + case Result::VALID: + out << "valid"; + break; + case Result::VALIDITY_UNKNOWN: + out << "unknown"; + if(r.whyUnknown() != Result::UNKNOWN_REASON) { + out << " (" << r.whyUnknown() << ")"; + } + break; + } + } +}/* Printer::toStream() */ + }/* CVC4 namespace */ diff --git a/src/printer/printer.h b/src/printer/printer.h index 9bcbba3b0..04b435060 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -62,6 +62,16 @@ public: /** Write a CommandStatus out to a stream with this Printer. */ virtual void toStream(std::ostream& out, const CommandStatus* s) const throw() = 0; + /** + * Write a Result out to a stream with this Printer. + * + * The default implementation writes a reasonable string in lowercase + * for sat, unsat, valid, invalid, or unknown results. This behavior + * is overridable by each Printer, since sometimes an output language + * has a particular preference for how results should appear. + */ + virtual void toStream(std::ostream& out, const Result& r) const throw(); + };/* class Printer */ }/* CVC4 namespace */ diff --git a/src/util/result.cpp b/src/util/result.cpp index bdb17f54c..84e422c19 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -23,6 +23,7 @@ #include "util/result.h" #include "util/Assert.h" +#include "printer/printer.h" using namespace std; @@ -190,38 +191,7 @@ ostream& operator<<(ostream& out, } ostream& operator<<(ostream& out, const 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 << "unknown"; - if(r.whyUnknown() != Result::UNKNOWN_REASON) { - out << " (" << r.whyUnknown() << ")"; - } - break; - } - } else { - switch(r.d_validity) { - case Result::INVALID: - out << "invalid"; - break; - case Result::VALID: - out << "valid"; - break; - case Result::VALIDITY_UNKNOWN: - out << "unknown"; - if(r.whyUnknown() != Result::UNKNOWN_REASON) { - out << " (" << r.whyUnknown() << ")"; - } - break; - } - } - + Printer::getPrinter(Node::setlanguage::getLanguage(out))->toStream(out, r); return out; }/* operator<<(ostream&, const Result&) */ diff --git a/src/util/result.h b/src/util/result.h index ac52ee382..f0cf3f20e 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -55,6 +55,12 @@ public: VALIDITY_UNKNOWN = 2 }; + enum Type { + TYPE_SAT, + TYPE_VALIDITY, + TYPE_NONE + }; + enum UnknownExplanation { REQUIRES_FULL_CHECK, INCOMPLETE, @@ -71,11 +77,9 @@ public: private: enum Sat d_sat; enum Validity d_validity; - enum { TYPE_SAT, TYPE_VALIDITY, TYPE_NONE } d_which; + enum Type d_which; enum UnknownExplanation d_unknownExplanation; - friend std::ostream& CVC4::operator<<(std::ostream& out, const Result& r); - public: Result() : d_sat(SAT_UNKNOWN), @@ -126,6 +130,9 @@ public: bool isUnknown() const { return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN; } + Type getType() const { + return d_which; + } bool isNull() const { return d_which == TYPE_NONE; } |