From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 27 Apr 2018 23:45:58 +0000 (-0500)
Subject: Print function for equality status. (#1826)
X-Git-Tag: cvc5-1.0.0~5117
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5b2c33bf0bd968b970d5f228f291477d20b751df;p=cvc5.git

Print function for equality status. (#1826)
---

diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 7151b4aaf..0056fb22f 100644
--- 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 e78a629e1..160a7b970 100644
--- 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).