From 83722fdc9072c8bee19c2123176d77bef50bbe0d Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Wed, 3 Oct 2012 19:41:45 +0000 Subject: [PATCH] added support for interrupting TheoryBV --- src/prop/bvminisat/bvminisat.h | 4 ++++ src/prop/bvminisat/core/Solver.cc | 22 +++++++++++++++++----- src/prop/bvminisat/core/Solver.h | 3 +++ src/prop/prop_engine.cpp | 1 + src/prop/sat_solver.h | 2 ++ src/smt/smt_engine.cpp | 1 + src/theory/bv/bitblaster.cpp | 4 ++++ src/theory/bv/bitblaster.h | 1 + src/theory/theory_engine.cpp | 29 +++++++++++++++++++++++++++-- src/theory/theory_engine.h | 12 ++++++++++++ 10 files changed, 72 insertions(+), 7 deletions(-) diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index e13775ab2..0dd208088 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -46,6 +46,10 @@ private: toSatClause(clause, satClause); d_notify->notify(satClause); } + + void safePoint() { + d_notify->safePoint(); + } }; BVMinisat::SimpSolver* d_minisat; diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 293ddd657..978ac8d7b 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -27,9 +27,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "util/output.h" #include "util/utility.h" - +#include "util/exception.h" #include "theory/bv/options.h" - +#include "theory/interrupted.h" using namespace BVMinisat; namespace CVC4 { @@ -794,13 +794,25 @@ lbool Solver::search(int nof_conflicts, UIP uip) }else{ // NO CONFLICT - if (decisionLevel() > assumptions.size() && nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){ + bool isWithinBudget; + try { + isWithinBudget = withinBudget(); + } + catch (const CVC4::theory::Interrupted& e) { + // do some clean-up and rethrow + cancelUntil(assumptions.size()); + throw e; + } + + if (decisionLevel() > assumptions.size() && nof_conflicts >= 0 && conflictC >= nof_conflicts || + !isWithinBudget) { // Reached bound on number of conflicts: Debug("bvminisat::search") << OUTPUT_TAG << " restarting " << std::endl; progress_estimate = progressEstimate(); cancelUntil(assumptions.size()); - return l_Undef; } - + return l_Undef; + } + // Simplify the set of problem clauses: if (decisionLevel() == 0 && !simplify()) { Debug("bvminisat::search") << OUTPUT_TAG << " base level conflict, we're unsat" << std::endl; diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index b50ab632e..53d92ac39 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -52,6 +52,7 @@ public: */ virtual void notify(vec& learnt) = 0; + virtual void safePoint() = 0; }; //================================================================================================= @@ -410,6 +411,8 @@ inline void Solver::interrupt(){ asynch_interrupt = true; } inline void Solver::clearInterrupt(){ asynch_interrupt = false; } inline void Solver::budgetOff(){ conflict_budget = propagation_budget = -1; } inline bool Solver::withinBudget() const { + Assert (notify); + notify->safePoint(); return !asynch_interrupt && (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) && (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index fe25caf29..973adc67f 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -282,6 +282,7 @@ void PropEngine::interrupt() throw(ModalException) { d_interrupted = true; d_satSolver->interrupt(); + d_theoryEngine->interrupt(); Debug("prop") << "interrupt()" << endl; } diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index a4fdd5b3a..7e3af69cf 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -94,6 +94,8 @@ public: * Notify about a learnt clause. */ virtual void notify(SatClause& clause) = 0; + virtual void safePoint() = 0; + };/* class BVSatSolverInterface::Notify */ virtual void setNotify(Notify* notify) = 0; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d3806199b..878588d15 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2446,6 +2446,7 @@ void SmtEngine::interrupt() throw(ModalException) { return; } d_propEngine->interrupt(); + d_theoryEngine->interrupt(); } void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) { diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index 2c45fb603..3beb7c229 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -356,6 +356,10 @@ void Bitblaster::MinisatNotify::notify(prop::SatClause& clause) { } }; +void Bitblaster::MinisatNotify::safePoint() { + d_bv->d_out->safePoint(); +} + EqualityStatus Bitblaster::getEqualityStatus(TNode a, TNode b) { // We don't want to bit-blast every possibly expensive term for the sake of equality checking diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h index 2ff12bbdf..ada9802bd 100644 --- a/src/theory/bv/bitblaster.h +++ b/src/theory/bv/bitblaster.h @@ -78,6 +78,7 @@ class Bitblaster { {} bool notify(prop::SatLiteral lit); void notify(prop::SatClause& clause); + void safePoint(); }; typedef __gnu_cxx::hash_map TermDefMap; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 932f11f74..0db71aba4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -71,6 +71,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_propagatedLiterals(context), d_propagatedLiteralsIndex(context, 0), d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"), + d_interrupted(false), d_inPreregister(false), d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), @@ -113,6 +114,10 @@ TheoryEngine::~TheoryEngine() { StatisticsRegistry::unregisterStat(&d_combineTheoriesTime); } +void TheoryEngine::interrupt() throw(ModalException) { + d_interrupted = true; +} + void TheoryEngine::preRegister(TNode preprocessed) { if(Dump.isOn("missed-t-propagations")) { @@ -282,6 +287,9 @@ void TheoryEngine::check(Theory::Effort effort) { d_propEngine->checkTime(); + // Reset the interrupt flag + d_interrupted = false; + #ifdef CVC4_FOR_EACH_THEORY_STATEMENT #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif @@ -293,7 +301,6 @@ void TheoryEngine::check(Theory::Effort effort) { } \ } - // Do the checking try { @@ -455,6 +462,9 @@ void TheoryEngine::combineTheories() { } void TheoryEngine::propagate(Theory::Effort effort) { + // Reset the interrupt flag + d_interrupted = false; + // Definition of the statement that is to be run by every theory #ifdef CVC4_FOR_EACH_THEORY_STATEMENT #undef CVC4_FOR_EACH_THEORY_STATEMENT @@ -464,6 +474,9 @@ void TheoryEngine::propagate(Theory::Effort effort) { theoryOf(THEORY)->propagate(effort); \ } + // Reset the interrupt flag + d_interrupted = false; + // Propagate for each theory using the statement above CVC4_FOR_EACH_THEORY; @@ -592,6 +605,8 @@ TheoryModel* TheoryEngine::getModel() { } bool TheoryEngine::presolve() { + // Reset the interrupt flag + d_interrupted = false; try { // Definition of the statement that is to be run by every theory @@ -599,7 +614,7 @@ bool TheoryEngine::presolve() { #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits::hasPresolve) { \ + if (theory::TheoryTraits::hasPresolve) { \ theoryOf(THEORY)->presolve(); \ if(d_inConflict) { \ return true; \ @@ -616,6 +631,8 @@ bool TheoryEngine::presolve() { }/* TheoryEngine::presolve() */ void TheoryEngine::postsolve() { + // Reset the interrupt flag + d_interrupted = false; try { // Definition of the statement that is to be run by every theory @@ -637,6 +654,9 @@ void TheoryEngine::postsolve() { void TheoryEngine::notifyRestart() { + // Reset the interrupt flag + d_interrupted = false; + // Definition of the statement that is to be run by every theory #ifdef CVC4_FOR_EACH_THEORY_STATEMENT #undef CVC4_FOR_EACH_THEORY_STATEMENT @@ -651,6 +671,8 @@ void TheoryEngine::notifyRestart() { } void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder<>& learned) { + // Reset the interrupt flag + d_interrupted = false; // Definition of the statement that is to be run by every theory #ifdef CVC4_FOR_EACH_THEORY_STATEMENT @@ -683,6 +705,9 @@ void TheoryEngine::shutdown() { } theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) { + // Reset the interrupt flag + d_interrupted = false; + TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 5ec0d9776..8f534a62c 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -36,11 +36,13 @@ #include "theory/shared_terms_database.h" #include "theory/term_registration_visitor.h" #include "theory/valuation.h" +#include "theory/interrupted.h" #include "options/options.h" #include "smt/options.h" #include "util/statistics_registry.h" #include "util/hash.h" #include "util/cache.h" +#include "util/cvc4_assert.h" #include "theory/ite_simplifier.h" #include "theory/unconstrained_simplifier.h" #include "theory/model.h" @@ -230,6 +232,11 @@ class TheoryEngine { { } + void safePoint() throw(theory::Interrupted, AssertionException) { + if (d_engine->d_interrupted) + throw theory::Interrupted(); + } + void conflict(TNode conflictNode) throw(AssertionException) { Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; ++ d_statistics.conflicts; @@ -386,6 +393,9 @@ class TheoryEngine { Node d_true; Node d_false; + /** Whether we were just interrupted (or not) */ + bool d_interrupted; + public: /** Constructs a theory engine */ @@ -394,6 +404,8 @@ public: /** Destroys a theory engine */ ~TheoryEngine(); + void interrupt() throw(ModalException); + /** * Adds a theory. Only one theory per TheoryId can be present, so if * there is another theory it will be deleted. -- 2.30.2