From: Morgan Deters Date: Tue, 7 Oct 2014 02:57:57 +0000 (-0400) Subject: Fix a resource limiting issue where interruption didn't occur promptly. Thanks Johan... X-Git-Tag: cvc5-1.0.0~6586 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=744792614fdd8da94eecd5b0cad7c3cb19b3d91c;p=cvc5.git Fix a resource limiting issue where interruption didn't occur promptly. Thanks Johannes Kanig for the report. --- 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