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.

1 files changed, 167 insertions, 18 deletions

diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index 8f00a23ea..2667d8513 100644
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -19,6 +19,7 @@
 #include "base/check.h"
 #include "base/output.h"
 #include "options/smt_options.h"
+#include "util/statistics_registry.h"
 
 using namespace std;
 
@@ -100,28 +101,110 @@ bool Timer::expired() const {
   return false;
 }
 
+/*---------------------------------------------------------------------------*/
+
+struct ResourceManager::Statistics
+{
+  IntStat d_numBitblastStep;
+  IntStat d_numBvEagerAssertStep;
+  IntStat d_numBvPropagationStep;
+  IntStat d_numBvSatConflictsStep;
+  IntStat d_numCnfStep;
+  IntStat d_numDecisionStep;
+  IntStat d_numLemmaStep;
+  IntStat d_numParseStep;
+  IntStat d_numPreprocessStep;
+  IntStat d_numQuantifierStep;
+  IntStat d_numRestartStep;
+  IntStat d_numRewriteStep;
+  IntStat d_numSatConflictStep;
+  IntStat d_numTheoryCheckStep;
+  Statistics(StatisticsRegistry& stats);
+  ~Statistics();
+
+ private:
+  StatisticsRegistry& d_statisticsRegistry;
+};
+
+ResourceManager::Statistics::Statistics(StatisticsRegistry& stats)
+    : d_numBitblastStep("resource::BitblastStep", 0),
+      d_numBvEagerAssertStep("resource::BvEagerAssertStep", 0),
+      d_numBvPropagationStep("resource::BvPropagationStep", 0),
+      d_numBvSatConflictsStep("resource::BvSatConflictsStep", 0),
+      d_numCnfStep("resource::CnfStep", 0),
+      d_numDecisionStep("resource::DecisionStep", 0),
+      d_numLemmaStep("resource::LemmaStep", 0),
+      d_numParseStep("resource::ParseStep", 0),
+      d_numPreprocessStep("resource::PreprocessStep", 0),
+      d_numQuantifierStep("resource::QuantifierStep", 0),
+      d_numRestartStep("resource::RestartStep", 0),
+      d_numRewriteStep("resource::RewriteStep", 0),
+      d_numSatConflictStep("resource::SatConflictStep", 0),
+      d_numTheoryCheckStep("resource::TheoryCheckStep", 0),
+      d_statisticsRegistry(stats)
+{
+  d_statisticsRegistry.registerStat(&d_numBitblastStep);
+  d_statisticsRegistry.registerStat(&d_numBvEagerAssertStep);
+  d_statisticsRegistry.registerStat(&d_numBvPropagationStep);
+  d_statisticsRegistry.registerStat(&d_numBvSatConflictsStep);
+  d_statisticsRegistry.registerStat(&d_numCnfStep);
+  d_statisticsRegistry.registerStat(&d_numDecisionStep);
+  d_statisticsRegistry.registerStat(&d_numLemmaStep);
+  d_statisticsRegistry.registerStat(&d_numParseStep);
+  d_statisticsRegistry.registerStat(&d_numPreprocessStep);
+  d_statisticsRegistry.registerStat(&d_numQuantifierStep);
+  d_statisticsRegistry.registerStat(&d_numRestartStep);
+  d_statisticsRegistry.registerStat(&d_numRewriteStep);
+  d_statisticsRegistry.registerStat(&d_numSatConflictStep);
+  d_statisticsRegistry.registerStat(&d_numTheoryCheckStep);
+}
+
+ResourceManager::Statistics::~Statistics()
+{
+  d_statisticsRegistry.unregisterStat(&d_numBitblastStep);
+  d_statisticsRegistry.unregisterStat(&d_numBvEagerAssertStep);
+  d_statisticsRegistry.unregisterStat(&d_numBvPropagationStep);
+  d_statisticsRegistry.unregisterStat(&d_numBvSatConflictsStep);
+  d_statisticsRegistry.unregisterStat(&d_numCnfStep);
+  d_statisticsRegistry.unregisterStat(&d_numDecisionStep);
+  d_statisticsRegistry.unregisterStat(&d_numLemmaStep);
+  d_statisticsRegistry.unregisterStat(&d_numParseStep);
+  d_statisticsRegistry.unregisterStat(&d_numPreprocessStep);
+  d_statisticsRegistry.unregisterStat(&d_numQuantifierStep);
+  d_statisticsRegistry.unregisterStat(&d_numRestartStep);
+  d_statisticsRegistry.unregisterStat(&d_numRewriteStep);
+  d_statisticsRegistry.unregisterStat(&d_numSatConflictStep);
+  d_statisticsRegistry.unregisterStat(&d_numTheoryCheckStep);
+}
+
+/*---------------------------------------------------------------------------*/
+
 const uint64_t ResourceManager::s_resourceCount = 1000;
 
-ResourceManager::ResourceManager()
-  : d_cumulativeTimer()
-  , d_perCallTimer()
-  , d_timeBudgetCumulative(0)
-  , d_timeBudgetPerCall(0)
-  , d_resourceBudgetCumulative(0)
-  , d_resourceBudgetPerCall(0)
-  , d_cumulativeTimeUsed(0)
-  , d_cumulativeResourceUsed(0)
-  , d_thisCallResourceUsed(0)
-  , d_thisCallTimeBudget(0)
-  , d_thisCallResourceBudget(0)
-  , d_isHardLimit()
-  , d_on(false)
-  , d_cpuTime(false)
-  , d_spendResourceCalls(0)
-  , d_hardListeners()
-  , d_softListeners()
+ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options)
+    : d_cumulativeTimer(),
+      d_perCallTimer(),
+      d_timeBudgetCumulative(0),
+      d_timeBudgetPerCall(0),
+      d_resourceBudgetCumulative(0),
+      d_resourceBudgetPerCall(0),
+      d_cumulativeTimeUsed(0),
+      d_cumulativeResourceUsed(0),
+      d_thisCallResourceUsed(0),
+      d_thisCallTimeBudget(0),
+      d_thisCallResourceBudget(0),
+      d_isHardLimit(),
+      d_on(false),
+      d_cpuTime(false),
+      d_spendResourceCalls(0),
+      d_hardListeners(),
+      d_softListeners(),
+      d_statistics(new ResourceManager::Statistics(stats)),
+      d_options(options)
+
 {}
 
+ResourceManager::~ResourceManager() {}
 
 void ResourceManager::setResourceLimit(uint64_t units, bool cumulative) {
   d_on = true;
@@ -199,6 +282,72 @@ void ResourceManager::spendResource(unsigned amount)
   }
 }
 
+void ResourceManager::spendResource(Resource r)
+{
+  uint32_t amount = 0;
+  switch (r)
+  {
+    case Resource::BitblastStep:
+      amount = d_options[options::bitblastStep];
+      ++d_statistics->d_numBitblastStep;
+      break;
+    case Resource::BvEagerAssertStep:
+      amount = d_options[options::bvEagerAssertStep];
+      ++d_statistics->d_numBvEagerAssertStep;
+      break;
+    case Resource::BvPropagationStep:
+      amount = d_options[options::bvPropagationStep];
+      ++d_statistics->d_numBvPropagationStep;
+      break;
+    case Resource::BvSatConflictsStep:
+      amount = d_options[options::bvSatConflictStep];
+      ++d_statistics->d_numBvSatConflictsStep;
+      break;
+    case Resource::CnfStep:
+      amount = d_options[options::cnfStep];
+      ++d_statistics->d_numCnfStep;
+      break;
+    case Resource::DecisionStep:
+      amount = d_options[options::decisionStep];
+      ++d_statistics->d_numDecisionStep;
+      break;
+    case Resource::LemmaStep:
+      amount = d_options[options::lemmaStep];
+      ++d_statistics->d_numLemmaStep;
+      break;
+    case Resource::ParseStep:
+      amount = d_options[options::parseStep];
+      ++d_statistics->d_numParseStep;
+      break;
+    case Resource::PreprocessStep:
+      amount = d_options[options::preprocessStep];
+      ++d_statistics->d_numPreprocessStep;
+      break;
+    case Resource::QuantifierStep:
+      amount = d_options[options::quantifierStep];
+      ++d_statistics->d_numQuantifierStep;
+      break;
+    case Resource::RestartStep:
+      amount = d_options[options::restartStep];
+      ++d_statistics->d_numRestartStep;
+      break;
+    case Resource::RewriteStep:
+      amount = d_options[options::rewriteStep];
+      ++d_statistics->d_numRewriteStep;
+      break;
+    case Resource::SatConflictStep:
+      amount = d_options[options::satConflictStep];
+      ++d_statistics->d_numSatConflictStep;
+      break;
+    case Resource::TheoryCheckStep:
+      amount = d_options[options::theoryCheckStep];
+      ++d_statistics->d_numTheoryCheckStep;
+      break;
+    default: Unreachable() << "Invalid resource " << std::endl;
+  }
+  spendResource(amount);
+}
+
 void ResourceManager::beginCall() {
 
   d_perCallTimer.set(d_timeBudgetPerCall, !d_cpuTime);