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.

6 files changed, 54 insertions, 40 deletions

diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index d079682c5..9bb66f649 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -31,7 +31,7 @@ using namespace cvc5::smt;
 
 namespace cvc5 {
 
-Env::Env(NodeManager* nm)
+Env::Env(NodeManager* nm, Options* opts)
     : d_context(new context::Context()),
       d_userContext(new context::UserContext()),
       d_nodeManager(nm),
@@ -40,22 +40,18 @@ Env::Env(NodeManager* nm)
       d_dumpManager(new DumpManager(d_userContext.get())),
       d_logic(),
       d_statisticsRegistry(std::make_unique<StatisticsRegistry>()),
-      d_resourceManager(std::make_unique<ResourceManager>(*d_statisticsRegistry, d_options))
+      d_options(),
+      d_resourceManager()
 {
-}
-
-Env::~Env() {}
-
-void Env::setOptions(Options* optr)
-{
-  if (optr != nullptr)
+  if (opts != nullptr)
   {
-    // if we provided a set of options, copy their values to the options
-    // owned by this Env.
-    d_options.copyValues(*optr);
+    d_options.copyValues(*opts);
   }
+  d_resourceManager = std::make_unique<ResourceManager>(*d_statisticsRegistry, d_options);
 }
 
+Env::~Env() {}
+
 void Env::setProofNodeManager(ProofNodeManager* pnm)
 {
   d_proofNodeManager = pnm;
diff --git a/src/smt/env.h b/src/smt/env.h
index 09e3238ac..209b6f3e7 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -60,7 +60,7 @@ class Env
   /**
    * Construct an Env with the given node manager.
    */
-  Env(NodeManager* nm);
+  Env(NodeManager* nm, Options* opts);
   /** Destruct the env.  */
   ~Env();
 
@@ -116,8 +116,6 @@ class Env
  private:
   /* Private initialization ------------------------------------------------- */
 
-  /** Set options, which makes a deep copy of optr if non-null */
-  void setOptions(Options* optr = nullptr);
   /** Set the statistics registry */
   void setStatisticsRegistry(StatisticsRegistry* statReg);
   /** Set proof node manager if it exists */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 122e69488..3e64c5d23 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -83,7 +83,7 @@ using namespace cvc5::theory;
 namespace cvc5 {
 
 SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
-    : d_env(new Env(nm)),
+    : d_env(new Env(nm, optr)),
       d_state(new SmtEngineState(getContext(), getUserContext(), *this)),
       d_absValues(new AbstractValues(getNodeManager())),
       d_asserts(new Assertions(getUserContext(), *d_absValues.get())),
@@ -120,9 +120,6 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
   // On the other hand, this hack breaks use cases where multiple SmtEngine
   // objects are created by the user.
   d_scope.reset(new SmtScope(this));
-  // Set options in the environment, which makes a deep copy of optr if
-  // non-null. This may throw an options exception.
-  d_env->setOptions(optr);
   // set the options manager
   d_optm.reset(new smt::OptionsManager(&getOptions()));
   // listen to node manager events
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 3bc7351fe..ad988e534 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/theory_inference_manager.h"
 
+#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/output_channel.h"
 #include "theory/rewriter.h"
@@ -118,6 +119,7 @@ void TheoryInferenceManager::conflict(TNode conf, InferenceId id)
 void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id)
 {
   d_conflictIdStats << id;
+  smt::currentResourceManager()->spendResource(id);
   Trace("im") << "(conflict " << id << " " << tconf.getProven() << ")"
               << std::endl;
   d_theoryState.notifyInConflict();
@@ -250,6 +252,7 @@ bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem,
     }
   }
   d_lemmaIdStats << id;
+  smt::currentResourceManager()->spendResource(id);
   Trace("im") << "(lemma " << id << " " << tlem.getProven() << ")" << std::endl;
   d_numCurrentLemmas++;
   d_out.trustedLemma(tlem, p);
@@ -370,6 +373,7 @@ bool TheoryInferenceManager::processInternalFact(TNode atom,
                                                  ProofGenerator* pg)
 {
   d_factIdStats << iid;
+  smt::currentResourceManager()->spendResource(iid);
   Trace("im") << "(fact " << iid << " " << (pol ? Node(atom) : atom.notNode())
               << ")" << std::endl;
   // make the node corresponding to the explanation
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 */