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.

10 files changed, 14 insertions, 14 deletions

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) {