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.

21 files changed, 30 insertions, 30 deletions

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index c9ac5f367..9a13944f3 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -3497,7 +3497,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
   for (std::size_t i = 0; i < nPivots; ++i)
   {
     d_containing.d_out->spendResource(
-        ResourceManager::Resource::ArithPivotStep);
+        Resource::ArithPivotStep);
   }
 
   Debug("arith::ems") << "ems: " << emmittedConflictOrSplit
diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index 38a8a8540..24a833fcc 100644
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -108,12 +108,12 @@ class MinisatEmptyNotify : public prop::BVSatSolverNotify
   MinisatEmptyNotify() {}
   bool notify(prop::SatLiteral lit) override { return true; }
   void notify(prop::SatClause& clause) override {}
-  void spendResource(ResourceManager::Resource r) override
+  void spendResource(Resource r) override
   {
     smt::currentResourceManager()->spendResource(r);
   }
 
-  void safePoint(ResourceManager::Resource r) override {}
+  void safePoint(Resource r) override {}
 };
 
 // Bitblaster implementation
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 04e4a3c50..ed02746ed 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -148,7 +148,7 @@ void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
     return;
   }
 
-  d_bv->spendResource(ResourceManager::Resource::BitblastStep);
+  d_bv->spendResource(Resource::BitblastStep);
   Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n";
 
   d_termBBStrategies[node.getKind()](node, bits, this);
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 0131b7a95..3a2bb6432 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -225,7 +225,7 @@ void TLazyBitblaster::bbTerm(TNode node, Bits& bits) {
   }
   Assert(node.getType().isBitVector());
 
-  d_bv->spendResource(ResourceManager::Resource::BitblastStep);
+  d_bv->spendResource(Resource::BitblastStep);
   Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n";
   ++d_statistics.d_numTerms;
 
@@ -421,12 +421,12 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) {
   }
 }
 
-void TLazyBitblaster::MinisatNotify::spendResource(ResourceManager::Resource r)
+void TLazyBitblaster::MinisatNotify::spendResource(Resource r)
 {
   d_bv->spendResource(r);
 }
 
-void TLazyBitblaster::MinisatNotify::safePoint(ResourceManager::Resource r)
+void TLazyBitblaster::MinisatNotify::safePoint(Resource r)
 {
   d_bv->d_im.safePoint(r);
 }
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index 6af9be7aa..52230c3b5 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.h
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -120,8 +120,8 @@ class TLazyBitblaster : public TBitblaster<Node>
 
     bool notify(prop::SatLiteral lit) override;
     void notify(prop::SatClause& clause) override;
-    void spendResource(ResourceManager::Resource r) override;
-    void safePoint(ResourceManager::Resource r) override;
+    void spendResource(Resource r) override;
+    void safePoint(Resource r) override;
   };
 
   BVSolverLazy* d_bv;
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 8653cd7b5..2d0ae1931 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -65,7 +65,7 @@ bool EagerBitblastSolver::isInitialized() {
 }
 
 void EagerBitblastSolver::assertFormula(TNode formula) {
-  d_bv->spendResource(ResourceManager::Resource::BvEagerAssertStep);
+  d_bv->spendResource(Resource::BvEagerAssertStep);
   Assert(isInitialized());
   Debug("bitvector-eager") << "EagerBitblastSolver::assertFormula " << formula
                            << "\n";
diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index ba114fa2b..a36c4d4fb 100644
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -118,7 +118,7 @@ void BVSolverLazy::finishInit()
   }
 }
 
-void BVSolverLazy::spendResource(ResourceManager::Resource r)
+void BVSolverLazy::spendResource(Resource r)
 {
   d_im.spendResource(r);
 }
diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h
index db1d6c8a3..9129b1c69 100644
--- a/src/theory/bv/bv_solver_lazy.h
+++ b/src/theory/bv/bv_solver_lazy.h
@@ -125,7 +125,7 @@ class BVSolverLazy : public BVSolver
   Statistics d_statistics;
 
   void check(Theory::Effort e);
-  void spendResource(ResourceManager::Resource r);
+  void spendResource(Resource r);
 
   typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
   typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 890ec2cc6..70c9d9de6 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -172,7 +172,7 @@ bool BitblastSolver::check(Theory::Effort e)
   // We need to ensure we are fully propagated, so propagate now
   if (d_useSatPropagation)
   {
-    d_bv->spendResource(ResourceManager::Resource::BvPropagationStep);
+    d_bv->spendResource(Resource::BvPropagationStep);
     bool ok = d_bitblaster->propagate();
     if (!ok)
     {
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 61301e93c..0a391f474 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -188,7 +188,7 @@ void CoreSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
 bool CoreSolver::check(Theory::Effort e) {
   Trace("bitvector::core") << "CoreSolver::check \n";
 
-  d_bv->d_im.spendResource(ResourceManager::Resource::TheoryCheckStep);
+  d_bv->d_im.spendResource(Resource::TheoryCheckStep);
 
   d_checkCalled = true;
   Assert(!d_bv->inConflict());
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 3864defc7..3613584fe 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -33,7 +33,7 @@ bool InequalitySolver::check(Theory::Effort e) {
   Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n";
   TimerStat::CodeTimer inequalityTimer(d_statistics.d_solveTime);
   ++(d_statistics.d_numCallstoCheck);
-  d_bv->spendResource(ResourceManager::Resource::TheoryCheckStep);
+  d_bv->spendResource(Resource::TheoryCheckStep);
 
   bool ok = true;
   while (!done() && ok) {
diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp
index dd68cb8e5..d5ce5ab79 100644
--- a/src/theory/engine_output_channel.cpp
+++ b/src/theory/engine_output_channel.cpp
@@ -60,7 +60,7 @@ EngineOutputChannel::EngineOutputChannel(TheoryEngine* engine,
 {
 }
 
-void EngineOutputChannel::safePoint(ResourceManager::Resource r)
+void EngineOutputChannel::safePoint(Resource r)
 {
   spendResource(r);
   if (d_engine->d_interrupted)
@@ -146,7 +146,7 @@ void EngineOutputChannel::setIncomplete(IncompleteId id)
   d_engine->setIncomplete(d_theory, id);
 }
 
-void EngineOutputChannel::spendResource(ResourceManager::Resource r)
+void EngineOutputChannel::spendResource(Resource r)
 {
   d_engine->spendResource(r);
 }
diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h
index 00f2f2acb..493edd512 100644
--- a/src/theory/engine_output_channel.h
+++ b/src/theory/engine_output_channel.h
@@ -46,7 +46,7 @@ class EngineOutputChannel : public theory::OutputChannel
  public:
   EngineOutputChannel(TheoryEngine* engine, theory::TheoryId theory);
 
-  void safePoint(ResourceManager::Resource r) override;
+  void safePoint(Resource r) override;
 
   void conflict(TNode conflictNode) override;
   bool propagate(TNode literal) override;
@@ -61,7 +61,7 @@ class EngineOutputChannel : public theory::OutputChannel
 
   void setIncomplete(IncompleteId id) override;
 
-  void spendResource(ResourceManager::Resource r) override;
+  void spendResource(Resource r) override;
 
   void handleUserAttribute(const char* attr, theory::Theory* t) override;
 
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index a3a656cec..615484358 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -90,7 +90,7 @@ class OutputChannel {
    *
    * @throws Interrupted if the theory can be safely interrupted.
    */
-  virtual void safePoint(ResourceManager::Resource r) {}
+  virtual void safePoint(Resource r) {}
 
   /**
    * Indicate a theory conflict has arisen.
@@ -163,7 +163,7 @@ class OutputChannel {
    * long-running operations, they cannot rely on resource() to break
    * out of infinite or intractable computations.
    */
-  virtual void spendResource(ResourceManager::Resource r) {}
+  virtual void spendResource(Resource r) {}
 
   /**
    * Handle user attribute.
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index b193b94b4..b45380f5e 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -100,7 +100,7 @@ bool Instantiate::addInstantiation(Node q,
                                    bool doVts)
 {
   // For resource-limiting (also does a time check).
-  d_qim.safePoint(ResourceManager::Resource::QuantifierStep);
+  d_qim.safePoint(Resource::QuantifierStep);
   Assert(!d_qstate.isInConflict());
   Assert(terms.size() == q[0].getNumChildren());
   Trace("inst-add-debug") << "For quantified formula " << q
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 2916088aa..5cea6592c 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -220,7 +220,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
   for (;;){
     if (hasSmtEngine)
     {
-      rm->spendResource(ResourceManager::Resource::RewriteStep);
+      rm->spendResource(Resource::RewriteStep);
     }
 
     // Get the top of the recursion stack
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 4e922410f..78a83c4da 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -489,7 +489,7 @@ void Theory::check(Effort level)
   }
   Assert(d_theoryState!=nullptr);
   // standard calls for resource, stats
-  d_out->spendResource(ResourceManager::Resource::TheoryCheckStep);
+  d_out->spendResource(Resource::TheoryCheckStep);
   TimerStat::CodeTimer checkTimer(d_checkTime);
   Trace("theory-check") << "Theory::preCheck " << level << " " << d_id
                         << std::endl;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 8b11b3198..8c030351b 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1907,7 +1907,7 @@ std::pair<bool, Node> TheoryEngine::entailmentCheck(options::TheoryOfMode mode,
   }
 }
 
-void TheoryEngine::spendResource(ResourceManager::Resource r)
+void TheoryEngine::spendResource(Resource r)
 {
   d_resourceManager->spendResource(r);
 }
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index dd3ca4f99..4da9a38dd 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -302,7 +302,7 @@ class TheoryEngine {
   void interrupt();
 
   /** "Spend" a resource during a search or preprocessing.*/
-  void spendResource(ResourceManager::Resource r);
+  void spendResource(Resource r);
 
   /**
    * Adds a theory. Only one theory per TheoryId can be present, so if
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 467ed0a28..e52321c49 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -508,12 +508,12 @@ void TheoryInferenceManager::requirePhase(TNode n, bool pol)
   return d_out.requirePhase(n, pol);
 }
 
-void TheoryInferenceManager::spendResource(ResourceManager::Resource r)
+void TheoryInferenceManager::spendResource(Resource r)
 {
   d_out.spendResource(r);
 }
 
-void TheoryInferenceManager::safePoint(ResourceManager::Resource r)
+void TheoryInferenceManager::safePoint(Resource r)
 {
   d_out.safePoint(r);
 }
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index c2d5ce52b..c9d198e2c 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -361,12 +361,12 @@ class TheoryInferenceManager
   /**
    * Forward to OutputChannel::spendResource() to spend resources.
    */
-  void spendResource(ResourceManager::Resource r);
+  void spendResource(Resource r);
 
   /**
    * Forward to OutputChannel::safePoint() to spend resources.
    */
-  void safePoint(ResourceManager::Resource r);
+  void safePoint(Resource r);
   /**
    * Notification from a theory that it realizes it is incomplete at
    * this context level.