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.

1 files changed, 34 insertions, 1 deletions

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 */