Make d_result in DE context dependent

(fixes bugs in bv, others with JH on)

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index b1ecabf813cdb75af3cdd8433971accebdbb7c4b..b38b3c1e0a633b9cab21409671cad00f54c0d11a 100644 (file)
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -37,7 +37,7 @@ namespace CVC4 {
   d_satSolver(NULL),
   d_satContext(sc),
   d_userContext(uc),
-  d_result(SAT_VALUE_UNKNOWN)
+  d_result(sc, SAT_VALUE_UNKNOWN)
 {
   const Options* options = Options::current();
   Trace("decision") << "Creating decision engine" << std::endl;

diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index fb6f673d936eddd344473a9b57a57764ae50e481..e19307170694c6d0095c8ed98601f0ecb96a7a1f 100644 (file)
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -50,10 +50,12 @@ class DecisionEngine {
 
   context::Context* d_satContext;
   context::Context* d_userContext;
-  SatValue d_result;
+
+  // Does decision engine know the answer?
+  context::CDO<SatValue> d_result;
 
   // Disable creating decision engine without required parameters
-  DecisionEngine() {}
+  DecisionEngine() : d_result(NULL) {}
 public:
   // Necessary functions
 
@@ -128,7 +130,7 @@ public:
 
   /** */
   Result getResult() {
-    switch(d_result) {
+    switch(d_result.get()) {
     case SAT_VALUE_TRUE: return Result(Result::SAT);
     case SAT_VALUE_FALSE: return Result(Result::UNSAT);
     case SAT_VALUE_UNKNOWN: return Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);