diff options
author | Liana Hadarean <lianah@cs.nyu.edu> | 2014-11-17 15:26:42 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-11-17 15:26:42 -0500 |
commit | 3ba7ed6b1b09739385ae2ffb77a5c7ccd18b40a5 (patch) | |
tree | 845ae47600ffff9c68fa654c0f78d3474e406beb /src/prop | |
parent | d8da3b13bc9df7750723cf3da38edc8cb6f67d3d (diff) |
Resource-limiting work.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bvminisat/bvminisat.cpp | 4 | ||||
-rw-r--r-- | src/prop/bvminisat/bvminisat.h | 7 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.h | 7 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 7 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 6 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 14 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 6 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 4 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 1 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 34 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 108 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 7 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 6 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 2 |
14 files changed, 62 insertions, 151 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index 71b8eb69d..aceb0f2e9 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -97,10 +97,6 @@ void BVMinisatSatSolver::markUnremovable(SatLiteral lit){ d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true); } -bool BVMinisatSatSolver::spendResource(){ - // Do nothing for the BV solver. - return false; -} void BVMinisatSatSolver::interrupt(){ d_minisat->interrupt(); diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index fea437565..e163ddcfd 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -46,8 +46,11 @@ private: d_notify->notify(satClause); } + void spendResource() { + d_notify->spendResource(); + } void safePoint() { - d_notify->safePoint(); + d_notify->safePoint(); } }; @@ -86,8 +89,6 @@ public: void markUnremovable(SatLiteral lit); - bool spendResource(); - void interrupt(); SatValue solve(); diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index 882f23ef7..a7a55208d 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -52,6 +52,7 @@ public: */ virtual void notify(vec<Lit>& learnt) = 0; + virtual void spendResource() = 0; virtual void safePoint() = 0; }; @@ -412,8 +413,10 @@ 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(); + Assert (notify); + notify->spendResource(); + 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/cnf_stream.cpp b/src/prop/cnf_stream.cpp index ad187aa46..8d7b014cc 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -30,6 +30,7 @@ #include "proof/proof_manager.h" #include "proof/sat_proof.h" #include "prop/minisat/minisat.h" +#include "smt/smt_engine_scope.h" #include <queue> using namespace std; @@ -665,6 +666,12 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl; + if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) { + NodeManager::currentResourceManager()->spendResource(); + d_convertAndAssertCounter = 0; + } + ++d_convertAndAssertCounter; + switch(node.getKind()) { case AND: convertAndAssertAnd(node, negated); diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index b76051279..b22290ae4 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -74,6 +74,12 @@ protected: */ const bool d_fullLitToNodeMap; + /** + * Counter for resource limiting that is used to spend a resource + * every ResourceManager::resourceCounter calls to convertAndAssert. + */ + unsigned long d_convertAndAssertCounter; + /** The "registrar" for pre-registration of terms */ Registrar* d_registrar; diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index e5e28bb0b..ea370ac08 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -1593,7 +1593,7 @@ CRef Solver::updateLemmas() { Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl; // Avoid adding lemmas indefinitely without resource-out - spendResource(); + proxy->spendResource(); CRef conflict = CRef_Undef; @@ -1710,3 +1710,15 @@ CRef Solver::updateLemmas() { return conflict; } + +inline bool Solver::withinBudget() const { + Assert (proxy); + // spendResource sets async_interrupt or throws UnsafeInterruptException + // depending on whether hard-limit is enabled + proxy->spendResource(); + + bool within_budget = !asynch_interrupt && + (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) && + (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); + return within_budget; +} diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 6d9fd538f..3ec19b026 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -219,7 +219,6 @@ public: void budgetOff(); void interrupt(); // Trigger a (potentially asynchronous) interruption of the solver. void clearInterrupt(); // Clear interrupt indicator flag. - void spendResource(); // Memory managment: // @@ -535,11 +534,6 @@ inline void Solver::setPropBudget(int64_t x){ propagation_budget = propagati 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 { - return !asynch_interrupt && - (conflict_budget < 0 || conflicts + resources_consumed < (uint64_t)conflict_budget) && - (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); } -inline void Solver::spendResource() { ++resources_consumed; } // FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a // pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 99341455c..b9fa37230 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -182,10 +182,6 @@ SatValue MinisatSatSolver::solve() { return toSatLiteralValue(d_minisat->solve()); } -bool MinisatSatSolver::spendResource() { - d_minisat->spendResource(); - return !d_minisat->withinBudget(); -} void MinisatSatSolver::interrupt() { d_minisat->interrupt(); diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 96893fe41..7c6e10170 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -61,7 +61,6 @@ public: SatValue solve(); SatValue solve(long unsigned int&); - bool spendResource(); void interrupt(); SatValue value(SatLiteral l); diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index a998d4240..c7dae533e 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -32,6 +32,7 @@ #include "main/options.h" #include "util/output.h" #include "util/result.h" +#include "util/resource_manager.h" #include "expr/expr.h" #include "expr/command.h" @@ -74,8 +75,8 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext d_satSolver(NULL), d_registrar(NULL), d_cnfStream(NULL), - d_satTimer(*this), - d_interrupted(false) { + d_interrupted(false), + d_resourceManager(NodeManager::currentResourceManager()) { Debug("prop") << "Constructing the PropEngine" << endl; @@ -159,7 +160,7 @@ void PropEngine::printSatisfyingAssignment(){ } } -Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) { +Result PropEngine::checkSat() { Assert(!d_inCheckSat, "Sat solver in solve()!"); Debug("prop") << "PropEngine::checkSat()" << endl; @@ -171,25 +172,23 @@ Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) { d_theoryEngine->presolve(); if(options::preprocessOnly()) { - millis = resource = 0; return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK); } - // Set the timer - d_satTimer.set(millis); - // Reset the interrupted flag d_interrupted = false; // Check the problem - SatValue result = d_satSolver->solve(resource); - - millis = d_satTimer.elapsed(); + SatValue result = d_satSolver->solve(); if( result == SAT_VALUE_UNKNOWN ) { - Result::UnknownExplanation why = - d_satTimer.expired() ? Result::TIMEOUT : - (d_interrupted ? Result::INTERRUPTED : Result::RESOURCEOUT); + + Result::UnknownExplanation why = Result::INTERRUPTED; + if (d_resourceManager->outOfTime()) + why = Result::TIMEOUT; + if (d_resourceManager->outOfResources()) + why = Result::RESOURCEOUT; + return Result(Result::SAT_UNKNOWN, why); } @@ -279,16 +278,11 @@ void PropEngine::interrupt() throw(ModalException) { d_interrupted = true; d_satSolver->interrupt(); - d_theoryEngine->interrupt(); Debug("prop") << "interrupt()" << endl; } -void PropEngine::spendResource() throw() { - if(d_satSolver->spendResource()) { - d_satSolver->interrupt(); - d_theoryEngine->interrupt(); - } - checkTime(); +void PropEngine::spendResource() throw (UnsafeInterruptException) { + d_resourceManager->spendResource(); } bool PropEngine::properExplanation(TNode node, TNode expl) const { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index ed022a64f..2750319e6 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -24,12 +24,14 @@ #include "expr/node.h" #include "options/options.h" #include "util/result.h" +#include "util/unsafe_interrupt_exception.h" #include "smt/modal_exception.h" #include "proof/proof_manager.h" #include <sys/time.h> namespace CVC4 { +class ResourceManager; class DecisionEngine; class TheoryEngine; @@ -45,78 +47,6 @@ class DPLLSatSolverInterface; class PropEngine; /** - * A helper class to keep track of a time budget and signal - * the PropEngine when the budget expires. - */ -class SatTimer { - - PropEngine& d_propEngine; - unsigned long d_ms; - timeval d_limit; - -public: - - /** Construct a SatTimer attached to the given PropEngine. */ - SatTimer(PropEngine& propEngine) : - d_propEngine(propEngine), - d_ms(0) { - } - - /** Is the timer currently active? */ - bool on() const { - return d_ms != 0; - } - - /** Set a millisecond timer (0==off). */ - void set(unsigned long millis) { - d_ms = millis; - // keep track of when it was set, even if it's disabled (i.e. == 0) - Trace("limit") << "SatTimer::set(" << d_ms << ")" << std::endl; - gettimeofday(&d_limit, NULL); - Trace("limit") << "SatTimer::set(): it's " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl; - d_limit.tv_sec += millis / 1000; - d_limit.tv_usec += (millis % 1000) * 1000; - if(d_limit.tv_usec > 1000000) { - ++d_limit.tv_sec; - d_limit.tv_usec -= 1000000; - } - Trace("limit") << "SatTimer::set(): limit is at " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl; - } - - /** Return the milliseconds elapsed since last set(). */ - unsigned long elapsed() { - timeval tv; - gettimeofday(&tv, NULL); - Trace("limit") << "SatTimer::elapsed(): it's now " << tv.tv_sec << "," << tv.tv_usec << std::endl; - tv.tv_sec -= d_limit.tv_sec - d_ms / 1000; - tv.tv_usec -= d_limit.tv_usec - (d_ms % 1000) * 1000; - Trace("limit") << "SatTimer::elapsed(): elapsed time is " << tv.tv_sec << "," << tv.tv_usec << std::endl; - return tv.tv_sec * 1000 + tv.tv_usec / 1000; - } - - bool expired() { - if(on()) { - timeval tv; - gettimeofday(&tv, NULL); - Trace("limit") << "SatTimer::expired(): current time is " << tv.tv_sec << "," << tv.tv_usec << std::endl; - Trace("limit") << "SatTimer::expired(): limit time is " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl; - if(d_limit.tv_sec < tv.tv_sec || - (d_limit.tv_sec == tv.tv_sec && d_limit.tv_usec <= tv.tv_usec)) { - Trace("limit") << "SatTimer::expired(): OVER LIMIT!" << std::endl; - return true; - } else { - Trace("limit") << "SatTimer::expired(): within limit" << std::endl; - } - } - return false; - } - - /** Check the current time and signal the PropEngine if over-time. */ - void check(); - -};/* class SatTimer */ - -/** * PropEngine is the abstraction of a Sat Solver, providing methods for * solving the SAT problem and conversion to CNF (via the CnfStream). */ @@ -152,11 +82,10 @@ class PropEngine { /** The CNF converter in use */ CnfStream* d_cnfStream; - /** A timer for SAT calls */ - SatTimer d_satTimer; - /** Whether we were just interrupted (or not) */ bool d_interrupted; + /** Pointer to resource manager for associated SmtEngine */ + ResourceManager* d_resourceManager; /** Dump out the satisfying assignment (after SAT result) */ void printSatisfyingAssignment(); @@ -236,12 +165,8 @@ public: /** * Checks the current context for satisfiability. * - * @param millis the time limit for this call in milliseconds - * (0==off); on output, it is set to the milliseconds used - * @param on input, resource the number of resource units permitted - * for this call (0==off); on output, it is set to the resource used */ - Result checkSat(unsigned long& millis, unsigned long& resource); + Result checkSat(); /** * Get the value of a boolean variable. @@ -295,21 +220,15 @@ public: bool isRunning() const; /** - * Check the current time budget. - */ - void checkTime(); - - /** * Interrupt a running solver (cause a timeout). */ void interrupt() throw(ModalException); /** - * "Spend" a "resource." If the sum of these externally-counted - * resources and SAT-internal resources exceed the current limit, - * SAT should terminate. + * Informs the ResourceManager that a resource has been spent. If out of + * resources, can throw an UnsafeInterruptException exception. */ - void spendResource() throw(); + void spendResource() throw (UnsafeInterruptException); /** * For debugging. Return true if "expl" is a well-formed @@ -326,17 +245,6 @@ public: };/* class PropEngine */ -inline void SatTimer::check() { - if(d_propEngine.isRunning() && expired()) { - Trace("limit") << "SatTimer::check(): interrupt!" << std::endl; - d_propEngine.interrupt(); - } -} - -inline void PropEngine::checkTime() { - d_satTimer.check(); -} - }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index adf6dfd07..b71844590 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -62,12 +62,6 @@ 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. - * Returns true if resources are exhausted. - */ - virtual bool spendResource() = 0; - /** Interrupt the solver */ virtual void interrupt() = 0; @@ -102,6 +96,7 @@ public: * Notify about a learnt clause. */ virtual void notify(SatClause& clause) = 0; + virtual void spendResource() = 0; virtual void safePoint() = 0; };/* class BVSatSolverInterface::Notify */ diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 2bcd48099..59e87dd33 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -103,7 +103,7 @@ TNode TheoryProxy::getNode(SatLiteral lit) { } void TheoryProxy::notifyRestart() { - d_propEngine->checkTime(); + d_propEngine->spendResource(); d_theoryEngine->notifyRestart(); static uint32_t lemmaCount = 0; @@ -179,8 +179,8 @@ void TheoryProxy::logDecision(SatLiteral lit) { #endif /* CVC4_REPLAY */ } -void TheoryProxy::checkTime() { - d_propEngine->checkTime(); +void TheoryProxy::spendResource() { + d_theoryEngine->spendResource(); } bool TheoryProxy::isDecisionRelevant(SatVariable var) { diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index a962f653a..3565aa501 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -111,7 +111,7 @@ public: void logDecision(SatLiteral lit); - void checkTime(); + void spendResource(); bool isDecisionEngineDone(); |