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.

2 files changed, 12 insertions, 35 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&) */
 
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;
   }