Fixes to Valuation.

3 files changed, 19 insertions, 3 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index d64aadc96..44709630d 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -104,7 +104,7 @@ void PropEngine::printSatisfyingAssignment(){
     SatLiteral l = curr.second.literal;
     if(!sign(l)) {
       Node n = curr.first;
-      SatLiteralValue value = d_satSolver->value(l);
+      SatLiteralValue value = d_satSolver->modelValue(l);
       Debug("prop-value") << "'" << l << "' " << value << " " << n << endl;
     }
   }
@@ -138,7 +138,9 @@ Result PropEngine::checkSat() {
 
 Node PropEngine::getValue(TNode node) {
   Assert(node.getType().isBoolean());
-  SatLiteralValue v = d_satSolver->value(d_cnfStream->getLiteral(node));
+  SatLiteral lit = d_cnfStream->getLiteral(node);
+
+  SatLiteralValue v = d_satSolver->value(lit);
   if(v == l_True) {
     return NodeManager::currentNM()->mkConst(true);
   } else if(v == l_False) {
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 88df366e2..f9e135c0d 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -232,8 +232,12 @@ public:
 
   void setCnfStream(CnfStream* cnfStream);
 
+  /** Call value() during the search.*/
   SatLiteralValue value(SatLiteral l);
 
+  /** Call value() when the search is done.*/
+  SatLiteralValue modelValue(SatLiteral l);
+
   int getLevel() const;
 
   void push();
@@ -294,6 +298,10 @@ inline SatVariable SatSolver::newVar(bool theoryAtom) {
 }
 
 inline SatLiteralValue SatSolver::value(SatLiteral l) {
+  return d_minisat->value(l);
+}
+
+inline SatLiteralValue SatSolver::modelValue(SatLiteral l) {
   return d_minisat->modelValue(l);
 }
 
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 1f82f1404..9f33c2c4f 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -29,7 +29,13 @@ Node Valuation::getValue(TNode n) {
 
 Node Valuation::getSatValue(TNode n) {
   if(n.getKind() == kind::NOT) {
-    return NodeManager::currentNM()->mkConst(! d_engine->getPropEngine()->getValue(n[0]).getConst<bool>());
+    Node atomRes = d_engine->getPropEngine()->getValue(n[0]);
+    if(atomRes.getKind() == kind::CONST_BOOLEAN){
+      return NodeManager::currentNM()->mkConst(!atomRes.getConst<bool>());
+    }else{
+      Assert(atomRes.isNull());
+      return atomRes;
+    }
   } else {
     return d_engine->getPropEngine()->getValue(n);
   }