surprize surprize

2 files changed, 23 insertions, 0 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 7e335a21b..cbec9faea 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -154,6 +154,24 @@ Node PropEngine::getValue(TNode node) {
   }
 }
 
+bool PropEngine::hasValue(TNode node, bool& value) {
+  Assert(node.getType().isBoolean());
+  SatLiteral lit = d_cnfStream->getLiteral(node);
+
+  SatLiteralValue v = d_satSolver->value(lit);
+  if(v == l_True) {
+    value = true;
+    return true;
+  } else if(v == l_False) {
+    value = false;
+    return true;
+  } else {
+    Assert(v == l_Undef);
+    return false;
+  }
+}
+
+
 void PropEngine::push() {
   Assert(!d_inCheckSat, "Sat solver in solve()!");
   d_satSolver->push();
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index e1a1c08d7..f44ad16f7 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -115,6 +115,11 @@ public:
   Node getValue(TNode node);
 
   /**
+   * Check if the node has a value and return it if yes.
+   */
+  bool hasValue(TNode node, bool& value);
+
+  /**
    * Push the context level.
    */
   void push();