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/bvminisat | |
parent | 3df7ea65b701a9ab054179af7efb4be120d280f2 (diff) |
added options for controlling resource step-count for various solving stages
Diffstat (limited to 'src/prop/bvminisat')
-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 |
3 files changed, 13 insertions, 12 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) && |