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.

57 files changed, 246 insertions, 471 deletions

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index a5ffe2c43..12e148500 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -69,7 +69,7 @@ void DecisionEngine::shutdown()
 
 SatLiteral DecisionEngine::getNext(bool& stopSearch)
 {
-  d_resourceManager->spendResource(ResourceManager::Resource::DecisionStep);
+  d_resourceManager->spendResource(Resource::DecisionStep);
   Assert(d_cnfStream != nullptr)
       << "Forgot to set cnfStream for decision engine?";
   Assert(d_satSolver != nullptr)
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index b93186767..4fe93c129 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -23,7 +23,7 @@
       <tpl-src> location of all *_template.{cpp,h} files
       <tpl-doc> location of all *_template documentation files
       <dst>     destination directory for the generated source code files
-      <toml>+   one or more *_optios.toml files
+      <toml>+   one or more *_options.toml files
 
 
     Directory <tpl-src> must contain:
diff --git a/src/options/options.h b/src/options/options.h
index 8abebc253..0bbc31b77 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -183,7 +183,6 @@ public:
   std::ostream* getOut();
   std::ostream* getOutConst() const; // TODO: Remove this.
   std::string getBinaryName() const;
-  unsigned getParseStep() const;
 
   // TODO: Document these.
   void setInputLanguage(InputLanguage);
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 2df4de4bc..28b8073b9 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -34,6 +34,7 @@
 #include "options/didyoumean.h"
 #include "options/language.h"
 #include "options/option_exception.h"
+#include "options/options_holder.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 
@@ -80,6 +81,12 @@ unsigned long OptionsHandler::limitHandler(std::string option,
   }
   return ms;
 }
+
+void OptionsHandler::setResourceWeight(std::string option, std::string optarg)
+{
+  d_options->d_holder->resourceWeightHolder.emplace_back(optarg);
+}
+
 // theory/quantifiers/options_handlers.h
 
 void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode)
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 3e5da9ca1..680f2093c 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -89,6 +89,7 @@ public:
   void statsEnabledBuild(std::string option, bool value);
 
   unsigned long limitHandler(std::string option, std::string optarg);
+  void setResourceWeight(std::string option, std::string optarg);
 
   /* expr/options_handlers.h */
   void setDefaultExprDepthPredicate(std::string option, int depth);
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index f617076d5..3d9c2b669 100644
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -182,10 +182,6 @@ std::string Options::getBinaryName() const{
   return (*this)[options::binary_name];
 }
 
-unsigned Options::getParseStep() const{
-  return (*this)[options::parseStep];
-}
-
 std::ostream* Options::currentGetOut() {
   return current()->getOut();
 }
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 2d678ec2b..c8a1a8fb4 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -466,176 +466,27 @@ header = "options/smt_options.h"
   read_only  = true
   help       = "enable resource limiting per query"
 
-[[option]]
-  name       = "arithPivotStep"
-  category   = "expert"
-  long       = "arith-pivot-step=N"
-  type       = "unsigned"
-  default    = "1"
-  read_only  = true
-  help       = "amount of resources spent for each arithmetic pivot step"
-
-[[option]]
-  name       = "arithNlLemmaStep"
-  category   = "expert"
-  long       = "arith-nl-lemma-step=N"
-  type       = "unsigned"
-  default    = "1"
-  read_only  = true
-  help       = "amount of resources spent for each arithmetic nonlinear lemma step"
-
-[[option]]
-  name       = "rewriteStep"
-  category   = "expert"
-  long       = "rewrite-step=N"
-  type       = "unsigned"
-  default    = "1"
-  read_only  = true
-  help       = "amount of resources spent for each rewrite step"
-
-[[option]]
-  name       = "theoryCheckStep"
-  category   = "expert"
-  long       = "theory-check-step=N"
-  type       = "unsigned"
-  default    = "1"
-  read_only  = true
-  help       = "amount of resources spent for each theory check call"
-
-[[option]]
-  name       = "decisionStep"
-  category   = "expert"
-  long       = "decision-step=N"
-  type       = "unsigned"
-  default    = "1"
-  read_only  = true
-  help       = "amount of getNext decision calls in the decision engine"
-
-[[option]]
-  name       = "bitblastStep"
-  category   = "expert"
-  long       = "bitblast-step=N"
-  type       = "unsigned"
-  default    = "1"
-  read_only  = true
-  help       = "amount of resources spent for each bitblast step"
-
-[[option]]
-  name       = "bvPropagationStep"
-  category   = "expert"
-  long       = "bv-propagation-step=N"
-  type       = "unsigned"
-  default    = "1"
-  read_only  = true
-  help       = "amount of resources spent for each BV propagation step"
-
-[[option]]
-  name       = "bvEagerAssertStep"
-  category   = "expert"
-  long       = "bv-eager-assert-step=N"
-  type       = "unsigned"
-  default    = "1"
-  read_only  = true
-  help       = "amount of resources spent for each eager BV assert step"
-
-[[option]]
-  name       = "parseStep"
-  category   = "expert"
-  long       = "parse-step=N"
-  type       = "unsigned"
-  default    = "1"
-  read_only  = true
-  help       = "amount of resources spent for each command/expression parsing"
-
-[[option]]
-  name       = "lemmaStep"
+# --rweight is used to override the default of one particular resource weight.
+# It can be given multiple times to override multiple weights. When options are
+# parsed, the resource manager might now be created yet, and it is not clear
+# how an option handler would access it in a reasonable way. The option handler
+# thus merely puts the data in another option that holds a vector of strings.
+# This other option "resourceWeightHolder" has the sole purpose of storing
+# this data in a way so that the resource manager can access it in its
+# constructor.
+[[option]]
+  smt_name   = "resourceWeight"
   category   = "expert"
-  long       = "lemma-step=N"
-  type       = "unsigned"
-  default    = "1"
-  read_only  = true
-  help       = "amount of resources spent when adding lemmas"
-
-[[option]]
-  name       = "newSkolemStep"
-  category   = "expert"
-  long       = "new-skolem-step=N"
-  type       = "unsigned"
-  default    = "1"
-  read_only  = true
-  help       = "amount of resources spent when adding new skolems"
-
-[[option]]
-  name       = "restartStep"
-  category   = "expert"
-  long       = "restart-step=N"
-  type       = "unsigned"
-  default    = "1"
-  read_only  = true
-  help       = "amount of resources spent for each theory restart"
-
-[[option]]
-  name       = "cnfStep"
-  category   = "expert"
-  long       = "cnf-step=N"
-  type       = "unsigned"
-  default    = "1"
-  read_only  = true
-  help       = "amount of resources spent for each call to cnf conversion"
-
-[[option]]
-  name       = "preprocessStep"
-  category   = "expert"
-  long       = "preprocess-step=N"
-  type       = "unsigned"
-  default    = "1"
-  read_only  = true
-  help       = "amount of resources spent for each preprocessing step in SmtEngine"
-
-[[option]]
-  name       = "quantifierStep"
-  category   = "expert"
-  long       = "quantifier-step=N"
-  type       = "unsigned"
-  default    = "1"
-  read_only  = true
-  help       = "amount of resources spent for quantifier instantiations"
-
-[[option]]
-  name       = "satConflictStep"
-  category   = "expert"
-  long       = "sat-conflict-step=N"
-  type       = "unsigned"
-  default    = "1"
-  read_only  = true
-  help       = "amount of resources spent for each sat conflict (main sat solver)"
-
-[[option]]
-  name       = "bvSatConflictStep"
-  category   = "expert"
-  long       = "bv-sat-conflict-step=N"
-  type       = "unsigned"
-  default    = "1"
-  read_only  = true
-  help       = "amount of resources spent for each sat conflict (bitvectors)"
-
-[[option]]
-  name       = "bvSatPropagateStep"
-  category   = "expert"
-  long       = "bv-sat-propagate-step=N"
-  type       = "unsigned"
-  default    = "1"
+  long       = "rweight=VAL=N"
+  type       = "std::string"
+  handler    = "setResourceWeight"
   read_only  = true
-  help       = "amount of resources spent for each sat propagate (bitvectors)"
+  help       = "set a single resource weight"
 
 [[option]]
-  name       = "bvSatSimplifyStep"
-  category   = "expert"
-  long       = "bv-sat-simplify-step=N"
-  type       = "unsigned"
-  default    = "1"
-  read_only  = true
-  help       = "amount of resources spent for each sat simplify (bitvectors)"
+  name       = "resourceWeightHolder"
+  category   = "undocumented"
+  type       = "std::vector<std::string>"
 
 [[option]]
   name       = "forceNoLimitCpuWhileDump"
diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index 324cd89b9..20c173316 100644
--- a/src/preprocessing/passes/apply_substs.cpp
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -53,7 +53,7 @@ PreprocessingPassResult ApplySubsts::applyInternal(
     }
     Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i]
                           << std::endl;
-    d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
+    d_preprocContext->spendResource(Resource::PreprocessStep);
     assertionsToPreprocess->replaceTrusted(
         i, tlsm.apply((*assertionsToPreprocess)[i]));
     Trace("apply-substs") << "  got " << (*assertionsToPreprocess)[i]
diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
index dfa0c378d..7fd54420f 100644
--- a/src/preprocessing/passes/bool_to_bv.cpp
+++ b/src/preprocessing/passes/bool_to_bv.cpp
@@ -41,7 +41,7 @@ BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult BoolToBV::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
+  d_preprocContext->spendResource(Resource::PreprocessStep);
 
   size_t size = assertionsToPreprocess->size();
 
diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp
index c30017f31..71719e064 100644
--- a/src/preprocessing/passes/bv_to_bool.cpp
+++ b/src/preprocessing/passes/bv_to_bool.cpp
@@ -48,7 +48,7 @@ BVToBool::BVToBool(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult BVToBool::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
+  d_preprocContext->spendResource(Resource::PreprocessStep);
   std::vector<Node> new_assertions;
   liftBvToBool(assertionsToPreprocess->ref(), new_assertions);
   for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index 278192c97..068e47f13 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -40,7 +40,7 @@ IteRemoval::IteRemoval(PreprocessingPassContext* preprocContext)
 
 PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
 {
-  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
+  d_preprocContext->spendResource(Resource::PreprocessStep);
 
   IteSkolemMap& imap = assertions->getIteSkolemMap();
   // Remove all of the ITE occurrences and normalize
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index efa50e0a0..f79c7fec9 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -236,12 +236,12 @@ ITESimp::ITESimp(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult ITESimp::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
+  d_preprocContext->spendResource(Resource::PreprocessStep);
 
   size_t nasserts = assertionsToPreprocess->size();
   for (size_t i = 0; i < nasserts; ++i)
   {
-    d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
+    d_preprocContext->spendResource(Resource::PreprocessStep);
     Node simp = simpITE(&d_iteUtilities, (*assertionsToPreprocess)[i]);
     assertionsToPreprocess->replace(i, simp);
     if (simp.isConst() && !simp.getConst<bool>())
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index e2b8c0276..c9f20d774 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -77,7 +77,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
   Assert(!options::unsatCores() || isProofEnabled())
       << "Unsat cores with non-clausal simp only supported with new proofs";
 
-  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
+  d_preprocContext->spendResource(Resource::PreprocessStep);
 
   theory::booleans::CircuitPropagator* propagator =
       d_preprocContext->getCircuitPropagator();
diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp
index 278252da9..09d24d900 100644
--- a/src/preprocessing/passes/static_learning.cpp
+++ b/src/preprocessing/passes/static_learning.cpp
@@ -33,7 +33,7 @@ StaticLearning::StaticLearning(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult StaticLearning::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
+  d_preprocContext->spendResource(Resource::PreprocessStep);
 
   for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
   {
diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index 88cc8112d..cc8820226 100644
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -37,7 +37,7 @@ TheoryPreprocess::TheoryPreprocess(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult TheoryPreprocess::applyInternal(
     AssertionPipeline* assertions)
 {
-  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
+  d_preprocContext->spendResource(Resource::PreprocessStep);
 
   IteSkolemMap& imap = assertions->getIteSkolemMap();
   prop::PropEngine* propEngine = d_preprocContext->getPropEngine();
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 922c3bdd5..15b3c62df 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -846,7 +846,7 @@ void UnconstrainedSimplifier::processUnconstrained()
 PreprocessingPassResult UnconstrainedSimplifier::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
+  d_preprocContext->spendResource(Resource::PreprocessStep);
 
   const std::vector<Node>& assertions = assertionsToPreprocess->ref();
 
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index 902db959f..b7d0d37f4 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -62,7 +62,7 @@ class PreprocessingPassContext
     return d_symsInAssertions;
   }
 
-  void spendResource(ResourceManager::Resource r)
+  void spendResource(Resource r)
   {
     d_resourceManager->spendResource(r);
   }
diff --git a/src/prop/bv_sat_solver_notify.h b/src/prop/bv_sat_solver_notify.h
index 45fbf1699..9c1051754 100644
--- a/src/prop/bv_sat_solver_notify.h
+++ b/src/prop/bv_sat_solver_notify.h
@@ -40,8 +40,8 @@ public:
    * Notify about a learnt clause.
    */
   virtual void notify(SatClause& clause) = 0;
-  virtual void spendResource(ResourceManager::Resource r) = 0;
-  virtual void safePoint(ResourceManager::Resource r) = 0;
+  virtual void spendResource(Resource r) = 0;
+  virtual void safePoint(Resource r) = 0;
 
 };/* class BVSatSolverInterface::Notify */
 
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index e7dc3ef0c..5dfc3f9f4 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -47,11 +47,11 @@ class BVMinisatSatSolver : public BVSatSolverInterface,
       return d_notify->notify(toSatLiteral(lit));
     }
     void notify(BVMinisat::vec<BVMinisat::Lit>& clause) override;
-    void spendResource(ResourceManager::Resource r) override
+    void spendResource(Resource r) override
     {
       d_notify->spendResource(r);
     }
-    void safePoint(ResourceManager::Resource r) override
+    void safePoint(Resource r) override
     {
       d_notify->safePoint(r);
     }
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index d154b5e7f..e517b8f74 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -886,7 +886,7 @@ bool Solver::simplify()
 
   if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) return true;
 
-  d_notify->spendResource(ResourceManager::Resource::BvSatSimplifyStep);
+  d_notify->spendResource(Resource::BvSatSimplifyStep);
 
   // Remove satisfied clauses:
   removeSatisfied(learnts);
@@ -927,7 +927,7 @@ lbool Solver::search(int nof_conflicts, UIP uip)
 
   for (;;)
   {
-    d_notify->safePoint(ResourceManager::Resource::BvSatPropagateStep);
+    d_notify->safePoint(Resource::BvSatPropagateStep);
     CRef confl = propagate();
     if (confl != CRef_Undef)
     {
@@ -1026,7 +1026,7 @@ lbool Solver::search(int nof_conflicts, UIP uip)
       try
       {
         isWithinBudget =
-            withinBudget(ResourceManager::Resource::BvSatConflictsStep);
+            withinBudget(Resource::BvSatConflictsStep);
       }
       catch (const cvc5::theory::Interrupted& e)
       {
@@ -1197,7 +1197,7 @@ lbool Solver::solve_()
     while (status == l_Undef){
         double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts);
         status = search(rest_base * restart_first);
-        if (!withinBudget(ResourceManager::Resource::BvSatConflictsStep)) break;
+        if (!withinBudget(Resource::BvSatConflictsStep)) break;
         curr_restarts++;
     }
 
@@ -1406,7 +1406,7 @@ void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to)
 }
 
 void Solver::setNotify(Notify* toNotify) { d_notify = toNotify; }
-bool Solver::withinBudget(ResourceManager::Resource r) const
+bool Solver::withinBudget(Resource r) const
 {
   AlwaysAssert(d_notify);
   d_notify->safePoint(r);
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 3bd43f889..3826eb9f9 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -59,8 +59,8 @@ public:
    */
   virtual void notify(vec<Lit>& learnt) = 0;
 
-  virtual void spendResource(ResourceManager::Resource r) = 0;
-  virtual void safePoint(ResourceManager::Resource r) = 0;
+  virtual void spendResource(Resource r) = 0;
+  virtual void safePoint(Resource r) = 0;
 };
 
 //=================================================================================================
@@ -379,7 +379,7 @@ protected:
     CRef     reason           (Var x) const;
     int      level            (Var x) const;
     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
-    bool withinBudget(ResourceManager::Resource r) const;
+    bool withinBudget(Resource r) const;
 
     // Static helpers:
     //
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 8603d5ca3..0fb4a59b5 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -755,7 +755,7 @@ void CnfStream::convertAndAssert(TNode node, bool negated)
   Trace("cnf") << "convertAndAssert(" << node
                << ", negated = " << (negated ? "true" : "false") << ")\n";
 
-  d_resourceManager->spendResource(ResourceManager::Resource::CnfStep);
+  d_resourceManager->spendResource(Resource::CnfStep);
 
   switch(node.getKind()) {
     case kind::AND: convertAndAssertAnd(node, negated); break;
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index cd3ae5edf..7a7809eef 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1789,7 +1789,7 @@ lbool Solver::search(int nof_conflicts)
       }
 
       if ((nof_conflicts >= 0 && conflictC >= nof_conflicts)
-          || !withinBudget(ResourceManager::Resource::SatConflictStep))
+          || !withinBudget(Resource::SatConflictStep))
       {
         // Reached bound on number of conflicts:
         progress_estimate = progressEstimate();
@@ -1934,12 +1934,12 @@ lbool Solver::solve_()
     while (status == l_Undef){
         double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts);
         status = search(rest_base * restart_first);
-        if (!withinBudget(ResourceManager::Resource::SatConflictStep))
+        if (!withinBudget(Resource::SatConflictStep))
           break;  // FIXME add restart option?
         curr_restarts++;
     }
 
-    if (!withinBudget(ResourceManager::Resource::SatConflictStep))
+    if (!withinBudget(Resource::SatConflictStep))
       status = l_Undef;
 
     if (verbosity >= 1)
@@ -2188,7 +2188,7 @@ CRef Solver::updateLemmas() {
   Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl;
 
   // Avoid adding lemmas indefinitely without resource-out
-  d_proxy->spendResource(ResourceManager::Resource::LemmaStep);
+  d_proxy->spendResource(Resource::LemmaStep);
 
   CRef conflict = CRef_Undef;
 
@@ -2370,7 +2370,7 @@ void ClauseAllocator::reloc(CRef& cr,
   else if (to[cr].has_extra()) to[cr].calcAbstraction();
 }
 
-inline bool Solver::withinBudget(ResourceManager::Resource r) const
+inline bool Solver::withinBudget(Resource r) const
 {
   Assert(d_proxy);
   // spendResource sets async_interrupt or throws UnsafeInterruptException
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 9da0e2f89..534587bf7 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -485,7 +485,7 @@ protected:
     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
 public:
     bool     withinBudget     (uint64_t amount)      const;
-    bool withinBudget(ResourceManager::Resource r) const;
+    bool withinBudget(Resource r) const;
 
    protected:
     // Static helpers:
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 866110e5d..4af943537 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -534,7 +534,7 @@ void PropEngine::interrupt()
   Debug("prop") << "interrupt()" << std::endl;
 }
 
-void PropEngine::spendResource(ResourceManager::Resource r)
+void PropEngine::spendResource(Resource r)
 {
   d_resourceManager->spendResource(r);
 }
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 2beb633ee..ee2be0ca2 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -252,7 +252,7 @@ class PropEngine
    * Informs the ResourceManager that a resource has been spent.  If out of
    * resources, can throw an UnsafeInterruptException exception.
    */
-  void spendResource(ResourceManager::Resource r);
+  void spendResource(Resource r);
 
   /**
    * For debugging.  Return true if "expl" is a well-formed
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index dffd36fd5..bf386fc0e 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -162,11 +162,11 @@ TNode TheoryProxy::getNode(SatLiteral lit) {
 }
 
 void TheoryProxy::notifyRestart() {
-  d_propEngine->spendResource(ResourceManager::Resource::RestartStep);
+  d_propEngine->spendResource(Resource::RestartStep);
   d_theoryEngine->notifyRestart();
 }
 
-void TheoryProxy::spendResource(ResourceManager::Resource r)
+void TheoryProxy::spendResource(Resource r)
 {
   d_theoryEngine->spendResource(r);
 }
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index e468930e7..31f095749 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -88,7 +88,7 @@ class TheoryProxy : public Registrar
 
   void notifyRestart();
 
-  void spendResource(ResourceManager::Resource r);
+  void spendResource(Resource r);
 
   bool isDecisionEngineDone();
 
diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp
index 0c5cf6ad5..c5080db81 100644
--- a/src/smt/expand_definitions.cpp
+++ b/src/smt/expand_definitions.cpp
@@ -67,7 +67,7 @@ TrustNode ExpandDefs::expandDefinitions(
 
   do
   {
-    d_resourceManager.spendResource(ResourceManager::Resource::PreprocessStep);
+    d_resourceManager.spendResource(Resource::PreprocessStep);
 
     // n is the input / original
     // node is the output / result
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 2c97d9413..1aa46c73c 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -94,7 +94,7 @@ void ProcessAssertions::finishInit(PreprocessingPassContext* pc)
 
 void ProcessAssertions::cleanup() { d_passes.clear(); }
 
-void ProcessAssertions::spendResource(ResourceManager::Resource r)
+void ProcessAssertions::spendResource(Resource r)
 {
   d_resourceManager.spendResource(r);
 }
@@ -359,7 +359,7 @@ bool ProcessAssertions::apply(Assertions& as)
 // returns false if simplification led to "false"
 bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions)
 {
-  spendResource(ResourceManager::Resource::PreprocessStep);
+  spendResource(Resource::PreprocessStep);
   try
   {
     ScopeCounter depth(d_simplifyAssertionsDepth);
diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h
index 5931899d9..1cd00dfab 100644
--- a/src/smt/process_assertions.h
+++ b/src/smt/process_assertions.h
@@ -107,7 +107,7 @@ class ProcessAssertions
    */
   unsigned d_simplifyAssertionsDepth;
   /** Spend resource r by the resource manager of this class. */
-  void spendResource(ResourceManager::Resource r);
+  void spendResource(Resource r);
   /**
    * Perform non-clausal simplification of a Node.  This involves
    * Theory implementations, but does NOT involve the SAT solver in
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3a67b7bf3..5f85445ff 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1148,7 +1148,7 @@ Node SmtEngine::simplify(const Node& ex)
 Node SmtEngine::expandDefinitions(const Node& ex, bool expandOnly)
 {
   getResourceManager()->spendResource(
-      ResourceManager::Resource::PreprocessStep);
+      Resource::PreprocessStep);
 
   SmtScope smts(this);
   finishInit();
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index fbb679cf7..ceec0619b 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -221,7 +221,7 @@ Result SmtSolver::checkSatisfiability(Assertions& as,
 void SmtSolver::processAssertions(Assertions& as)
 {
   TimerStat::CodeTimer paTimer(d_stats.d_processAssertionsTime);
-  d_rm->spendResource(ResourceManager::Resource::PreprocessStep);
+  d_rm->spendResource(Resource::PreprocessStep);
   Assert(d_state.isFullyReady());
 
   preprocessing::AssertionPipeline& ap = as.getAssertionPipeline();
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.
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
diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h
index 3c19a8c03..1aed7ce3f 100644
--- a/test/unit/test_smt.h
+++ b/test/unit/test_smt.h
@@ -112,7 +112,7 @@ class DummyOutputChannel : public cvc5::theory::OutputChannel
   DummyOutputChannel() {}
   ~DummyOutputChannel() override {}
 
-  void safePoint(ResourceManager::Resource r) override {}
+  void safePoint(Resource r) override {}
   void conflict(TNode n) override { push(CONFLICT, n); }
 
   void trustedConflict(theory::TrustNode n) override