added options for controlling resource step-count for various solving stages

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) &&