Sharing work

1 files changed, 42 insertions, 1 deletions

diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 148b95632..627125a27 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -24,6 +24,38 @@
 namespace CVC4 {
 namespace theory {
 
+bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2) {
+ switch (s1) {
+ case EQUALITY_TRUE:
+ case EQUALITY_TRUE_IN_MODEL:
+ case EQUALITY_TRUE_AND_PROPAGATED:
+   switch (s2) {
+   case EQUALITY_TRUE:
+   case EQUALITY_TRUE_IN_MODEL:
+   case EQUALITY_TRUE_AND_PROPAGATED:
+     return true;
+   default:
+     return false;
+   }
+   break;
+ case EQUALITY_FALSE:
+ case EQUALITY_FALSE_IN_MODEL:
+ case EQUALITY_FALSE_AND_PROPAGATED:
+   switch (s2) {
+   case EQUALITY_FALSE:
+   case EQUALITY_FALSE_IN_MODEL:
+   case EQUALITY_FALSE_AND_PROPAGATED:
+     return true;
+   default:
+     return false;
+   }
+   break;
+ default:
+   return false;
+ }
+}
+
+
 Node Valuation::getValue(TNode n) const {
   return d_engine->getValue(n);
 }
@@ -47,7 +79,16 @@ Node Valuation::getSatValue(TNode n) const {
 }
 
 bool Valuation::hasSatValue(TNode n, bool& value) const {
-  return d_engine->getPropEngine()->hasValue(n, value);
+  Node normalized = Rewriter::rewrite(n);
+  if (d_engine->getPropEngine()->isSatLiteral(normalized)) {
+    return d_engine->getPropEngine()->hasValue(normalized, value);
+  } else {
+    return false;
+  }
+}
+
+EqualityStatus Valuation::getEqualityStatus(TNode a, TNode b) {
+  return d_engine->getEqualityStatus(a, b);
 }
 
 Node Valuation::ensureLiteral(TNode n) {