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

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();