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.

11 files changed, 46 insertions, 35 deletions

diff --git a/src/prop/bv_sat_solver_notify.h b/src/prop/bv_sat_solver_notify.h
index 77163cfe6..eca6bdfd6 100644
--- a/src/prop/bv_sat_solver_notify.h
+++ b/src/prop/bv_sat_solver_notify.h
@@ -19,6 +19,7 @@
 #define CVC4__PROP__BVSATSOLVERNOTIFY_H
 
 #include "prop/sat_solver_types.h"
+#include "util/resource_manager.h"
 
 namespace CVC4 {
 namespace prop {
@@ -38,8 +39,8 @@ public:
    * Notify about a learnt clause.
    */
   virtual void notify(SatClause& clause) = 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;
 
 };/* class BVSatSolverInterface::Notify */
 
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:
     //
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 6d60bfafc..6690f12db 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -711,7 +711,8 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
                << ", negated = " << (negated ? "true" : "false") << ")" << endl;
 
   if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) {
-    NodeManager::currentResourceManager()->spendResource(options::cnfStep());
+    NodeManager::currentResourceManager()->spendResource(
+        ResourceManager::Resource::CnfStep);
     d_convertAndAssertCounter = 0;
   }
   ++d_convertAndAssertCounter;
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 6126983fa..83f6fb897 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1419,7 +1419,7 @@ lbool Solver::search(int nof_conflicts)
             }
 
             if ((nof_conflicts >= 0 && conflictC >= nof_conflicts)
-                || !withinBudget(options::satConflictStep()))
+                || !withinBudget(ResourceManager::Resource::SatConflictStep))
             {
               // Reached bound on number of conflicts:
               progress_estimate = progressEstimate();
@@ -1558,12 +1558,13 @@ 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(options::satConflictStep())) break; // FIXME add restart option?
+        if (!withinBudget(ResourceManager::Resource::SatConflictStep))
+          break;  // FIXME add restart option?
         curr_restarts++;
     }
 
-    if(!withinBudget(options::satConflictStep()))
-        status = l_Undef;
+    if (!withinBudget(ResourceManager::Resource::SatConflictStep))
+      status = l_Undef;
 
     if (verbosity >= 1)
         printf("===============================================================================\n");
@@ -1778,7 +1779,7 @@ CRef Solver::updateLemmas() {
   Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl;
 
   // Avoid adding lemmas indefinitely without resource-out
-  proxy->spendResource(options::lemmaStep());
+  proxy->spendResource(ResourceManager::Resource::LemmaStep);
 
   CRef conflict = CRef_Undef;
 
@@ -1948,19 +1949,20 @@ void ClauseAllocator::reloc(CRef& cr,
   else if (to[cr].has_extra()) to[cr].calcAbstraction();
 }
 
-inline bool Solver::withinBudget(uint64_t amount) const
+inline bool Solver::withinBudget(ResourceManager::Resource r) const
 {
   Assert(proxy);
   // spendResource sets async_interrupt or throws UnsafeInterruptException
   // depending on whether hard-limit is enabled
-  proxy->spendResource(amount);
+  proxy->spendResource(r);
 
-  bool within_budget =  !asynch_interrupt &&
-    (conflict_budget    < 0 || conflicts < (uint64_t)conflict_budget) &&
-    (propagation_budget < 0 || propagations < (uint64_t)propagation_budget);
+  bool within_budget =
+      !asynch_interrupt
+      && (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget)
+      && (propagation_budget < 0
+          || propagations < (uint64_t)propagation_budget);
   return within_budget;
 }
 
-
 } /* CVC4::Minisat namespace */
 } /* CVC4 namespace */
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index aa3b96c57..0cec30d24 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -440,8 +440,9 @@ protected:
     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
 public:
     bool     withinBudget     (uint64_t amount)      const;
-protected:
+    bool withinBudget(ResourceManager::Resource r) const;
 
+   protected:
     // Static helpers:
     //
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 8a0cc9f15..bac584236 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -295,9 +295,9 @@ void PropEngine::interrupt()
   Debug("prop") << "interrupt()" << endl;
 }
 
-void PropEngine::spendResource(unsigned amount)
+void PropEngine::spendResource(ResourceManager::Resource r)
 {
-  d_resourceManager->spendResource(amount);
+  d_resourceManager->spendResource(r);
 }
 
 bool PropEngine::properExplanation(TNode node, TNode expl) const {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index aaa65b85a..efbd82947 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -29,6 +29,7 @@
 #include "options/options.h"
 #include "proof/proof_manager.h"
 #include "smt_util/lemma_channels.h"
+#include "util/resource_manager.h"
 #include "util/result.h"
 #include "util/unsafe_interrupt_exception.h"
 
@@ -228,7 +229,7 @@ public:
    * Informs the ResourceManager that a resource has been spent.  If out of
    * resources, can throw an UnsafeInterruptException exception.
    */
-  void spendResource(unsigned amount);
+  void spendResource(ResourceManager::Resource r);
 
   /**
    * For debugging.  Return true if "expl" is a well-formed
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 1258d2ee2..cf7c9f0d9 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -161,7 +161,7 @@ TNode TheoryProxy::getNode(SatLiteral lit) {
 }
 
 void TheoryProxy::notifyRestart() {
-  d_propEngine->spendResource(options::restartStep());
+  d_propEngine->spendResource(ResourceManager::Resource::RestartStep);
   d_theoryEngine->notifyRestart();
 
   static uint32_t lemmaCount = 0;
@@ -238,9 +238,9 @@ void TheoryProxy::logDecision(SatLiteral lit) {
 #endif /* CVC4_REPLAY */
 }
 
-void TheoryProxy::spendResource(unsigned amount)
+void TheoryProxy::spendResource(ResourceManager::Resource r)
 {
-  d_theoryEngine->spendResource(amount);
+  d_theoryEngine->spendResource(r);
 }
 
 bool TheoryProxy::isDecisionRelevant(SatVariable var) {
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 3bb15aa4e..61c556f34 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -34,6 +34,7 @@
 #include "smt_util/lemma_input_channel.h"
 #include "smt_util/lemma_output_channel.h"
 #include "theory/theory.h"
+#include "util/resource_manager.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -92,7 +93,7 @@ public:
 
   void logDecision(SatLiteral lit);
 
-  void spendResource(unsigned amount);
+  void spendResource(ResourceManager::Resource r);
 
   bool isDecisionEngineDone();