From 846de1aa9b4a34d1af657dc43cf22641abb06f2e Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Wed, 13 Jun 2012 15:31:38 +0000 Subject: [PATCH] Make d_result in DE context dependent (fixes bugs in bv, others with JH on) --- src/decision/decision_engine.cpp | 2 +- src/decision/decision_engine.h | 8 +++++--- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index b1ecabf81..b38b3c1e0 100644 --- 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 fb6f673d9..e19307170 100644 --- 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 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); -- 2.30.2