From 744792614fdd8da94eecd5b0cad7c3cb19b3d91c Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 6 Oct 2014 22:57:57 -0400 Subject: [PATCH] Fix a resource limiting issue where interruption didn't occur promptly. Thanks Johannes Kanig for the report. --- src/prop/bvminisat/bvminisat.cpp | 5 +++-- src/prop/bvminisat/bvminisat.h | 2 +- src/prop/minisat/core/Solver.cc | 3 ++- src/prop/minisat/core/Solver.h | 2 ++ src/prop/minisat/minisat.cpp | 3 ++- src/prop/minisat/minisat.h | 2 +- src/prop/prop_engine.cpp | 15 +++++++++------ src/prop/sat_solver.h | 7 +++++-- src/theory/quantifiers_engine.cpp | 2 +- 9 files changed, 26 insertions(+), 15 deletions(-) diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index 498b31ce5..71b8eb69d 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -97,8 +97,9 @@ void BVMinisatSatSolver::markUnremovable(SatLiteral lit){ d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true); } -void BVMinisatSatSolver::spendResource(){ - // do nothing for the BV solver +bool BVMinisatSatSolver::spendResource(){ + // Do nothing for the BV solver. + return false; } void BVMinisatSatSolver::interrupt(){ diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 04f21e761..c7ee2e0b7 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -87,7 +87,7 @@ public: void markUnremovable(SatLiteral lit); - void spendResource(); + bool spendResource(); void interrupt(); diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 5403b992e..e5e28bb0b 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -815,7 +815,8 @@ CRef Solver::propagate(TheoryCheckType type) if (type == CHECK_FINAL) { // Do the theory check theoryCheck(CVC4::theory::Theory::EFFORT_FULL); - // Pick up the theory propagated literals (there could be some, if new lemmas are added) + // Pick up the theory propagated literals (there could be some, + // if new lemmas are added) propagateTheory(); // If there are lemmas (or conflicts) update them if (lemmas.size() > 0) { diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 2d70cfeef..6d9fd538f 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -423,7 +423,9 @@ protected: int intro_level (Var x) const; // User level at which this variable was created int trail_index (Var x) const; // Index in the trail double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... +public: bool withinBudget () const; +protected: // Static helpers: // diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index b50c1c09f..99341455c 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -182,8 +182,9 @@ SatValue MinisatSatSolver::solve() { return toSatLiteralValue(d_minisat->solve()); } -void MinisatSatSolver::spendResource() { +bool MinisatSatSolver::spendResource() { d_minisat->spendResource(); + return !d_minisat->withinBudget(); } void MinisatSatSolver::interrupt() { diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 3992f1adb..3d3cea356 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -62,7 +62,7 @@ public: SatValue solve(); SatValue solve(long unsigned int&); - void spendResource(); + bool spendResource(); void interrupt(); SatValue value(SatLiteral l); diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 1572dfa88..a998d4240 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -79,14 +79,14 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext Debug("prop") << "Constructing the PropEngine" << endl; - d_satSolver = SatSolverFactory::createDPLLMinisat(); + d_satSolver = SatSolverFactory::createDPLLMinisat(); d_registrar = new theory::TheoryRegistrar(d_theoryEngine); d_cnfStream = new CVC4::prop::TseitinCnfStream (d_satSolver, d_registrar, userContext, - // fullLitToNode Map = - options::threads() > 1 || + // fullLitToNode Map = + options::threads() > 1 || options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY ); @@ -95,7 +95,7 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext d_decisionEngine->setSatSolver(d_satSolver); d_decisionEngine->setCnfStream(d_cnfStream); - PROOF (ProofManager::currentPM()->initCnfProof(d_cnfStream); ); + PROOF (ProofManager::currentPM()->initCnfProof(d_cnfStream); ); } PropEngine::~PropEngine() { @@ -279,12 +279,15 @@ void PropEngine::interrupt() throw(ModalException) { d_interrupted = true; d_satSolver->interrupt(); - d_theoryEngine->interrupt(); + d_theoryEngine->interrupt(); Debug("prop") << "interrupt()" << endl; } void PropEngine::spendResource() throw() { - d_satSolver->spendResource(); + if(d_satSolver->spendResource()) { + d_satSolver->interrupt(); + d_theoryEngine->interrupt(); + } checkTime(); } diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index e3b0f3449..adf6dfd07 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -62,8 +62,11 @@ public: /** Check the satisfiability of the added clauses */ virtual SatValue solve(long unsigned int&) = 0; - /** Instruct the solver that it should bump its consumed resource count. */ - virtual void spendResource() = 0; + /** + * Instruct the solver that it should bump its consumed resource count. + * Returns true if resources are exhausted. + */ + virtual bool spendResource() = 0; /** Interrupt the solver */ virtual void interrupt() = 0; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a4d7aaec1..5bf285ae2 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -601,7 +601,7 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst ){ // For resource-limiting (also does a time check). - getOutputChannel().spendResource(); + getOutputChannel().safePoint(); std::vector< Node > terms; //make sure there are values for each variable we are instantiating -- 2.30.2