diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-08 21:21:42 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-08 21:21:42 +0000 |
commit | 58372a2ad23298810ae886a16db3c57f9df251af (patch) | |
tree | 7dd58f171e5b972f883a106f404aba989065c179 /src/util/result.cpp | |
parent | f1b4a985be64e08b1a440b1eaf75d3f8e2105d01 (diff) |
Extend Printer infrastructure also to the "Result" class, meaning that different output languages can write "sat", "unsat", etc., in different ways. No output is changed by this commit, but the flexibility is added that Francois wanted at today's meeting.
Diffstat (limited to 'src/util/result.cpp')
-rw-r--r-- | src/util/result.cpp | 34 |
1 files changed, 2 insertions, 32 deletions
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&) */ |