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, 311 insertions, 140 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);
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index 264565a76..659d455f2 100644
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -20,15 +20,20 @@
 #ifndef CVC4__RESOURCE_MANAGER_H
 #define CVC4__RESOURCE_MANAGER_H
 
-#include <cstddef>
 #include <sys/time.h>
 
+#include <cstddef>
+#include <memory>
+
 #include "base/exception.h"
 #include "base/listener.h"
+#include "options/options.h"
 #include "util/unsafe_interrupt_exception.h"
 
 namespace CVC4 {
 
+class StatisticsRegistry;
+
 /**
  * A helper class to keep track of a time budget and signal
  * the PropEngine when the budget expires.
@@ -74,123 +79,145 @@ class CVC4_PUBLIC Timer {
 
 
 class CVC4_PUBLIC ResourceManager {
-
-  Timer d_cumulativeTimer;
-  Timer d_perCallTimer;
-
-  /** A user-imposed cumulative time budget, in milliseconds. 0 = no limit. */
-  uint64_t d_timeBudgetCumulative;
-  /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */
-  uint64_t d_timeBudgetPerCall;
-  /** A user-imposed cumulative resource budget. 0 = no limit. */
-  uint64_t d_resourceBudgetCumulative;
-  /** A user-imposed per-call resource budget. 0 = no limit. */
-  uint64_t d_resourceBudgetPerCall;
-
-  /** The number of milliseconds used. */
-  uint64_t d_cumulativeTimeUsed;
-  /** The amount of resource used. */
-  uint64_t d_cumulativeResourceUsed;
-
-  /** The amount of resource used during this call. */
-  uint64_t d_thisCallResourceUsed;
-
-  /**
-   * The amount of resource budget for this call (min between per call
-   * budget and left-over cumulative budget.
-   */
-  uint64_t d_thisCallTimeBudget;
-  uint64_t d_thisCallResourceBudget;
-
-  bool d_isHardLimit;
-  bool d_on;
-  bool d_cpuTime;
-  uint64_t d_spendResourceCalls;
-
-  /** Counter indicating how often to check resource manager in loops */
-  static const uint64_t s_resourceCount;
-
-  /** Receives a notification on reaching a hard limit. */
-  ListenerCollection d_hardListeners;
-
-  /** Receives a notification on reaching a hard limit. */
-  ListenerCollection d_softListeners;
-
-  /**
-   * ResourceManagers cannot be copied as they are given an explicit
-   * list of Listeners to respond to.
-   */
-  ResourceManager(const ResourceManager&) = delete;
-
-  /**
-   * ResourceManagers cannot be assigned as they are given an explicit
-   * list of Listeners to respond to.
-   */
-  ResourceManager& operator=(const ResourceManager&) = delete;
-
 public:
-
-  ResourceManager();
-
-  bool limitOn() const { return cumulativeLimitOn() || perCallLimitOn(); }
-  bool cumulativeLimitOn() const;
-  bool perCallLimitOn() const;
-
-  bool outOfResources() const;
-  bool outOfTime() const;
-  bool out() const { return d_on && (outOfResources() || outOfTime()); }
-
-
-  /**
-   * This returns a const uint64_t& to support being used as a ReferenceStat.
-   */
-  const uint64_t& getResourceUsage() const;
-  uint64_t getTimeUsage() const;
-  uint64_t getResourceRemaining() const;
-  uint64_t getTimeRemaining() const;
-
-  uint64_t getResourceBudgetForThisCall() {
-    return d_thisCallResourceBudget;
-  }
-  // Throws an UnsafeInterruptException if there are no remaining resources.
-  void spendResource(unsigned amount);
-
-  void setHardLimit(bool value);
-  void setResourceLimit(uint64_t units, bool cumulative = false);
-  void setTimeLimit(uint64_t millis, bool cumulative = false);
-  void useCPUTime(bool cpu);
-
-  void enable(bool on);
-
-  /**
-   * Resets perCall limits to mark the start of a new call,
-   * updates budget for current call and starts the timer
-   */
-  void beginCall();
-
-  /**
-   * Marks the end of a SmtEngine check call, stops the per
-   * call timer, updates cumulative time used.
-   */
-  void endCall();
-
-  static uint64_t getFrequencyCount() { return s_resourceCount; }
-
-  /**
-   * Registers a listener that is notified on a hard resource out.
-   *
-   * This Registration must be destroyed by the user before this
-   * ResourceManager.
-   */
-  ListenerCollection::Registration* registerHardListener(Listener* listener);
-
-  /**
-   * Registers a listener that is notified on a soft resource out.
-   *
-   * This Registration must be destroyed by the user before this
-   * ResourceManager.
-   */
-  ListenerCollection::Registration* registerSoftListener(Listener* listener);
+ enum class Resource
+ {
+   BitblastStep,
+   BvEagerAssertStep,
+   BvPropagationStep,
+   BvSatConflictsStep,
+   CnfStep,
+   DecisionStep,
+   LemmaStep,
+   ParseStep,
+   PreprocessStep,
+   QuantifierStep,
+   RestartStep,
+   RewriteStep,
+   SatConflictStep,
+   TheoryCheckStep,
+ };
+
+ ResourceManager(StatisticsRegistry& statistics_registry, Options& options);
+ ~ResourceManager();
+
+ bool limitOn() const { return cumulativeLimitOn() || perCallLimitOn(); }
+ bool cumulativeLimitOn() const;
+ bool perCallLimitOn() const;
+
+ bool outOfResources() const;
+ bool outOfTime() const;
+ bool out() const { return d_on && (outOfResources() || outOfTime()); }
+
+ /**
+  * This returns a const uint64_t& to support being used as a ReferenceStat.
+  */
+ const uint64_t& getResourceUsage() const;
+ uint64_t getTimeUsage() const;
+ uint64_t getResourceRemaining() const;
+ uint64_t getTimeRemaining() const;
+
+ uint64_t getResourceBudgetForThisCall() { return d_thisCallResourceBudget; }
+ // Throws an UnsafeInterruptException if there are no remaining resources.
+ void spendResource(Resource r);
+
+ void setHardLimit(bool value);
+ void setResourceLimit(uint64_t units, bool cumulative = false);
+ void setTimeLimit(uint64_t millis, bool cumulative = false);
+ void useCPUTime(bool cpu);
+
+ void enable(bool on);
+
+ /**
+  * Resets perCall limits to mark the start of a new call,
+  * updates budget for current call and starts the timer
+  */
+ void beginCall();
+
+ /**
+  * Marks the end of a SmtEngine check call, stops the per
+  * call timer, updates cumulative time used.
+  */
+ void endCall();
+
+ static uint64_t getFrequencyCount() { return s_resourceCount; }
+
+ /**
+  * Registers a listener that is notified on a hard resource out.
+  *
+  * This Registration must be destroyed by the user before this
+  * ResourceManager.
+  */
+ ListenerCollection::Registration* registerHardListener(Listener* listener);
+
+ /**
+  * Registers a listener that is notified on a soft resource out.
+  *
+  * This Registration must be destroyed by the user before this
+  * ResourceManager.
+  */
+ ListenerCollection::Registration* registerSoftListener(Listener* listener);
+
+private:
+ Timer d_cumulativeTimer;
+ Timer d_perCallTimer;
+
+ /** A user-imposed cumulative time budget, in milliseconds. 0 = no limit. */
+ uint64_t d_timeBudgetCumulative;
+ /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */
+ uint64_t d_timeBudgetPerCall;
+ /** A user-imposed cumulative resource budget. 0 = no limit. */
+ uint64_t d_resourceBudgetCumulative;
+ /** A user-imposed per-call resource budget. 0 = no limit. */
+ uint64_t d_resourceBudgetPerCall;
+
+ /** The number of milliseconds used. */
+ uint64_t d_cumulativeTimeUsed;
+ /** The amount of resource used. */
+ uint64_t d_cumulativeResourceUsed;
+
+ /** The amount of resource used during this call. */
+ uint64_t d_thisCallResourceUsed;
+
+ /**
+  * The amount of resource budget for this call (min between per call
+  * budget and left-over cumulative budget.
+  */
+ uint64_t d_thisCallTimeBudget;
+ uint64_t d_thisCallResourceBudget;
+
+ bool d_isHardLimit;
+ bool d_on;
+ bool d_cpuTime;
+ uint64_t d_spendResourceCalls;
+
+ /** Counter indicating how often to check resource manager in loops */
+ static const uint64_t s_resourceCount;
+
+ /** Receives a notification on reaching a hard limit. */
+ ListenerCollection d_hardListeners;
+
+ /** Receives a notification on reaching a hard limit. */
+ ListenerCollection d_softListeners;
+
+ /**
+  * ResourceManagers cannot be copied as they are given an explicit
+  * list of Listeners to respond to.
+  */
+ ResourceManager(const ResourceManager&) = delete;
+
+ /**
+  * ResourceManagers cannot be assigned as they are given an explicit
+  * list of Listeners to respond to.
+  */
+ ResourceManager& operator=(const ResourceManager&) = delete;
+
+ void spendResource(unsigned amount);
+
+ struct Statistics;
+ std::unique_ptr<Statistics> d_statistics;
+
+ Options& d_options;
 
 };/* class ResourceManager */
 
diff --git a/src/util/resource_manager.i b/src/util/resource_manager.i
deleted file mode 100644
index 0f55c2bce..000000000
--- a/src/util/resource_manager.i
+++ /dev/null
@@ -1,5 +0,0 @@
-%{
-#include "util/resource_manager.h"
-%}
-
-%include "util/resource_manager.h"