From 58372a2ad23298810ae886a16db3c57f9df251af Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 8 Jun 2012 21:21:42 +0000
Subject: [PATCH] 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.

---
 src/expr/command.cpp    |  2 +-
 src/printer/printer.cpp | 35 ++++++++++++++++++++++++++++++++++-
 src/printer/printer.h   | 10 ++++++++++
 src/util/result.cpp     | 34 ++--------------------------------
 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;
   }
-- 
2.30.2