resource manager: Add statistic for every resource. (#3772)

This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`).

Fixes #3751.

3 files changed, 17 insertions, 13 deletions

diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 70e0b9157..f71dac3e5 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -23,9 +23,10 @@
 #include "context/cdo.h"
 #include "proof/clause_id.h"
 #include "proof/resolution_bitvector_proof.h"
+#include "prop/bv_sat_solver_notify.h"
 #include "prop/bvminisat/simp/SimpSolver.h"
 #include "prop/sat_solver.h"
-#include "prop/bv_sat_solver_notify.h"
+#include "util/resource_manager.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -46,11 +47,14 @@ class BVMinisatSatSolver : public BVSatSolverInterface,
       return d_notify->notify(toSatLiteral(lit));
     }
     void notify(BVMinisat::vec<BVMinisat::Lit>& clause) override;
-    void spendResource(unsigned amount) override
+    void spendResource(ResourceManager::Resource r) override
+    {
+      d_notify->spendResource(r);
+    }
+    void safePoint(ResourceManager::Resource r) override
     {
-      d_notify->spendResource(amount);
+      d_notify->safePoint(r);
     }
-    void safePoint(unsigned amount) override { d_notify->safePoint(amount); }
   };
 
 	std::unique_ptr<BVMinisat::SimpSolver> d_minisat;
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 04658fc38..25b6a3da2 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -1076,7 +1076,8 @@ lbool Solver::search(int nof_conflicts, UIP uip)
             // NO CONFLICT
             bool isWithinBudget;
             try {
-              isWithinBudget = withinBudget(CVC4::options::bvSatConflictStep()); 
+              isWithinBudget =
+                  withinBudget(ResourceManager::Resource::BvSatConflictsStep);
             }
             catch (const CVC4::theory::Interrupted& e) {
               // do some clean-up and rethrow 
@@ -1232,7 +1233,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(CVC4::options::bvSatConflictStep())) break;
+        if (!withinBudget(ResourceManager::Resource::BvSatConflictsStep)) break;
         curr_restarts++;
     }
 
@@ -1482,11 +1483,10 @@ void ClauseAllocator::reloc(CRef& cr,
 }
 
 void Solver::setNotify(Notify* toNotify) { d_notify = toNotify; }
-bool Solver::withinBudget(uint64_t amount) const
+bool Solver::withinBudget(ResourceManager::Resource r) const
 {
   AlwaysAssert(d_notify);
-  d_notify->spendResource(amount);
-  d_notify->safePoint(0);
+  d_notify->safePoint(r);
 
   return !asynch_interrupt &&
          (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) &&
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index eef1c4e4c..2197d030f 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -31,7 +31,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/bvminisat/mtl/Heap.h"
 #include "prop/bvminisat/mtl/Vec.h"
 #include "prop/bvminisat/utils/Options.h"
-
+#include "util/resource_manager.h"
 
 namespace CVC4 {
 
@@ -64,8 +64,8 @@ public:
    */
   virtual void notify(vec<Lit>& learnt) = 0;
 
-  virtual void spendResource(unsigned amount) = 0;
-  virtual void safePoint(unsigned amount) = 0;
+  virtual void spendResource(ResourceManager::Resource r) = 0;
+  virtual void safePoint(ResourceManager::Resource r) = 0;
 };
 
 //=================================================================================================
@@ -347,7 +347,7 @@ public:
     CRef     reason           (Var x) const;
     int      level            (Var x) const;
     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
-    bool     withinBudget     (uint64_t amount)      const;
+    bool withinBudget(ResourceManager::Resource r) const;
 
     // Static helpers:
     //