4 files changed, 27 insertions, 5 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 2ff107068..919214f9b 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -184,7 +184,7 @@ public:
   const NodeCache& getNodeCache() const {
     return d_nodeCache;
   }
-}; /* class CnfStream */
+};/* class CnfStream */
 
 /**
  * TseitinCnfStream is based on the following recursive algorithm
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index c49d5f38a..961a18bdb 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -130,6 +130,20 @@ Result PropEngine::checkSat() {
   return Result(result ? Result::SAT : Result::UNSAT);
 }
 
+Node PropEngine::getValue(TNode node) {
+  Assert(node.getKind() == kind::VARIABLE &&
+         node.getType().isBoolean());
+  SatLiteralValue v = d_satSolver->value(d_cnfStream->getLiteral(node));
+  if(v == l_True) {
+    return NodeManager::currentNM()->mkConst(true);
+  } else if(v == l_False) {
+    return NodeManager::currentNM()->mkConst(false);
+  } else {
+    Assert(v == l_Undef);
+    return Node::null();
+  }
+}
+
 void PropEngine::push() {
   Assert(!d_inCheckSat, "Sat solver in solve()!");
   Debug("prop") << "push()" << endl;
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index c33982ddc..7eb903180 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -114,6 +114,14 @@ public:
   Result checkSat();
 
   /**
+   * Get the value of a boolean variable.
+   *
+   * @return mkConst<true>, mkConst<false>, or Node::null() if
+   * unassigned.
+   */
+  Node getValue(TNode node);
+
+  /**
    * Push the context level.
    */
   void push();
diff --git a/src/prop/sat.h b/src/prop/sat.h
index d780230a8..776895b4c 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -89,9 +89,9 @@ inline std::string stringOfLiteralValue(SatLiteralValue val) {
 }
 #endif /* __CVC4_USE_MINISAT */
 
-/** Interface encapsulating the "input" to the solver, e.g., from the 
- * CNF converter. 
- * 
+/** Interface encapsulating the "input" to the solver, e.g., from the
+ * CNF converter.
+ *
  * TODO: Is it possible to push the typedefs of SatClause and SatVariable
  * into here, somehow?
  */
@@ -226,7 +226,7 @@ public:
   void setCnfStream(CnfStream* cnfStream);
 
   SatLiteralValue value(SatLiteral l);
-};
+};/* class SatSolver */
 
 /* Functions that delegate to the concrete SAT solver. */