2 files changed, 44 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 */
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 */