summaryrefslogtreecommitdiff
path: root/src/theory/valuation.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/valuation.cpp')
-rw-r--r--src/theory/valuation.cpp20
1 files changed, 20 insertions, 0 deletions
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:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback