Merging the unate-propagator branch into the trunk. This is a big update so expect a little turbulence. This commit will not compile. There will be a second commit that fixes this in a moment. I am delaying a change to avoid svn whining about a conflict.

1 files changed, 16 insertions, 0 deletions

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index e06c9594c..5e83d3728 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -103,5 +103,21 @@ Node Theory::get() {
   return fact;
 }
 
+std::ostream& operator<<(std::ostream& os, Theory::Effort level){
+  switch(level){
+  case Theory::MIN_EFFORT:
+    os << "MIN_EFFORT"; break;
+  case Theory::QUICK_CHECK:
+    os << "QUICK_CHECK:"; break;
+  case Theory::STANDARD:
+    os << "STANDARD"; break;
+  case Theory::FULL_EFFORT:
+    os << "FULL_EFFORT"; break;
+  default:
+      Unreachable();
+  }
+  return os;
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */