Print function for equality status. (#1826)

diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 7151b4aaf554efb746e5d51e82aa66e370c465c2..0056fb22f0454944dc5da35480f21e1b48782821 100644 (file)
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -22,6 +22,26 @@
 namespace CVC4 {
 namespace theory {
 
+std::ostream& operator<<(std::ostream& os, EqualityStatus s)
+{
+  switch (s)
+  {
+    case EQUALITY_TRUE_AND_PROPAGATED:
+      os << "EQUALITY_TRUE_AND_PROPAGATED";
+      break;
+    case EQUALITY_FALSE_AND_PROPAGATED:
+      os << "EQUALITY_FALSE_AND_PROPAGATED";
+      break;
+    case EQUALITY_TRUE: os << "EQUALITY_TRUE"; break;
+    case EQUALITY_FALSE: os << "EQUALITY_FALSE"; break;
+    case EQUALITY_TRUE_IN_MODEL: os << "EQUALITY_TRUE_IN_MODEL"; break;
+    case EQUALITY_FALSE_IN_MODEL: os << "EQUALITY_FALSE_IN_MODEL"; break;
+    case EQUALITY_UNKNOWN: os << "EQUALITY_UNKNOWN"; break;
+    default: Unhandled(); break;
+  }
+  return os;
+}
+
 bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2) {
   switch (s1) {
   case EQUALITY_TRUE:

diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index e78a629e1ca5c7ccf0a2e164634a8c7c39444691..160a7b970d2fce9ae36b29c9c9aade733bdd1c06 100644 (file)
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -54,6 +54,8 @@ enum EqualityStatus {
   EQUALITY_UNKNOWN
 };/* enum EqualityStatus */
 
+std::ostream& operator<<(std::ostream& os, EqualityStatus s);
+
 /**
  * Returns true if the two statuses are compatible, i.e. both TRUE
  * or both FALSE (regardless of inmodel/propagation).