cleanup of exit mechanism when decisionEngine is on\n\n fixes some bugs we were seein...

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 697ab4853589ee44fd667b182f2cb6ff3245269a..9aefda75af9a2df4f4fd573e682764339c5248ca 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1100,12 +1100,6 @@ lbool Solver::search(int nof_conflicts)
                 continue;
               } else {
                 // Yes, we're truly satisfiable
-               if(decisionEngineDone) {
-                 // but we might know that only because of decision engine
-                 Trace("decision") << decisionEngineDone << " decision engine stopping us" << std::endl;
-                 interrupt();
-                 return l_Undef;
-               }
                 return l_True;
               }
             } else if (check_type == CHECK_FINAL_FAKE) {

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 65274955730c24216471bf39454ad2eab4d12e82..7cac970f8be795d4221fd5736512519f735d64fc 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -266,8 +266,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
   d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
   d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
-  d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
-  d_statResultSource("smt::resultSource", "unknown") {
+  d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0) {
 
   NodeManagerScope nms(d_nodeManager);
 
@@ -282,7 +281,6 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   StatisticsRegistry::registerStat(&d_cnfConversionTime);
   StatisticsRegistry::registerStat(&d_numAssertionsPre);
   StatisticsRegistry::registerStat(&d_numAssertionsPost);
-  StatisticsRegistry::registerStat(&d_statResultSource);
 
   // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
@@ -402,7 +400,6 @@ SmtEngine::~SmtEngine() throw() {
     StatisticsRegistry::unregisterStat(&d_cnfConversionTime);
     StatisticsRegistry::unregisterStat(&d_numAssertionsPre);
     StatisticsRegistry::unregisterStat(&d_numAssertionsPost);
-    StatisticsRegistry::unregisterStat(&d_statResultSource);
 
     delete d_private;
     delete d_userContext;
@@ -1257,7 +1254,6 @@ Result SmtEngine::check() {
 
   Trace("smt") << "SmtEngine::check(): running check" << endl;
   Result result = d_propEngine->checkSat(millis, resource);
-  d_statResultSource.setData("satSolver");
 
   // PropEngine::checkSat() returns the actual amount used in these
   // variables.
@@ -1267,14 +1263,6 @@ Result SmtEngine::check() {
   Trace("limit") << "SmtEngine::check(): cumulative millis " << d_cumulativeTimeUsed
                  << ", conflicts " << d_cumulativeResourceUsed << endl;
 
-  if(result.isUnknown() and d_decisionEngine != NULL) {
-    Result deResult = d_decisionEngine->getResult();
-    if(not deResult.isUnknown()) {
-      d_statResultSource.setData("decisionEngine");
-      result = deResult;
-    }
-  }
-
   return result;
 }
 

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index e0f544f9e02d394adb3fe4342645817a4761cefb..0873aea96a213cd41ccb8850a039beaaeb3d60f2 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -258,9 +258,6 @@ class CVC4_PUBLIC SmtEngine {
   /** Num of assertions after ite removal */
   IntStat d_numAssertionsPost;
 
-  /** how the SMT engine got the answer -- SAT solver or DE */
-  BackedStat<std::string> d_statResultSource;
-
 public:
 
   /**