diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-12 17:33:29 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-12 17:33:29 +0000 |
commit | 0659b7c7b50e49cbea1728f90f7ff04598f01eac (patch) | |
tree | c0f2ab0f6734fa6c78c68857c1a2c2d551f7a644 | |
parent | 43dd3569232fd72d7791db7dd113bdff0bdf916d (diff) |
cleanup of exit mechanism when decisionEngine is on\n\n fixes some bugs we were seeing in quantifiers+decision stuff
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 6 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 14 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 3 |
3 files changed, 1 insertions, 22 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 697ab4853..9aefda75a 100644 --- 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 652749557..7cac970f8 100644 --- 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 e0f544f9e..0873aea96 100644 --- 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: /** |