diff options
author | Liana Hadarean <lianahady@gmail.com> | 2015-05-28 15:03:10 +0100 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2015-05-28 15:03:10 +0100 |
commit | b4aaa40ca834958130a8ee5a922ac45c6de84ce1 (patch) | |
tree | d0ce340446271c56909bcac8b1697ca18b7d5773 /src/prop | |
parent | 3df7ea65b701a9ab054179af7efb4be120d280f2 (diff) |
added options for controlling resource step-count for various solving stages
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bvminisat/bvminisat.h | 8 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 5 | ||||
-rw-r--r-- | src/prop/bvminisat/core/Solver.h | 12 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 2 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 13 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 2 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 4 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 2 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 4 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 6 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 2 |
11 files changed, 31 insertions, 29 deletions
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 6246e6885..2c9662655 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -46,11 +46,11 @@ private: d_notify->notify(satClause); } - void spendResource() { - d_notify->spendResource(); + void spendResource(uint64_t ammount) { + d_notify->spendResource(ammount); } - void safePoint() { - d_notify->safePoint(); + void safePoint(uint64_t ammount) { + d_notify->safePoint(ammount); } }; diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index b6238460b..1267561fb 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -29,6 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "util/utility.h" #include "util/exception.h" #include "theory/bv/options.h" +#include "smt/options.h" #include "theory/interrupted.h" using namespace BVMinisat; @@ -871,7 +872,7 @@ lbool Solver::search(int nof_conflicts, UIP uip) // NO CONFLICT bool isWithinBudget; try { - isWithinBudget = withinBudget(); + isWithinBudget = withinBudget(CVC4::options::bvSatConflictStep()); } catch (const CVC4::theory::Interrupted& e) { // do some clean-up and rethrow @@ -1021,7 +1022,7 @@ lbool Solver::solve_() while (status == l_Undef){ double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts); status = search(rest_base * restart_first); - if (!withinBudget()) break; + if (!withinBudget(CVC4::options::bvSatConflictStep())) break; curr_restarts++; } diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index 3fcf34185..7d2a978b9 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -52,8 +52,8 @@ public: */ virtual void notify(vec<Lit>& learnt) = 0; - virtual void spendResource() = 0; - virtual void safePoint() = 0; + virtual void spendResource(uint64_t ammount) = 0; + virtual void safePoint(uint64_t ammount) = 0; }; //================================================================================================= @@ -324,7 +324,7 @@ protected: CRef reason (Var x) const; int level (Var x) const; double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... - bool withinBudget () const; + bool withinBudget (uint64_t ammount) const; // Static helpers: // @@ -412,10 +412,10 @@ 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 { +inline bool Solver::withinBudget(uint64_t ammount) const { Assert (notify); - notify->spendResource(); - notify->safePoint(); + notify->spendResource(ammount); + notify->safePoint(0); return !asynch_interrupt && (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) && diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index c8d86c73d..f03cc9944 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -679,7 +679,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated, ProofRule proo Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl; if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) { - NodeManager::currentResourceManager()->spendResource(); + NodeManager::currentResourceManager()->spendResource(options::cnfStep()); d_convertAndAssertCounter = 0; } ++d_convertAndAssertCounter; diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 56316ca0b..2c94401fb 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -1205,7 +1205,8 @@ lbool Solver::search(int nof_conflicts) check_type = CHECK_WITH_THEORY; } - if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()) { + if (nof_conflicts >= 0 && conflictC >= nof_conflicts || + !withinBudget(options::satConflictStep())) { // Reached bound on number of conflicts: progress_estimate = progressEstimate(); cancelUntil(0); @@ -1343,11 +1344,11 @@ lbool Solver::solve_() while (status == l_Undef){ double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts); status = search(rest_base * restart_first); - if (!withinBudget()) break; + if (!withinBudget(options::satConflictStep())) break; // FIXME add restart option? curr_restarts++; } - if(!withinBudget()) + if(!withinBudget(options::satConflictStep())) status = l_Undef; if (verbosity >= 1) @@ -1599,7 +1600,7 @@ CRef Solver::updateLemmas() { Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl; // Avoid adding lemmas indefinitely without resource-out - proxy->spendResource(); + proxy->spendResource(options::lemmaStep()); CRef conflict = CRef_Undef; @@ -1717,11 +1718,11 @@ CRef Solver::updateLemmas() { return conflict; } -inline bool Solver::withinBudget() const { +inline bool Solver::withinBudget(uint64_t ammount) const { Assert (proxy); // spendResource sets async_interrupt or throws UnsafeInterruptException // depending on whether hard-limit is enabled - proxy->spendResource(); + proxy->spendResource(ammount); bool within_budget = !asynch_interrupt && (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) && diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 9243a2b35..1508e3e35 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -424,7 +424,7 @@ protected: int trail_index (Var x) const; // Index in the trail double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... public: - bool withinBudget () const; + bool withinBudget (uint64_t amount) const; protected: // Static helpers: diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index c7dae533e..e6d965f8f 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -281,8 +281,8 @@ void PropEngine::interrupt() throw(ModalException) { Debug("prop") << "interrupt()" << endl; } -void PropEngine::spendResource() throw (UnsafeInterruptException) { - d_resourceManager->spendResource(); +void PropEngine::spendResource(uint64_t ammount) throw (UnsafeInterruptException) { + d_resourceManager->spendResource(ammount); } bool PropEngine::properExplanation(TNode node, TNode expl) const { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 2750319e6..17ac394c3 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -228,7 +228,7 @@ public: * Informs the ResourceManager that a resource has been spent. If out of * resources, can throw an UnsafeInterruptException exception. */ - void spendResource() throw (UnsafeInterruptException); + void spendResource(uint64_t ammount) throw (UnsafeInterruptException); /** * For debugging. Return true if "expl" is a well-formed diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 8effa8189..79758a425 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -97,8 +97,8 @@ public: * Notify about a learnt clause. */ virtual void notify(SatClause& clause) = 0; - virtual void spendResource() = 0; - virtual void safePoint() = 0; + virtual void spendResource(uint64_t ammount) = 0; + virtual void safePoint(uint64_t ammount) = 0; };/* class BVSatSolverInterface::Notify */ diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 59e87dd33..5b80b7596 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->spendResource(); + d_propEngine->spendResource(options::restartStep()); d_theoryEngine->notifyRestart(); static uint32_t lemmaCount = 0; @@ -179,8 +179,8 @@ void TheoryProxy::logDecision(SatLiteral lit) { #endif /* CVC4_REPLAY */ } -void TheoryProxy::spendResource() { - d_theoryEngine->spendResource(); +void TheoryProxy::spendResource(uint64_t ammount) { + d_theoryEngine->spendResource(ammount); } bool TheoryProxy::isDecisionRelevant(SatVariable var) { diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 3565aa501..d978edefd 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -111,7 +111,7 @@ public: void logDecision(SatLiteral lit); - void spendResource(); + void spendResource(uint64_t ammount); bool isDecisionEngineDone(); |