parsing/expr/command/result/various other fixes

1 files changed, 22 insertions, 2 deletions

diff --git a/src/util/result.h b/src/util/result.h
index 1e2b61738..8d9b93a1e 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -50,9 +50,11 @@ private:
   enum Validity d_validity;
   enum { TYPE_SAT, TYPE_VALIDITY } d_which;
 
+  friend std::ostream& CVC4::operator<<(std::ostream& out, Result r);
+
 public:
-  Result(enum SAT);
-  Result(enum Validity);
+  Result(enum SAT s) : d_sat(s), d_validity(VALIDITY_UNKNOWN), d_which(TYPE_SAT) {}
+  Result(enum Validity v) : d_sat(SAT_UNKNOWN), d_validity(v), d_which(TYPE_VALIDITY) {}
 
   enum SAT isSAT();
   enum Validity isValid();
@@ -60,6 +62,24 @@ public:
 
 };/* class Result */
 
+inline std::ostream& operator<<(std::ostream& out, 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 << "SAT_UNKNOWN"; break;
+    }
+  } else {
+    switch(r.d_validity) {
+    case Result::INVALID: out << "INVALID"; break;
+    case Result::VALID: out << "VALID"; break;
+    case Result::VALIDITY_UNKNOWN: out << "VALIDITY_UNKNOWN"; break;
+    }
+  }
+
+  return out;
+}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__RESULT_H */