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.

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index a5ffe2c43c7b0b17e2af4c8366807211ddff7692..12e14850064af3aa0c12990800815415bfc10699 100644 (file)
--- 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 b93186767b80dd44c6e32464783ed07b8a516c49..4fe93c1295de5727f6df8fc7d64d6aa13b7d1b5b 100644 (file)
--- 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 8abebc25353d3b2300cdd93510f0e0769e2108f4..0bbc31b778617bdaa88b16c63c12318d318441aa 100644 (file)
--- 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 2df4de4bc7063f48937558fd0b94942939068d38..28b8073b97d5e764c4865f05d50f1cc080dee06d 100644 (file)
--- 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 3e5da9ca1cca8c992b247f0f5f1f6f54be600749..680f2093c4b526197245c7eae00071a6f3564257 100644 (file)
--- 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 f617076d56cf9cb5079676c5ba101683d2ca66eb..3d9c2b669bca350f6d3258f14d2eaa79ee91f909 100644 (file)
--- 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 2d678ec2b212456df2dab15d204725897d26bab7..c8a1a8fb4bf0ea7687cf6c5b732b4786846cd768 100644 (file)
--- 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 324cd89b95f3981026c5af732bfa228a049857cf..20c17331654d4c9ccbfa54a1384d7a9e66de7e59 100644 (file)
--- 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 dfa0c378d97407e4d1e145a465cf8f0b4281e9a3..7fd54420f1d5ff687d346a77a09d9c54b9ce0888 100644 (file)
--- 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 c30017f31a2600fce7a5b98970d181e12179436e..71719e064df886d9b4a0e0022711e86c33c47406 100644 (file)
--- 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 278192c9797dccc8097c101d4b8024652974db38..068e47f1339235aaed09a4bbec1b3c58e0dc4cfd 100644 (file)
--- 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 efa50e0a0267543e2b9744a1fad2368633ff589d..f79c7fec999a65e21d1c29cfb2f824fd70ef28d3 100644 (file)
--- 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 e2b8c0276623a4f88d50332137efe9c5af52f6bd..c9f20d7748f5b921fbce600255df3823b2bfe8fc 100644 (file)
--- 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 278252da98a7a95a34571dca55fcd67f39e73e45..09d24d90008f2d8a276e73f76562e8989f358b27 100644 (file)
--- 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 88cc8112d2ef728a505f4be0e92b73b01c671e7d..cc882022650f4fa3b90277f418cab015fbe910bb 100644 (file)
--- 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 922c3bdd5ecbd328f42af2db6bc7e615bdf8d76b..15b3c62df0792b0b4cc89e62fe2be8290f6194ef 100644 (file)
--- 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 902db959f55fcdbcc352adf5b455ebb71143cd0f..b7d0d37f42b5f901531f548cbd96c90169a4c4f6 100644 (file)
--- 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 45fbf1699fe1cb4bb2db532da861ccbfde3955ab..9c1051754a4479210269ccf1c32b90caae841f6a 100644 (file)
--- 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 e7dc3ef0c2028b240c22b1e35d7f45f6c42a131a..5dfc3f9f4d691146b06acee146f8264381ef21fb 100644 (file)
--- 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 d154b5e7f9cb0bac68e8475441136f61a7060589..e517b8f74a8b66ce43d152e3cdaad8df323919f7 100644 (file)
--- 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 3bd43f889c351f6056128bbed8079ad66b81675d..3826eb9f96320d0445ee9af09608633d6767edd4 100644 (file)
--- 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 8603d5ca35f2d6ae464b20a563b3a86af86cd174..0fb4a59b5dd40fea057dc8603c14964c5b4cd4a8 100644 (file)
--- 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 cd3ae5edffc45aebbe6c06709e5e969b2165c1bb..7a7809eefdfb6bd8d6a22344c5721cc7bb46923a 100644 (file)
--- 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 9da0e2f8951a7c888bbc2a72de8fb77bb9e424e8..534587bf721a069c3a1778500eec4a59e66a3141 100644 (file)
--- 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 866110e5d184070ffdf605198210124564c27e02..4af9435371bc01e3b10059bb5ec902e07fea8cde 100644 (file)
--- 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 2beb633eeece5d6391a50c5d3eb172e52a11e911..ee2be0ca2576a95f40bf8f7faa322c9f966a139c 100644 (file)
--- 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 dffd36fd5157d1356f73a7239724b0033567cce2..bf386fc0eb8aa1c7a803fd142dde11c83f5f5b9f 100644 (file)
--- 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 e468930e74439b489283748409d1c0152bf0ff1a..31f095749a64dcb9c7e14d69f2cb01682a1bc771 100644 (file)
--- 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 0c5cf6ad5e58e2a5d5617350f1ccab70d6f2386d..c5080db81dc9c4de4bb371f8be47b621471f63e6 100644 (file)
--- 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 2c97d94136e77c4c77519889cf66618147013bc8..1aa46c73caf61bdfb981d513f3dc386a8df65d49 100644 (file)
--- 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 5931899d96029d198c861794024b3b42d67e6c78..1cd00dfabc641e48e757ca30e5c42b4c29c0e775 100644 (file)
--- 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 3a67b7bf3da622a649679dd1f07f282c4ec73415..5f85445ff48ad78301220446c33248b9075342b6 100644 (file)
--- 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 fbb679cf72db2c4d9229ae6bce9ec1b70f07b335..ceec0619bc6ef39bf484798c31898f81e04a990b 100644 (file)
--- 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 c9ac5f367d88a912bca118dd3d26504c96202fa8..9a13944f3bf7345ab3f3c7bfd7a198f97b21a944 100644 (file)
--- 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 38a8a854016d5df50808a10e619d694e99f4ea27..24a833fcc309214bf4dfa802b718e132466f019c 100644 (file)
--- 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 04e4a3c5007b17661dcc59fda0c018d018beae2d..ed02746ed7b3932225fcbe3d255cc734c69f6b00 100644 (file)
--- 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 0131b7a95f8fdf692d7eb58b800cfa057953b059..3a2bb64324db1703fd223178d873e795ad2b3708 100644 (file)
--- 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 6af9be7aada5f181b3ae9b1d1a43fa28021287aa..52230c3b5dfeb49963c3ac6db87bdae6b391e372 100644 (file)
--- 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 8653cd7b5bad30737428adfaeaf805ba95b3505c..2d0ae1931b638cd7af5c3702169e0dd698ea825a 100644 (file)
--- 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 ba114fa2b27f7309f135133b17fe4d65d6ec4b4a..a36c4d4fb35b249b0750d251bb1c565cab1c6b29 100644 (file)
--- 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 db1d6c8a36c5d5b25856d67625c59ea601eade25..9129b1c69a04c85b487195a7685dc8f121eeb040 100644 (file)
--- 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 890ec2cc6d9c3fda83794717ebd0b541ad56dd4e..70c9d9de68d1649a99ba7e25d08347e3b495206f 100644 (file)
--- 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 61301e93cb8ff798b4da2f29b7ab2e939b50e40f..0a391f474e9598a4ef4c00ebc4694535ccd599ee 100644 (file)
--- 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 3864defc7a82989863e4913fc1d4610d822d31dc..3613584fe95fc1508a3e416bbd9e128d51a12bf1 100644 (file)
--- 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 dd68cb8e5bd062cfd082a1bf8edf3aeda9ff8ef2..d5ce5ab795bbd50b6b4d59c1a8cab2797375a03a 100644 (file)
--- 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 00f2f2acb5512134ebe1b1dfb0ecfdbbee4556b2..493edd5127bb1e291a132bd129bf24ab3b4397d7 100644 (file)
--- 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 a3a656cec6f27a4a3cc30262daa38f13439f0d03..61548435845b692375b1db03c7137c911a843ee1 100644 (file)
--- 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 b193b94b4bcc780ad8eebb05d56cb809327ae8c3..b45380f5e9b99885e23b30e5aaa50a0f953e44f1 100644 (file)
--- 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 2916088aa8dca5badf9a2834c56d695a6bd8b061..5cea6592c62aaf4a8c03bafb52535ee4f9d28f98 100644 (file)
--- 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 4e922410f493bafbadf507d2c6d4aed45717d4ee..78a83c4da3dfa0b3b714373ef3b3af8bc5ebc2f8 100644 (file)
--- 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 8b11b31989d2aed15881ab4ea4e166df79ba380c..8c030351b639f983094bc0a75ba0e9264ab752e6 100644 (file)
--- 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 dd3ca4f993d2d80b3cb197ceaf534137e59df58e..4da9a38dd91d48cc90947e3596f9fbaffbe3816a 100644 (file)
--- 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 467ed0a287832c1038eb4be70535572a6da0ae2f..e52321c4926c8cb77034280951787e4220bc71ad 100644 (file)
--- 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 c2d5ce52bd2a4d173cca5bb1e652f5b8c19df8fe..c9d198e2ca839dc4300eb103b4b4ad41af7a0b8b 100644 (file)
--- 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 56d760384686aaba1d91cecaa720bb22d659e4b3..d0074c4447d574bb826c3d8076322d580ca3ea1e 100644 (file)
--- 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 526e9f5f3e0e24525e85c62f00d8098ebddf40f3..1d5dd7d42358856653832b0fdd652ff4f7b35aba 100644 (file)
--- 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 3c19a8c03ff0b50cf58a7259c68f8ad9cd83dadc..1aed7ce3f5493029107a78907e24ef31fa1e5e9a 100644 (file)
--- 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