Refactor resource manager (#6322)

This PR does another round of refactoring of the resource manager and related code.

- it moves the Resource enum out of the ResourceManager class
- it treats the resources in a generic way (storing the statistics in a vector) instead of the manual treatment we had before
- weights no longer live in the options, but in the ResourceManager and are changed accordingly in the ResourceManager constructor
- following the generic treatment of resources, it also removes all the resource-specific options --x-step in favor of a generic --rweight name=weight
- removed several unused methods from the ResourceManager

Note that we handle the Resource enum in a way that allows to easily use other enums as additional resources, for example InferenceId. The general idea is that we will at some point have sensible default weights (so that the cumulative resources somewhat simulate the solver runtime) and users (almost) never need to modify them.

2 files changed, 147 insertions, 226 deletions

diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index 56d760384..d0074c444 100644
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -67,106 +67,113 @@ bool WallClockTimer::expired() const
 
 /*---------------------------------------------------------------------------*/
 
+const char* toString(Resource r)
+{
+  switch (r)
+  {
+    case Resource::ArithPivotStep: return "ArithPivotStep";
+    case Resource::ArithNlLemmaStep: return "ArithNlLemmaStep";
+    case Resource::BitblastStep: return "BitblastStep";
+    case Resource::BvEagerAssertStep: return "BvEagerAssertStep";
+    case Resource::BvPropagationStep: return "BvPropagationStep";
+    case Resource::BvSatConflictsStep: return "BvSatConflictsStep";
+    case Resource::BvSatPropagateStep: return "BvSatPropagateStep";
+    case Resource::BvSatSimplifyStep: return "BvSatSimplifyStep";
+    case Resource::CnfStep: return "CnfStep";
+    case Resource::DecisionStep: return "DecisionStep";
+    case Resource::LemmaStep: return "LemmaStep";
+    case Resource::NewSkolemStep: return "NewSkolemStep";
+    case Resource::ParseStep: return "ParseStep";
+    case Resource::PreprocessStep: return "PreprocessStep";
+    case Resource::QuantifierStep: return "QuantifierStep";
+    case Resource::RestartStep: return "RestartStep";
+    case Resource::RewriteStep: return "RewriteStep";
+    case Resource::SatConflictStep: return "SatConflictStep";
+    case Resource::TheoryCheckStep: return "TheoryCheckStep";
+    default: return "?Resource?";
+  }
+}
+
 struct ResourceManager::Statistics
 {
   ReferenceStat<std::uint64_t> d_resourceUnitsUsed;
   IntStat d_spendResourceCalls;
-  IntStat d_numArithPivotStep;
-  IntStat d_numArithNlLemmaStep;
-  IntStat d_numBitblastStep;
-  IntStat d_numBvEagerAssertStep;
-  IntStat d_numBvPropagationStep;
-  IntStat d_numBvSatConflictsStep;
-  IntStat d_numBvSatPropagateStep;
-  IntStat d_numBvSatSimplifyStep;
-  IntStat d_numCnfStep;
-  IntStat d_numDecisionStep;
-  IntStat d_numLemmaStep;
-  IntStat d_numNewSkolemStep;
-  IntStat d_numParseStep;
-  IntStat d_numPreprocessStep;
-  IntStat d_numQuantifierStep;
-  IntStat d_numRestartStep;
-  IntStat d_numRewriteStep;
-  IntStat d_numSatConflictStep;
-  IntStat d_numTheoryCheckStep;
+  std::vector<IntStat> d_resourceSteps;
   Statistics(StatisticsRegistry& stats);
   ~Statistics();
 
+  void bump(Resource r, uint64_t amount)
+  {
+    bump_impl(static_cast<std::size_t>(r), amount, d_resourceSteps);
+  }
+
  private:
+  void bump_impl(std::size_t id, uint64_t amount, std::vector<IntStat>& stats)
+  {
+    Assert(stats.size() > id);
+    stats[id] += amount;
+  }
+
   StatisticsRegistry& d_statisticsRegistry;
 };
 
 ResourceManager::Statistics::Statistics(StatisticsRegistry& stats)
     : d_resourceUnitsUsed("resource::resourceUnitsUsed"),
       d_spendResourceCalls("resource::spendResourceCalls", 0),
-      d_numArithPivotStep("resource::ArithPivotStep", 0),
-      d_numArithNlLemmaStep("resource::ArithNlLemmaStep", 0),
-      d_numBitblastStep("resource::BitblastStep", 0),
-      d_numBvEagerAssertStep("resource::BvEagerAssertStep", 0),
-      d_numBvPropagationStep("resource::BvPropagationStep", 0),
-      d_numBvSatConflictsStep("resource::BvSatConflictsStep", 0),
-      d_numBvSatPropagateStep("resource::BvSatPropagateStep", 0),
-      d_numBvSatSimplifyStep("resource::BvSatSimplifyStep", 0),
-      d_numCnfStep("resource::CnfStep", 0),
-      d_numDecisionStep("resource::DecisionStep", 0),
-      d_numLemmaStep("resource::LemmaStep", 0),
-      d_numNewSkolemStep("resource::NewSkolemStep", 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_resourceUnitsUsed);
   d_statisticsRegistry.registerStat(&d_spendResourceCalls);
-  d_statisticsRegistry.registerStat(&d_numArithPivotStep);
-  d_statisticsRegistry.registerStat(&d_numArithNlLemmaStep);
-  d_statisticsRegistry.registerStat(&d_numBitblastStep);
-  d_statisticsRegistry.registerStat(&d_numBvEagerAssertStep);
-  d_statisticsRegistry.registerStat(&d_numBvPropagationStep);
-  d_statisticsRegistry.registerStat(&d_numBvSatConflictsStep);
-  d_statisticsRegistry.registerStat(&d_numBvSatPropagateStep);
-  d_statisticsRegistry.registerStat(&d_numBvSatSimplifyStep);
-  d_statisticsRegistry.registerStat(&d_numCnfStep);
-  d_statisticsRegistry.registerStat(&d_numDecisionStep);
-  d_statisticsRegistry.registerStat(&d_numLemmaStep);
-  d_statisticsRegistry.registerStat(&d_numNewSkolemStep);
-  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);
+
+  // Make sure we don't reallocate the vector
+  d_resourceSteps.reserve(resman_detail::ResourceMax + 1);
+  for (std::size_t id = 0; id <= resman_detail::ResourceMax; ++id)
+  {
+    Resource r = static_cast<Resource>(id);
+    d_resourceSteps.emplace_back("resource::res::" + std::string(toString(r)),
+                                 0);
+    d_statisticsRegistry.registerStat(&d_resourceSteps[id]);
+  }
 }
 
 ResourceManager::Statistics::~Statistics()
 {
   d_statisticsRegistry.unregisterStat(&d_resourceUnitsUsed);
   d_statisticsRegistry.unregisterStat(&d_spendResourceCalls);
-  d_statisticsRegistry.unregisterStat(&d_numArithPivotStep);
-  d_statisticsRegistry.unregisterStat(&d_numArithNlLemmaStep);
-  d_statisticsRegistry.unregisterStat(&d_numBitblastStep);
-  d_statisticsRegistry.unregisterStat(&d_numBvEagerAssertStep);
-  d_statisticsRegistry.unregisterStat(&d_numBvPropagationStep);
-  d_statisticsRegistry.unregisterStat(&d_numBvSatConflictsStep);
-  d_statisticsRegistry.unregisterStat(&d_numBvSatPropagateStep);
-  d_statisticsRegistry.unregisterStat(&d_numBvSatSimplifyStep);
-  d_statisticsRegistry.unregisterStat(&d_numCnfStep);
-  d_statisticsRegistry.unregisterStat(&d_numDecisionStep);
-  d_statisticsRegistry.unregisterStat(&d_numLemmaStep);
-  d_statisticsRegistry.unregisterStat(&d_numNewSkolemStep);
-  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);
+
+  for (auto& stat : d_resourceSteps)
+  {
+    d_statisticsRegistry.unregisterStat(&stat);
+  }
+}
+
+bool parseOption(const std::string& optarg, std::string& name, uint64_t& weight)
+{
+  auto pos = optarg.find('=');
+  // Check if there is a '='
+  if (pos == std::string::npos) return false;
+  // The name is the part before '='
+  name = optarg.substr(0, pos);
+  // The weight is the part after '='
+  std::string num = optarg.substr(pos + 1);
+  std::size_t converted;
+  weight = std::stoull(num, &converted);
+  // Check everything after '=' was converted
+  return converted == num.size();
+}
+
+template <typename T, typename Weights>
+bool setWeight(const std::string& name, uint64_t weight, Weights& weights)
+{
+  for (std::size_t i = 0; i < weights.size(); ++i)
+  {
+    if (name == toString(static_cast<T>(i)))
+    {
+      weights[i] = weight;
+      return true;
+    }
+  }
+  return false;
 }
 
 /*---------------------------------------------------------------------------*/
@@ -180,19 +187,28 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options)
       d_cumulativeResourceUsed(0),
       d_thisCallResourceUsed(0),
       d_thisCallResourceBudget(0),
-      d_on(false),
-      d_statistics(new ResourceManager::Statistics(stats)),
-      d_options(options)
-
+      d_statistics(new ResourceManager::Statistics(stats))
 {
   d_statistics->d_resourceUnitsUsed.set(d_cumulativeResourceUsed);
+
+  d_resourceWeights.fill(1);
+  for (const auto& opt :
+       options[cvc5::options::resourceWeightHolder__option_t()])
+  {
+    std::string name;
+    uint64_t weight;
+    if (parseOption(opt, name, weight))
+    {
+      if (setWeight<Resource>(name, weight, d_resourceWeights)) continue;
+      throw OptionException("Did not recognize resource type " + name);
+    }
+  }
 }
 
 ResourceManager::~ResourceManager() {}
 
 void ResourceManager::setResourceLimit(uint64_t units, bool cumulative)
 {
-  d_on = true;
   if (cumulative)
   {
     Trace("limit") << "ResourceManager: setting cumulative resource limit to "
@@ -211,7 +227,6 @@ void ResourceManager::setResourceLimit(uint64_t units, bool cumulative)
 
 void ResourceManager::setTimeLimit(uint64_t millis)
 {
-  d_on = true;
   Trace("limit") << "ResourceManager: setting per-call time limit to " << millis
                  << " ms" << endl;
   d_timeBudgetPerCall = millis;
@@ -231,11 +246,10 @@ uint64_t ResourceManager::getResourceRemaining() const
   return d_resourceBudgetCumulative - d_cumulativeResourceUsed;
 }
 
-void ResourceManager::spendResource(unsigned amount)
+void ResourceManager::spendResource(uint64_t amount)
 {
   ++d_statistics->d_spendResourceCalls;
   d_cumulativeResourceUsed += amount;
-  if (!d_on) return;
 
   Debug("limit") << "ResourceManager::spendResource()" << std::endl;
   d_thisCallResourceUsed += amount;
@@ -259,95 +273,16 @@ void ResourceManager::spendResource(unsigned amount)
 
 void ResourceManager::spendResource(Resource r)
 {
-  uint32_t amount = 0;
-  switch (r)
-  {
-    case Resource::ArithPivotStep:
-      amount = d_options[options::arithPivotStep];
-      ++d_statistics->d_numArithPivotStep;
-      break;
-    case Resource::ArithNlLemmaStep:
-      amount = d_options[options::arithNlLemmaStep];
-      ++d_statistics->d_numArithNlLemmaStep;
-      break;
-    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::BvSatPropagateStep:
-      amount = d_options[options::bvSatPropagateStep];
-      ++d_statistics->d_numBvSatPropagateStep;
-      break;
-    case Resource::BvSatSimplifyStep:
-      amount = d_options[options::bvSatSimplifyStep];
-      ++d_statistics->d_numBvSatSimplifyStep;
-      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::NewSkolemStep:
-      amount = d_options[options::newSkolemStep];
-      ++d_statistics->d_numNewSkolemStep;
-      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);
+  std::size_t i = static_cast<std::size_t>(r);
+  Assert(d_resourceWeights.size() > i);
+  d_statistics->bump(r, d_resourceWeights[i]);
+  spendResource(d_resourceWeights[i]);
 }
 
 void ResourceManager::beginCall()
 {
   d_perCallTimer.set(d_timeBudgetPerCall);
   d_thisCallResourceUsed = 0;
-  if (!d_on) return;
 
   if (d_resourceBudgetCumulative > 0)
   {
@@ -372,14 +307,10 @@ void ResourceManager::endCall()
   d_thisCallResourceUsed = 0;
 }
 
-bool ResourceManager::cumulativeLimitOn() const
+bool ResourceManager::limitOn() const
 {
-  return d_resourceBudgetCumulative > 0;
-}
-
-bool ResourceManager::perCallLimitOn() const
-{
-  return (d_timeBudgetPerCall > 0) || (d_resourceBudgetPerCall > 0);
+  return (d_resourceBudgetCumulative > 0) || (d_timeBudgetPerCall > 0)
+         || (d_resourceBudgetPerCall > 0);
 }
 
 bool ResourceManager::outOfResources() const
@@ -409,12 +340,6 @@ bool ResourceManager::outOfTime() const
   return d_perCallTimer.expired();
 }
 
-void ResourceManager::enable(bool on)
-{
-  Trace("limit") << "ResourceManager::enable(" << on << ")\n";
-  d_on = on;
-}
-
 void ResourceManager::registerListener(Listener* listener)
 {
   return d_listeners.push_back(listener);
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index 526e9f5f3..1d5dd7d42 100644
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -21,6 +21,8 @@
 #define CVC5__RESOURCE_MANAGER_H
 
 #include <stdint.h>
+
+#include <array>
 #include <chrono>
 #include <memory>
 #include <vector>
@@ -65,39 +67,46 @@ class WallClockTimer
   time_point d_limit;
 };
 
+/** Types of resources. */
+enum class Resource
+{
+  ArithPivotStep,
+  ArithNlLemmaStep,
+  BitblastStep,
+  BvEagerAssertStep,
+  BvPropagationStep,
+  BvSatConflictsStep,
+  BvSatPropagateStep,
+  BvSatSimplifyStep,
+  CnfStep,
+  DecisionStep,
+  LemmaStep,
+  NewSkolemStep,
+  ParseStep,
+  PreprocessStep,
+  QuantifierStep,
+  RestartStep,
+  RewriteStep,
+  SatConflictStep,
+  TheoryCheckStep,
+  Unknown
+};
+
+const char* toString(Resource r);
+
+namespace resman_detail {
+constexpr std::size_t ResourceMax = static_cast<std::size_t>(Resource::Unknown);
+};  // namespace resman_detail
+
 /**
  * This class manages resource limits (cumulative or per call) and (per call)
- * time limits. The available resources are listed in ResourceManager::Resource
- * and their individual costs are configured via command line options.
+ * time limits. The available resources are listed in Resource and their individual
+ * costs are configured via command line options.
  */
 class ResourceManager
 {
  public:
-  /** Types of resources. */
-  enum class Resource
-  {
-    ArithPivotStep,
-    ArithNlLemmaStep,
-    BitblastStep,
-    BvEagerAssertStep,
-    BvPropagationStep,
-    BvSatConflictsStep,
-    BvSatPropagateStep,
-    BvSatSimplifyStep,
-    CnfStep,
-    DecisionStep,
-    LemmaStep,
-    NewSkolemStep,
-    ParseStep,
-    PreprocessStep,
-    QuantifierStep,
-    RestartStep,
-    RewriteStep,
-    SatConflictStep,
-    TheoryCheckStep,
-  };
-
-  /** Construst a resource manager. */
+  /** Construct a resource manager. */
   ResourceManager(StatisticsRegistry& statistics_registry, Options& options);
   /** Default destructor. */
   ~ResourceManager();
@@ -111,18 +120,14 @@ class ResourceManager
   ResourceManager& operator=(ResourceManager&&) = delete;
 
   /** Checks whether any limit is active. */
-  bool limitOn() const { return cumulativeLimitOn() || perCallLimitOn(); }
-  /** Checks whether any cumulative limit is active. */
-  bool cumulativeLimitOn() const;
-  /** Checks whether any per-call limit is active. */
-  bool perCallLimitOn() const;
+  bool limitOn() const;
 
   /** Checks whether resources have been exhausted. */
   bool outOfResources() const;
   /** Checks whether time has been exhausted. */
   bool outOfTime() const;
   /** Checks whether any limit has been exhausted. */
-  bool out() const { return d_on && (outOfResources() || outOfTime()); }
+  bool out() const { return outOfResources() || outOfTime(); }
 
   /** Retrieves amount of resources used overall. */
   uint64_t getResourceUsage() const;
@@ -131,11 +136,8 @@ class ResourceManager
   /** Retrieves the remaining number of cumulative resources. */
   uint64_t getResourceRemaining() const;
 
-  /** Retrieves resource budget for this call. */
-  uint64_t getResourceBudgetForThisCall() { return d_thisCallResourceBudget; }
-
   /**
-   * Spends a given resources. Throws an UnsafeInterruptException if there are
+   * Spends a given resource. Throws an UnsafeInterruptException if there are
    * no remaining resources.
    */
   void spendResource(Resource r);
@@ -144,8 +146,6 @@ class ResourceManager
   void setResourceLimit(uint64_t units, bool cumulative = false);
   /** Sets the time limit. */
   void setTimeLimit(uint64_t millis);
-  /** Sets whether resource limitation is enabled. */
-  void enable(bool on);
 
   /**
    * Resets perCall limits to mark the start of a new call,
@@ -190,19 +190,15 @@ class ResourceManager
    */
   uint64_t d_thisCallResourceBudget;
 
-  /** A flag indicating whether resource limitation is active. */
-  bool d_on;
-
   /** Receives a notification on reaching a limit. */
   std::vector<Listener*> d_listeners;
 
-  void spendResource(unsigned amount);
+  void spendResource(uint64_t amount);
+
+  std::array<uint64_t, resman_detail::ResourceMax + 1> d_resourceWeights;
 
   struct Statistics;
   std::unique_ptr<Statistics> d_statistics;
-
-  Options& d_options;
-
 }; /* class ResourceManager */
 
 }  // namespace cvc5