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.

3 files changed, 10 insertions, 10 deletions

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:
     //