From 93fffd49080e29affbf9d5657046d57add929fa8 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Wed, 21 Apr 2021 00:10:17 +0200
Subject: Add InferenceId as resources (#6339)

This PR extends the resource manager to consider theory::InferenceId a resource we can spend. This should give us a robust way to have the resource limiting cover a lot of theory reasoning. To make use of this, TheoryInferenceManager now spends these resources.
Also, it makes the ResourceManager properly use the options from the Env class.
---
 src/util/resource_manager.cpp | 45 +++++++++++++++++++++++--------------------
 src/util/resource_manager.h   | 16 +++++++++++++++
 2 files changed, 40 insertions(+), 21 deletions(-)

(limited to 'src/util')

diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index 40cc415be..f65f938b5 100644
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -93,38 +93,29 @@ const char* toString(Resource r)
     default: return "?Resource?";
   }
 }
+std::ostream& operator<<(std::ostream& os, Resource r)
+{
+  return os << toString(r);
+}
 
 struct ResourceManager::Statistics
 {
   ReferenceStat<uint64_t> d_resourceUnitsUsed;
   IntStat d_spendResourceCalls;
-  std::vector<IntStat> d_resourceSteps;
+  HistogramStat<theory::InferenceId> d_inferenceIdSteps;
+  HistogramStat<Resource> d_resourceSteps;
   Statistics(StatisticsRegistry& stats);
-
-  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;
-  }
 };
 
 ResourceManager::Statistics::Statistics(StatisticsRegistry& stats)
     : d_resourceUnitsUsed(
         stats.registerReference<uint64_t>("resource::resourceUnitsUsed")),
-      d_spendResourceCalls(stats.registerInt("resource::spendResourceCalls"))
+      d_spendResourceCalls(stats.registerInt("resource::spendResourceCalls")),
+      d_inferenceIdSteps(stats.registerHistogram<theory::InferenceId>(
+          "resource::steps::inference-id")),
+      d_resourceSteps(
+          stats.registerHistogram<Resource>("resource::steps::resource"))
 {
-  for (std::size_t id = 0; id <= resman_detail::ResourceMax; ++id)
-  {
-    Resource r = static_cast<Resource>(id);
-    d_resourceSteps.emplace_back(
-        stats.registerInt("resource::res::" + std::string(toString(r))));
-  }
 }
 
 bool parseOption(const std::string& optarg, std::string& name, uint64_t& weight)
@@ -145,6 +136,7 @@ bool parseOption(const std::string& optarg, std::string& name, uint64_t& weight)
 template <typename T, typename Weights>
 bool setWeight(const std::string& name, uint64_t weight, Weights& weights)
 {
+  using theory::toString;
   for (std::size_t i = 0; i < weights.size(); ++i)
   {
     if (name == toString(static_cast<T>(i)))
@@ -167,6 +159,7 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options)
 {
   d_statistics->d_resourceUnitsUsed.set(d_cumulativeResourceUsed);
 
+  d_infidWeights.fill(1);
   d_resourceWeights.fill(1);
   for (const auto& opt :
        options[cvc5::options::resourceWeightHolder__option_t()])
@@ -175,6 +168,8 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options)
     uint64_t weight;
     if (parseOption(opt, name, weight))
     {
+      if (setWeight<theory::InferenceId>(name, weight, d_infidWeights))
+        continue;
       if (setWeight<Resource>(name, weight, d_resourceWeights)) continue;
       throw OptionException("Did not recognize resource type " + name);
     }
@@ -225,10 +220,18 @@ void ResourceManager::spendResource(Resource r)
 {
   std::size_t i = static_cast<std::size_t>(r);
   Assert(d_resourceWeights.size() > i);
-  d_statistics->bump(r, d_resourceWeights[i]);
+  d_statistics->d_resourceSteps << r;
   spendResource(d_resourceWeights[i]);
 }
 
+void ResourceManager::spendResource(theory::InferenceId iid)
+{
+  std::size_t i = static_cast<std::size_t>(iid);
+  Assert(d_infidWeights.size() > i);
+  d_statistics->d_inferenceIdSteps << iid;
+  spendResource(d_infidWeights[i]);
+}
+
 void ResourceManager::beginCall()
 {
   d_perCallTimer.set(options::perCallMillisecondLimit());
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index 1ed7ee0d9..2590799fc 100644
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -27,6 +27,8 @@
 #include <memory>
 #include <vector>
 
+#include "theory/inference_id.h"
+
 namespace cvc5 {
 
 class Listener;
@@ -93,8 +95,13 @@ enum class Resource
 };
 
 const char* toString(Resource r);
+std::ostream& operator<<(std::ostream& os, Resource r);
 
 namespace resman_detail {
+/** The upper bound of values from the theory::InferenceId enum */
+constexpr std::size_t InferenceIdMax =
+    static_cast<std::size_t>(theory::InferenceId::UNKNOWN);
+/** The upper bound of values from the Resource enum */
 constexpr std::size_t ResourceMax = static_cast<std::size_t>(Resource::Unknown);
 };  // namespace resman_detail
 
@@ -141,6 +148,11 @@ class ResourceManager
    * no remaining resources.
    */
   void spendResource(Resource r);
+  /**
+   * Spends a given resource. Throws an UnsafeInterruptException if there are
+   * no remaining resources.
+   */
+  void spendResource(theory::InferenceId iid);
 
   /**
    * Resets perCall limits to mark the start of a new call,
@@ -183,9 +195,13 @@ class ResourceManager
 
   void spendResource(uint64_t amount);
 
+  /** Weights for InferenceId resources */
+  std::array<uint64_t, resman_detail::InferenceIdMax + 1> d_infidWeights;
+  /** Weights for Resource resources */
   std::array<uint64_t, resman_detail::ResourceMax + 1> d_resourceWeights;
 
   struct Statistics;
+  /** The statistics object */
   std::unique_ptr<Statistics> d_statistics;
 }; /* class ResourceManager */
 
-- 
cgit v1.2.3