resource manager: Add statistic for every resource. (#3772)

This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`).

Fixes #3751.

diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt
index 7c2985e5cd682b11c50ac0be069fe6c8266428ca..589890ead45b1e0dbe1a68191d891b4ef6f10fd6 100644 (file)
--- a/src/bindings/java/CMakeLists.txt
+++ b/src/bindings/java/CMakeLists.txt
@@ -174,7 +174,6 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/RegExpType.java
   ${CMAKE_CURRENT_BINARY_DIR}/ResetAssertionsCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/ResetCommand.java
-  ${CMAKE_CURRENT_BINARY_DIR}/ResourceManager.java
   ${CMAKE_CURRENT_BINARY_DIR}/Result.java
   ${CMAKE_CURRENT_BINARY_DIR}/RoundingMode.java
   ${CMAKE_CURRENT_BINARY_DIR}/RoundingModeType.java
@@ -226,7 +225,6 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/SynthFunCommand.java
   ${CMAKE_CURRENT_BINARY_DIR}/TesterType.java
   ${CMAKE_CURRENT_BINARY_DIR}/TheoryId.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Timer.java
   ${CMAKE_CURRENT_BINARY_DIR}/TupleUpdate.java
   ${CMAKE_CURRENT_BINARY_DIR}/TupleUpdateHashFunction.java
   ${CMAKE_CURRENT_BINARY_DIR}/Type.java

diff --git a/src/cvc4.i b/src/cvc4.i
index bed988b322b456bc8a71e37f49ea8f789f49b2bc..6ed620960a786201a2740f51bc5fc4a9df01df7c 100644 (file)
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -321,7 +321,6 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %include "util/hash.i"
 %include "util/proof.i"
 %include "util/regexp.i"
-%include "util/resource_manager.i"
 %include "util/result.i"
 %include "util/sexpr.i"
 %include "util/statistics.i"

diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 41d439d4f65958993952db6844bc6bb09cc39b63..5ebcda8fe2346096dedeb3320be8d43a1b6f9a62 100644 (file)
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -117,7 +117,8 @@ public:
 
   /** Gets the next decision based on strategies that are enabled */
   SatLiteral getNext(bool &stopSearch) {
-    NodeManager::currentResourceManager()->spendResource(options::decisionStep());
+    NodeManager::currentResourceManager()->spendResource(
+        ResourceManager::Resource::DecisionStep);
     Assert(d_cnfStream != NULL)
         << "Forgot to set cnfStream for decision engine?";
     Assert(d_satSolver != NULL)

diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 7cc63525922e79584c04f7a4ac6d3f3cce808eb5..dbfd01242e254c2a0dfd12d5d71582575ef25303 100644 (file)
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -37,6 +37,7 @@
 #endif /* SWIGOCAML */
 
 %ignore CVC4::stats::getStatisticsRegistry(ExprManager*);
+%ignore CVC4::ExprManager::getResourceManager();
 
 %include "expr/expr_manager.h"
 

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 39be675ec678c8112d962e276d817b734d14ecc0..367162420cfaa7b73aa6781ea2a0e0c288593242 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -91,34 +91,34 @@ namespace attr {
 // attribute that stores the canonical bound variable list for function types
 typedef expr::Attribute<attr::LambdaBoundVarListTag, Node> LambdaBoundVarListAttr;
 
-NodeManager::NodeManager(ExprManager* exprManager) :
-  d_options(new Options()),
-  d_statisticsRegistry(new StatisticsRegistry()),
-  d_resourceManager(new ResourceManager()),
-  d_registrations(new ListenerRegistrationList()),
-  next_id(0),
-  d_attrManager(new expr::attr::AttributeManager()),
-  d_exprManager(exprManager),
-  d_nodeUnderDeletion(NULL),
-  d_inReclaimZombies(false),
-  d_abstractValueCount(0),
-  d_skolemCounter(0) {
+NodeManager::NodeManager(ExprManager* exprManager)
+    : d_options(new Options()),
+      d_statisticsRegistry(new StatisticsRegistry()),
+      d_resourceManager(new ResourceManager(*d_statisticsRegistry, *d_options)),
+      d_registrations(new ListenerRegistrationList()),
+      next_id(0),
+      d_attrManager(new expr::attr::AttributeManager()),
+      d_exprManager(exprManager),
+      d_nodeUnderDeletion(NULL),
+      d_inReclaimZombies(false),
+      d_abstractValueCount(0),
+      d_skolemCounter(0)
+{
   init();
 }
 
-NodeManager::NodeManager(ExprManager* exprManager,
-                         const Options& options) :
-  d_options(new Options()),
-  d_statisticsRegistry(new StatisticsRegistry()),
-  d_resourceManager(new ResourceManager()),
-  d_registrations(new ListenerRegistrationList()),
-  next_id(0),
-  d_attrManager(new expr::attr::AttributeManager()),
-  d_exprManager(exprManager),
-  d_nodeUnderDeletion(NULL),
-  d_inReclaimZombies(false),
-  d_abstractValueCount(0),
-  d_skolemCounter(0)
+NodeManager::NodeManager(ExprManager* exprManager, const Options& options)
+    : d_options(new Options()),
+      d_statisticsRegistry(new StatisticsRegistry()),
+      d_resourceManager(new ResourceManager(*d_statisticsRegistry, *d_options)),
+      d_registrations(new ListenerRegistrationList()),
+      next_id(0),
+      d_attrManager(new expr::attr::AttributeManager()),
+      d_exprManager(exprManager),
+      d_nodeUnderDeletion(NULL),
+      d_inReclaimZombies(false),
+      d_abstractValueCount(0),
+      d_skolemCounter(0)
 {
   d_options->copyValues(options);
   init();
@@ -228,12 +228,12 @@ NodeManager::~NodeManager() {
   }
 
   // defensive coding, in case destruction-order issues pop up (they often do)
+  delete d_resourceManager;
+  d_resourceManager = NULL;
   delete d_statisticsRegistry;
   d_statisticsRegistry = NULL;
   delete d_registrations;
   d_registrations = NULL;
-  delete d_resourceManager;
-  d_resourceManager = NULL;
   delete d_attrManager;
   d_attrManager = NULL;
   delete d_options;

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index cd8a530fc8e7a1561ea688486f42f5385bcbed0f..f78dbb3b89c34f1a15ba99a37de86eda9b53127a 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -535,6 +535,24 @@ header = "options/smt_options.h"
   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"

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 681b2a1c9e3f7e8d573dc01783dd306adae790ae..32d55571858d5ccbcf1a27f9b285d2094872bdd3 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -640,8 +640,7 @@ Command* Parser::nextCommand()
       dynamic_cast<QuitCommand*>(cmd) == NULL) {
     // don't count set-option commands as to not get stuck in an infinite
     // loop of resourcing out
-    const Options& options = getExprManager()->getOptions();
-    d_resourceManager->spendResource(options.getParseStep());
+    d_resourceManager->spendResource(ResourceManager::Resource::ParseStep);
   }
   return cmd;
 }
@@ -649,8 +648,7 @@ Command* Parser::nextCommand()
 Expr Parser::nextExpression()
 {
   Debug("parser") << "nextExpression()" << std::endl;
-  const Options& options = getExprManager()->getOptions();
-  d_resourceManager->spendResource(options.getParseStep());
+  d_resourceManager->spendResource(ResourceManager::Resource::ParseStep);
   Expr result;
   if (!done()) {
     try {

diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index 791bb2dc705ce2c372a5ea25219e70bb7f95f544..98313efda53d745e92691bd245462935f0537178 100644 (file)
--- a/src/preprocessing/passes/apply_substs.cpp
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -52,7 +52,8 @@ PreprocessingPassResult ApplySubsts::applyInternal(
       }
       Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i]
                         << std::endl;
-      d_preprocContext->spendResource(options::preprocessStep());
+      d_preprocContext->spendResource(
+          ResourceManager::Resource::PreprocessStep);
       assertionsToPreprocess->replace(i,
                                       theory::Rewriter::rewrite(substMap.apply(
                                           (*assertionsToPreprocess)[i])));

diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
index 7787d763173e2c3521c5c6653e1f6b21ed39713f..30b64fd741f559acfd249a94531e965453599970 100644 (file)
--- a/src/preprocessing/passes/bool_to_bv.cpp
+++ b/src/preprocessing/passes/bool_to_bv.cpp
@@ -36,7 +36,7 @@ PreprocessingPassResult BoolToBV::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
   NodeManager::currentResourceManager()->spendResource(
-      options::preprocessStep());
+      ResourceManager::Resource::PreprocessStep);
 
   unsigned size = assertionsToPreprocess->size();
   for (unsigned i = 0; i < size; ++i)

diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp
index 3d3762ecd78467be82e9e07a9f661dc81c69a938..0637c541f84bfd6908712e1d79b7918a2ac75639 100644 (file)
--- a/src/preprocessing/passes/bv_to_bool.cpp
+++ b/src/preprocessing/passes/bv_to_bool.cpp
@@ -45,7 +45,7 @@ PreprocessingPassResult BVToBool::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
   NodeManager::currentResourceManager()->spendResource(
-      options::preprocessStep());
+      ResourceManager::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 bda38a6df50187b3217cc23868a8bcbe6868ce18..6ad97f4a3a69a44a8a0047a3f256822c337811fb 100644 (file)
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -32,7 +32,7 @@ IteRemoval::IteRemoval(PreprocessingPassContext* preprocContext)
 
 PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
 {
-  d_preprocContext->spendResource(options::preprocessStep());
+  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
 
   // Remove all of the ITE occurrences and normalize
   d_preprocContext->getIteRemover()->run(

diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index ad00ec204698ff856b88c4f406883fb9d0b26334..7f7c4c95fe24c701ff86fd17ae894229e608f6ad 100644 (file)
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -234,12 +234,12 @@ ITESimp::ITESimp(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult ITESimp::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  d_preprocContext->spendResource(options::preprocessStep());
+  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
 
   size_t nasserts = assertionsToPreprocess->size();
   for (size_t i = 0; i < nasserts; ++i)
   {
-    d_preprocContext->spendResource(options::preprocessStep());
+    d_preprocContext->spendResource(ResourceManager::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 139bf96a9dfa284bcb6360cfb0c9f2ef1afbc8a6..03f38370bb05635ba329a2bf6b1fb8a22622431a 100644 (file)
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -56,7 +56,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
 {
   Assert(!options::unsatCores() && !options::fewerPreprocessingHoles());
 
-  d_preprocContext->spendResource(options::preprocessStep());
+  d_preprocContext->spendResource(ResourceManager::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 7af9f7fac12dff1a8b0b8cc5ce76081157edd7bd..ec3982e03783ea59cdc630970485faaa42cd0251 100644 (file)
--- a/src/preprocessing/passes/static_learning.cpp
+++ b/src/preprocessing/passes/static_learning.cpp
@@ -30,7 +30,7 @@ PreprocessingPassResult StaticLearning::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
   NodeManager::currentResourceManager()->spendResource(
-      options::preprocessStep());
+      ResourceManager::Resource::PreprocessStep);
 
   for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
   {

diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 1695ae2ffadd49bdc8cad3e80be02ec5bc0afd46..8a2c58b99581d560282f2a41bda51e74a709bbd3 100644 (file)
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -813,7 +813,7 @@ void UnconstrainedSimplifier::processUnconstrained()
 PreprocessingPassResult UnconstrainedSimplifier::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  d_preprocContext->spendResource(options::preprocessStep());
+  d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
 
   std::vector<Node>& assertions = assertionsToPreprocess->ref();
 

diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index 37744151c6c33d86aa44b87bf03bace3a9b6a80b..70b1f70c24b4aaaba705cd17ce94be543fb327f9 100644 (file)
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -61,9 +61,9 @@ class PreprocessingPassContext
     return d_symsInAssertions;
   }
 
-  void spendResource(unsigned amount)
+  void spendResource(ResourceManager::Resource r)
   {
-    d_resourceManager->spendResource(amount);
+    d_resourceManager->spendResource(r);
   }
 
   const LogicInfo& getLogicInfo() { return d_smt->d_logic; }

diff --git a/src/prop/bv_sat_solver_notify.h b/src/prop/bv_sat_solver_notify.h
index 77163cfe607d3166dd0eea55c37a6de61ed02007..eca6bdfd65dbbf766e5fa9a8fec7bb2629029abe 100644 (file)
--- a/src/prop/bv_sat_solver_notify.h
+++ b/src/prop/bv_sat_solver_notify.h
@@ -19,6 +19,7 @@
 #define CVC4__PROP__BVSATSOLVERNOTIFY_H
 
 #include "prop/sat_solver_types.h"
+#include "util/resource_manager.h"
 
 namespace CVC4 {
 namespace prop {
@@ -38,8 +39,8 @@ public:
    * Notify about a learnt clause.
    */
   virtual void notify(SatClause& clause) = 0;
-  virtual void spendResource(unsigned amount) = 0;
-  virtual void safePoint(unsigned amount) = 0;
+  virtual void spendResource(ResourceManager::Resource r) = 0;
+  virtual void safePoint(ResourceManager::Resource r) = 0;
 
 };/* class BVSatSolverInterface::Notify */
 

diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 70e0b91573be1d5c1461181676d5eae514b7d55f..f71dac3e5ee80907cc95ef3c5255bb1818e69630 100644 (file)
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -23,9 +23,10 @@
 #include "context/cdo.h"
 #include "proof/clause_id.h"
 #include "proof/resolution_bitvector_proof.h"
+#include "prop/bv_sat_solver_notify.h"
 #include "prop/bvminisat/simp/SimpSolver.h"
 #include "prop/sat_solver.h"
-#include "prop/bv_sat_solver_notify.h"
+#include "util/resource_manager.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -46,11 +47,14 @@ class BVMinisatSatSolver : public BVSatSolverInterface,
       return d_notify->notify(toSatLiteral(lit));
     }
     void notify(BVMinisat::vec<BVMinisat::Lit>& clause) override;
-    void spendResource(unsigned amount) override
+    void spendResource(ResourceManager::Resource r) override
+    {
+      d_notify->spendResource(r);
+    }
+    void safePoint(ResourceManager::Resource r) override
     {
-      d_notify->spendResource(amount);
+      d_notify->safePoint(r);
     }
-    void safePoint(unsigned amount) override { d_notify->safePoint(amount); }
   };
 
        std::unique_ptr<BVMinisat::SimpSolver> d_minisat;

diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 04658fc38d5dfbeb52b5579ea9ec4f78b11ca604..25b6a3da2676ea13a8d1b29928ffacb042df40ed 100644 (file)
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -1076,7 +1076,8 @@ lbool Solver::search(int nof_conflicts, UIP uip)
             // NO CONFLICT
             bool isWithinBudget;
             try {
-              isWithinBudget = withinBudget(CVC4::options::bvSatConflictStep()); 
+              isWithinBudget =
+                  withinBudget(ResourceManager::Resource::BvSatConflictsStep);
             }
             catch (const CVC4::theory::Interrupted& e) {
               // do some clean-up and rethrow 
@@ -1232,7 +1233,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(CVC4::options::bvSatConflictStep())) break;
+        if (!withinBudget(ResourceManager::Resource::BvSatConflictsStep)) break;
         curr_restarts++;
     }
 
@@ -1482,11 +1483,10 @@ void ClauseAllocator::reloc(CRef& cr,
 }
 
 void Solver::setNotify(Notify* toNotify) { d_notify = toNotify; }
-bool Solver::withinBudget(uint64_t amount) const
+bool Solver::withinBudget(ResourceManager::Resource r) const
 {
   AlwaysAssert(d_notify);
-  d_notify->spendResource(amount);
-  d_notify->safePoint(0);
+  d_notify->safePoint(r);
 
   return !asynch_interrupt &&
          (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) &&

diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index eef1c4e4cceea4a2cf3a1a866a57a6650b8b7b35..2197d030fcadb5e9bf16b72a6248e11cd197ca72 100644 (file)
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -31,7 +31,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/bvminisat/mtl/Heap.h"
 #include "prop/bvminisat/mtl/Vec.h"
 #include "prop/bvminisat/utils/Options.h"
-
+#include "util/resource_manager.h"
 
 namespace CVC4 {
 
@@ -64,8 +64,8 @@ public:
    */
   virtual void notify(vec<Lit>& learnt) = 0;
 
-  virtual void spendResource(unsigned amount) = 0;
-  virtual void safePoint(unsigned amount) = 0;
+  virtual void spendResource(ResourceManager::Resource r) = 0;
+  virtual void safePoint(ResourceManager::Resource r) = 0;
 };
 
 //=================================================================================================
@@ -347,7 +347,7 @@ public:
     CRef     reason           (Var x) const;
     int      level            (Var x) const;
     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
-    bool     withinBudget     (uint64_t amount)      const;
+    bool withinBudget(ResourceManager::Resource r) const;
 
     // Static helpers:
     //

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 6d60bfafc7a0d6cb9e3c591cb508ddb6d623f17e..6690f12dbae34c4bfad4a1e008be966c78f99313 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -711,7 +711,8 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
                << ", negated = " << (negated ? "true" : "false") << ")" << endl;
 
   if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) {
-    NodeManager::currentResourceManager()->spendResource(options::cnfStep());
+    NodeManager::currentResourceManager()->spendResource(
+        ResourceManager::Resource::CnfStep);
     d_convertAndAssertCounter = 0;
   }
   ++d_convertAndAssertCounter;

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 6126983fa3f41a2f11197e2a251939d2c56501d6..83f6fb897f8bbd9bd9c9b1aa9252d1cc6009ed45 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1419,7 +1419,7 @@ lbool Solver::search(int nof_conflicts)
             }
 
             if ((nof_conflicts >= 0 && conflictC >= nof_conflicts)
-                || !withinBudget(options::satConflictStep()))
+                || !withinBudget(ResourceManager::Resource::SatConflictStep))
             {
               // Reached bound on number of conflicts:
               progress_estimate = progressEstimate();
@@ -1558,12 +1558,13 @@ 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(options::satConflictStep())) break; // FIXME add restart option?
+        if (!withinBudget(ResourceManager::Resource::SatConflictStep))
+          break;  // FIXME add restart option?
         curr_restarts++;
     }
 
-    if(!withinBudget(options::satConflictStep()))
-        status = l_Undef;
+    if (!withinBudget(ResourceManager::Resource::SatConflictStep))
+      status = l_Undef;
 
     if (verbosity >= 1)
         printf("===============================================================================\n");
@@ -1778,7 +1779,7 @@ CRef Solver::updateLemmas() {
   Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl;
 
   // Avoid adding lemmas indefinitely without resource-out
-  proxy->spendResource(options::lemmaStep());
+  proxy->spendResource(ResourceManager::Resource::LemmaStep);
 
   CRef conflict = CRef_Undef;
 
@@ -1948,19 +1949,20 @@ void ClauseAllocator::reloc(CRef& cr,
   else if (to[cr].has_extra()) to[cr].calcAbstraction();
 }
 
-inline bool Solver::withinBudget(uint64_t amount) const
+inline bool Solver::withinBudget(ResourceManager::Resource r) const
 {
   Assert(proxy);
   // spendResource sets async_interrupt or throws UnsafeInterruptException
   // depending on whether hard-limit is enabled
-  proxy->spendResource(amount);
+  proxy->spendResource(r);
 
-  bool within_budget =  !asynch_interrupt &&
-    (conflict_budget    < 0 || conflicts < (uint64_t)conflict_budget) &&
-    (propagation_budget < 0 || propagations < (uint64_t)propagation_budget);
+  bool within_budget =
+      !asynch_interrupt
+      && (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget)
+      && (propagation_budget < 0
+          || propagations < (uint64_t)propagation_budget);
   return within_budget;
 }
 
-
 } /* CVC4::Minisat namespace */
 } /* CVC4 namespace */

diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index aa3b96c57edc04c0083e94e25df0fc10de197f12..0cec30d24d933d0d808259863ac3bd11b3805276 100644 (file)
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -440,8 +440,9 @@ protected:
     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
 public:
     bool     withinBudget     (uint64_t amount)      const;
-protected:
+    bool withinBudget(ResourceManager::Resource r) const;
 
+   protected:
     // Static helpers:
     //
 

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 8a0cc9f15ae0860db322d41028a55695f27031e3..bac584236e923eeb6ac09e78e4819cbf079798ef 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -295,9 +295,9 @@ void PropEngine::interrupt()
   Debug("prop") << "interrupt()" << endl;
 }
 
-void PropEngine::spendResource(unsigned amount)
+void PropEngine::spendResource(ResourceManager::Resource r)
 {
-  d_resourceManager->spendResource(amount);
+  d_resourceManager->spendResource(r);
 }
 
 bool PropEngine::properExplanation(TNode node, TNode expl) const {

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index aaa65b85afa934220b1f840b71379a1b5969e105..efbd829475d5a35c03aa2da15565b461ee00cffe 100644 (file)
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -29,6 +29,7 @@
 #include "options/options.h"
 #include "proof/proof_manager.h"
 #include "smt_util/lemma_channels.h"
+#include "util/resource_manager.h"
 #include "util/result.h"
 #include "util/unsafe_interrupt_exception.h"
 
@@ -228,7 +229,7 @@ public:
    * Informs the ResourceManager that a resource has been spent.  If out of
    * resources, can throw an UnsafeInterruptException exception.
    */
-  void spendResource(unsigned amount);
+  void spendResource(ResourceManager::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 1258d2ee2b73fe2a69f5924bba2078dffc2b8e5f..cf7c9f0d9e2a24cb3da9a79edcd5ed34b276fd1d 100644 (file)
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -161,7 +161,7 @@ TNode TheoryProxy::getNode(SatLiteral lit) {
 }
 
 void TheoryProxy::notifyRestart() {
-  d_propEngine->spendResource(options::restartStep());
+  d_propEngine->spendResource(ResourceManager::Resource::RestartStep);
   d_theoryEngine->notifyRestart();
 
   static uint32_t lemmaCount = 0;
@@ -238,9 +238,9 @@ void TheoryProxy::logDecision(SatLiteral lit) {
 #endif /* CVC4_REPLAY */
 }
 
-void TheoryProxy::spendResource(unsigned amount)
+void TheoryProxy::spendResource(ResourceManager::Resource r)
 {
-  d_theoryEngine->spendResource(amount);
+  d_theoryEngine->spendResource(r);
 }
 
 bool TheoryProxy::isDecisionRelevant(SatVariable var) {

diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 3bb15aa4e87dea07448482fe4476a886e210bed1..61c556f3408d8c9383714100300deeeed68b76f9 100644 (file)
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -34,6 +34,7 @@
 #include "smt_util/lemma_input_channel.h"
 #include "smt_util/lemma_output_channel.h"
 #include "theory/theory.h"
+#include "util/resource_manager.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -92,7 +93,7 @@ public:
 
   void logDecision(SatLiteral lit);
 
-  void spendResource(unsigned amount);
+  void spendResource(ResourceManager::Resource r);
 
   bool isDecisionEngineDone();
 

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f1d602bc672534e20d85ae6901926e4809867852..2dc20cc3192524b3df75562acb980aeb035a78d5 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -651,9 +651,10 @@ class SmtEnginePrivate : public NodeManagerListener {
   void cleanupPreprocessingPasses() { d_passes.clear(); }
 
   ResourceManager* getResourceManager() { return d_resourceManager; }
-  void spendResource(unsigned amount)
+
+  void spendResource(ResourceManager::Resource r)
   {
-    d_resourceManager->spendResource(amount);
+    d_resourceManager->spendResource(r);
   }
 
   void nmNotifyNewSort(TypeNode tn, uint32_t flags) override
@@ -2753,7 +2754,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
   // or upward pass).
 
   do {
-    spendResource(options::preprocessStep());
+    spendResource(ResourceManager::Resource::PreprocessStep);
 
     // n is the input / original
     // node is the output / result
@@ -2944,7 +2945,7 @@ static void dumpAssertions(const char* key,
 // returns false if simplification led to "false"
 bool SmtEnginePrivate::simplifyAssertions()
 {
-  spendResource(options::preprocessStep());
+  spendResource(ResourceManager::Resource::PreprocessStep);
   Assert(d_smt.d_pendingPops == 0);
   try {
     ScopeCounter depth(d_simplifyAssertionsDepth);
@@ -3202,7 +3203,7 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, unordered_map<N
 
 void SmtEnginePrivate::processAssertions() {
   TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime);
-  spendResource(options::preprocessStep());
+  spendResource(ResourceManager::Resource::PreprocessStep);
   Assert(d_smt.d_fullyInited);
   Assert(d_smt.d_pendingPops == 0);
   SubstitutionMap& top_level_substs =
@@ -4180,7 +4181,7 @@ Expr SmtEngine::simplify(const Expr& ex)
 
 Expr SmtEngine::expandDefinitions(const Expr& ex)
 {
-  d_private->spendResource(options::preprocessStep());
+  d_private->spendResource(ResourceManager::Resource::PreprocessStep);
 
   Assert(ex.getExprManager() == d_exprManager);
   SmtScope smts(this);

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 6943c5546574660eb76058a3d8fd819944ffbd6d..8986e68945aee3ce36ad98a7cbd26be6f66ff3d1 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -83,7 +83,7 @@ void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
 }
 
 void TheoryArith::check(Effort effortLevel){
-  getOutputChannel().spendResource(options::theoryCheckStep());
+  getOutputChannel().spendResource(ResourceManager::Resource::TheoryCheckStep);
   d_internal->check(effortLevel);
 }
 

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index f2beec0b8e2bf4702c2dc02bdc41e59b9b844627..534a019c36b09b65fb36d5b9531bdcdf1d5d7c35 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1319,7 +1319,7 @@ void TheoryArrays::check(Effort e) {
     return;
   }
 
-  getOutputChannel().spendResource(options::theoryCheckStep());
+  getOutputChannel().spendResource(ResourceManager::Resource::TheoryCheckStep);
 
   TimerStat::CodeTimer checkTimer(d_checkTime);
 

diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index df7cc4f115ddd92265c0539b339ce3c410023abe..a16a8bbbf2250d106b0b67c153ec41106bfbb5e5 100644 (file)
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -109,11 +109,12 @@ class MinisatEmptyNotify : public prop::BVSatSolverNotify
   MinisatEmptyNotify() {}
   bool notify(prop::SatLiteral lit) override { return true; }
   void notify(prop::SatClause& clause) override {}
-  void spendResource(unsigned amount) override
+  void spendResource(ResourceManager::Resource r) override
   {
-    NodeManager::currentResourceManager()->spendResource(amount);
+    NodeManager::currentResourceManager()->spendResource(r);
   }
-  void safePoint(unsigned amount) override {}
+
+  void safePoint(ResourceManager::Resource r) override {}
 };
 
 // Bitblaster implementation

diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index cd906769de04a82e2a895614be1c16df57012a24..c4e3513bfc2a31059db105f76956b63c6112fee3 100644 (file)
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -152,7 +152,7 @@ void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
     return;
   }
 
-  d_bv->spendResource(options::bitblastStep());
+  d_bv->spendResource(ResourceManager::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 2018590f7260c29561b7294cccdcfcd8cd6a5391..06afa126dacc1165226e8af025b261f38eae9f67 100644 (file)
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -234,7 +234,7 @@ void TLazyBitblaster::bbTerm(TNode node, Bits& bits) {
   }
   Assert(node.getType().isBitVector());
 
-  d_bv->spendResource(options::bitblastStep());
+  d_bv->spendResource(ResourceManager::Resource::BitblastStep);
   Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n";
   ++d_statistics.d_numTerms;
 
@@ -426,14 +426,14 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) {
   }
 }
 
-void TLazyBitblaster::MinisatNotify::spendResource(unsigned amount)
+void TLazyBitblaster::MinisatNotify::spendResource(ResourceManager::Resource r)
 {
-  d_bv->spendResource(amount);
+  d_bv->spendResource(r);
 }
 
-void TLazyBitblaster::MinisatNotify::safePoint(unsigned amount)
+void TLazyBitblaster::MinisatNotify::safePoint(ResourceManager::Resource r)
 {
-  d_bv->d_out->safePoint(amount);
+  d_bv->d_out->safePoint(r);
 }
 
 EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b)

diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index ac5cd5c7f734493bcf7890eae72640ca2800a6ee..3fe2398f107a3bec65a3980279a5dfea906b1a36 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(unsigned amount) override;
-    void safePoint(unsigned amount) override;
+    void spendResource(ResourceManager::Resource r) override;
+    void safePoint(ResourceManager::Resource r) override;
   };
 
   TheoryBV* d_bv;

diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index dd0458a70919a440f345f1c72b2551b6a6d1c7b9..d743a60231b1f8f832ee06675b044e7b4a10bc43 100644 (file)
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -70,7 +70,7 @@ bool EagerBitblastSolver::isInitialized() {
 }
 
 void EagerBitblastSolver::assertFormula(TNode formula) {
-  d_bv->spendResource(1);
+  d_bv->spendResource(ResourceManager::Resource::BvEagerAssertStep);
   Assert(isInitialized());
   Debug("bitvector-eager") << "EagerBitblastSolver::assertFormula " << formula
                            << "\n";

diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 25fe7002ea867a7649f2501b9e82994c3acacc71..b5e4b7c853930b8651dc74a939876ba69012296b 100644 (file)
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -173,7 +173,7 @@ bool BitblastSolver::check(Theory::Effort e)
   // We need to ensure we are fully propagated, so propagate now
   if (d_useSatPropagation)
   {
-    d_bv->spendResource(1);
+    d_bv->spendResource(ResourceManager::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 bf9bfa4808f60e0c6ff02d08688376e6ecf45f22..5d9c297f163321aa75a0b97a352b644a4f842a0b 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -171,7 +171,7 @@ bool CoreSolver::decomposeFact(TNode fact) {
 bool CoreSolver::check(Theory::Effort e) {
   Trace("bitvector::core") << "CoreSolver::check \n";
 
-  d_bv->spendResource(options::theoryCheckStep());
+  d_bv->spendResource(ResourceManager::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 332f96aa26ce5318fc41a77eabd1cf6a3ff70fee..8a895e9eb23cc75db175abdd857bb8e928bca0e2 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(options::theoryCheckStep());
+  d_bv->spendResource(ResourceManager::Resource::TheoryCheckStep);
 
   bool ok = true;
   while (!done() && ok) {

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 48168d7d6f6d70ad5f58db575a0c6b7e676176c8..a35176a9359fd53e4db8b0d6653683c2b2e16e46 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -122,9 +122,9 @@ void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   }
 }
 
-void TheoryBV::spendResource(unsigned amount)
+void TheoryBV::spendResource(ResourceManager::Resource r)
 {
-  getOutputChannel().spendResource(amount);
+  getOutputChannel().spendResource(r);
 }
 
 TheoryBV::Statistics::Statistics():

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 7ca98f2eaf65ef7e4142e3864bcf7934ef80a6c9..196535a1938fdb4e908e234c41a2e1ef7a1f75e9 100644 (file)
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -131,7 +131,7 @@ public:
 
   Statistics d_statistics;
 
-  void spendResource(unsigned amount);
+  void spendResource(ResourceManager::Resource r);
 
   /**
    * Return the uninterpreted function symbol corresponding to division-by-zero

diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index bcbbfa274ce8529fe90ebce2020e8d3921a231cf..dc5dfc38870b410110de0d18bc353ef1f70866c9 100644 (file)
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -82,7 +82,7 @@ class OutputChannel {
    *
    * @throws Interrupted if the theory can be safely interrupted.
    */
-  virtual void safePoint(uint64_t amount) {}
+  virtual void safePoint(ResourceManager::Resource r) {}
 
   /**
    * Indicate a theory conflict has arisen.
@@ -172,7 +172,7 @@ class OutputChannel {
    * long-running operations, they cannot rely on resource() to break
    * out of infinite or intractable computations.
    */
-  virtual void spendResource(unsigned amount) {}
+  virtual void spendResource(ResourceManager::Resource r) {}
 
   /**
    * Handle user attribute.

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index aec648037c81f465346181625c2a86f72f6ea4bd..1d1eb97516df870e580243eecffbc22f0afb71bc 100644 (file)
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -110,7 +110,7 @@ bool Instantiate::addInstantiation(
     Node q, std::vector<Node>& terms, bool mkRep, bool modEq, bool doVts)
 {
   // For resource-limiting (also does a time check).
-  d_qe->getOutputChannel().safePoint(options::quantifierStep());
+  d_qe->getOutputChannel().safePoint(ResourceManager::Resource::QuantifierStep);
   Assert(!d_qe->inConflict());
   Assert(terms.size() == q[0].getNumChildren());
   Assert(d_term_db != nullptr);

diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 7a99ed2d972ccbca5f70019d6cd79f76b6c87b5d..2a7c3ff0d3d9246560fedfa2d9244c2263c949b5 100644 (file)
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -131,7 +131,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
 
     if (hasSmtEngine &&
                d_iterationCount % ResourceManager::getFrequencyCount() == 0) {
-      rm->spendResource(options::rewriteStep());
+      rm->spendResource(ResourceManager::Resource::RewriteStep);
       d_iterationCount = 0;
     }
 

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 1392f8fabbc15278df16dd62c4948727e15f7613..b5fc1cbc90ed6917fce28b90c58c3a9f97221724 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -308,7 +308,7 @@ void TheorySep::check(Effort e) {
     return;
   }
 
-  getOutputChannel().spendResource(options::theoryCheckStep());
+  getOutputChannel().spendResource(ResourceManager::Resource::TheoryCheckStep);
 
   TimerStat::CodeTimer checkTimer(d_checkTime);
   Trace("sep-check") << "Sep::check(): " << e << endl;

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index b43e55364d03a68faa7097593afeb96f0d08a27d..9cd226ba1ab3daa7bef94719bd7921851e8ee9bc 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -2313,9 +2313,9 @@ std::pair<bool, Node> TheoryEngine::entailmentCheck(
   }
 }
 
-void TheoryEngine::spendResource(unsigned amount)
+void TheoryEngine::spendResource(ResourceManager::Resource r)
 {
-  d_resourceManager->spendResource(amount);
+  d_resourceManager->spendResource(r);
 }
 
 void TheoryEngine::enableTheoryAlternative(const std::string& name){

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 5506b0120afaadf93c5cd19f394666b8f86a7fea..0770efc7baff2ca6bb23ba119cf1b7f96660fdac 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -47,6 +47,7 @@
 #include "theory/uf/equality_engine.h"
 #include "theory/valuation.h"
 #include "util/hash.h"
+#include "util/resource_manager.h"
 #include "util/statistics_registry.h"
 #include "util/unsafe_interrupt_exception.h"
 
@@ -281,8 +282,9 @@ class TheoryEngine {
     EngineOutputChannel(TheoryEngine* engine, theory::TheoryId theory)
         : d_engine(engine), d_statistics(theory), d_theory(theory) {}
 
-    void safePoint(uint64_t amount) override {
-      spendResource(amount);
+    void safePoint(ResourceManager::Resource r) override
+    {
+      spendResource(r);
       if (d_engine->d_interrupted) {
         throw theory::Interrupted();
       }
@@ -323,8 +325,9 @@ class TheoryEngine {
       d_engine->setIncomplete(d_theory);
     }
 
-    void spendResource(unsigned amount) override {
-      d_engine->spendResource(amount);
+    void spendResource(ResourceManager::Resource r) override
+    {
+      d_engine->spendResource(r);
     }
 
     void handleUserAttribute(const char* attr, theory::Theory* t) override {
@@ -481,7 +484,7 @@ public:
   void interrupt();
 
   /** "Spend" a resource during a search or preprocessing.*/
-  void spendResource(unsigned amount);
+  void spendResource(ResourceManager::Resource r);
 
   /**
    * Adds a theory. Only one theory per TheoryId can be present, so if

diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index dbb42f2bc5350a2e353ce5ea516d5f9a1636ccab..17b47d2d38d021215e667e06d766ed295e9d08e7 100644 (file)
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -28,6 +28,7 @@
 #include "theory/interrupted.h"
 #include "theory/output_channel.h"
 #include "util/proof.h"
+#include "util/resource_manager.h"
 #include "util/unsafe_interrupt_exception.h"
 
 namespace CVC4 {
@@ -67,7 +68,7 @@ public:
   TestOutputChannel() {}
   ~TestOutputChannel() override {}
 
-  void safePoint(uint64_t amount) override {}
+  void safePoint(ResourceManager::Resource r) override {}
   void conflict(TNode n, std::unique_ptr<Proof> pf) override
   {
     push(CONFLICT, n);

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 4d13bf3f2a64582280899e55fe90c3694d61922d..e336d16303ff8ac90157310395afe0895008ca8d 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -117,7 +117,7 @@ void TheoryUF::check(Effort level) {
   if (done() && !fullEffort(level)) {
     return;
   }
-  getOutputChannel().spendResource(options::theoryCheckStep());
+  getOutputChannel().spendResource(ResourceManager::Resource::TheoryCheckStep);
   TimerStat::CodeTimer checkTimer(d_checkTime);
 
   while (!done() && !d_conflict)

diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index 8f00a23eac2af091c92b9715f0a19ae2f3636828..2667d8513395a8f7740dc17a552864f3fd45da84 100644 (file)
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -19,6 +19,7 @@
 #include "base/check.h"
 #include "base/output.h"
 #include "options/smt_options.h"
+#include "util/statistics_registry.h"
 
 using namespace std;
 
@@ -100,28 +101,110 @@ bool Timer::expired() const {
   return false;
 }
 
+/*---------------------------------------------------------------------------*/
+
+struct ResourceManager::Statistics
+{
+  IntStat d_numBitblastStep;
+  IntStat d_numBvEagerAssertStep;
+  IntStat d_numBvPropagationStep;
+  IntStat d_numBvSatConflictsStep;
+  IntStat d_numCnfStep;
+  IntStat d_numDecisionStep;
+  IntStat d_numLemmaStep;
+  IntStat d_numParseStep;
+  IntStat d_numPreprocessStep;
+  IntStat d_numQuantifierStep;
+  IntStat d_numRestartStep;
+  IntStat d_numRewriteStep;
+  IntStat d_numSatConflictStep;
+  IntStat d_numTheoryCheckStep;
+  Statistics(StatisticsRegistry& stats);
+  ~Statistics();
+
+ private:
+  StatisticsRegistry& d_statisticsRegistry;
+};
+
+ResourceManager::Statistics::Statistics(StatisticsRegistry& stats)
+    : d_numBitblastStep("resource::BitblastStep", 0),
+      d_numBvEagerAssertStep("resource::BvEagerAssertStep", 0),
+      d_numBvPropagationStep("resource::BvPropagationStep", 0),
+      d_numBvSatConflictsStep("resource::BvSatConflictsStep", 0),
+      d_numCnfStep("resource::CnfStep", 0),
+      d_numDecisionStep("resource::DecisionStep", 0),
+      d_numLemmaStep("resource::LemmaStep", 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_numBitblastStep);
+  d_statisticsRegistry.registerStat(&d_numBvEagerAssertStep);
+  d_statisticsRegistry.registerStat(&d_numBvPropagationStep);
+  d_statisticsRegistry.registerStat(&d_numBvSatConflictsStep);
+  d_statisticsRegistry.registerStat(&d_numCnfStep);
+  d_statisticsRegistry.registerStat(&d_numDecisionStep);
+  d_statisticsRegistry.registerStat(&d_numLemmaStep);
+  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);
+}
+
+ResourceManager::Statistics::~Statistics()
+{
+  d_statisticsRegistry.unregisterStat(&d_numBitblastStep);
+  d_statisticsRegistry.unregisterStat(&d_numBvEagerAssertStep);
+  d_statisticsRegistry.unregisterStat(&d_numBvPropagationStep);
+  d_statisticsRegistry.unregisterStat(&d_numBvSatConflictsStep);
+  d_statisticsRegistry.unregisterStat(&d_numCnfStep);
+  d_statisticsRegistry.unregisterStat(&d_numDecisionStep);
+  d_statisticsRegistry.unregisterStat(&d_numLemmaStep);
+  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);
+}
+
+/*---------------------------------------------------------------------------*/
+
 const uint64_t ResourceManager::s_resourceCount = 1000;
 
-ResourceManager::ResourceManager()
-  : d_cumulativeTimer()
-  , d_perCallTimer()
-  , d_timeBudgetCumulative(0)
-  , d_timeBudgetPerCall(0)
-  , d_resourceBudgetCumulative(0)
-  , d_resourceBudgetPerCall(0)
-  , d_cumulativeTimeUsed(0)
-  , d_cumulativeResourceUsed(0)
-  , d_thisCallResourceUsed(0)
-  , d_thisCallTimeBudget(0)
-  , d_thisCallResourceBudget(0)
-  , d_isHardLimit()
-  , d_on(false)
-  , d_cpuTime(false)
-  , d_spendResourceCalls(0)
-  , d_hardListeners()
-  , d_softListeners()
+ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options)
+    : d_cumulativeTimer(),
+      d_perCallTimer(),
+      d_timeBudgetCumulative(0),
+      d_timeBudgetPerCall(0),
+      d_resourceBudgetCumulative(0),
+      d_resourceBudgetPerCall(0),
+      d_cumulativeTimeUsed(0),
+      d_cumulativeResourceUsed(0),
+      d_thisCallResourceUsed(0),
+      d_thisCallTimeBudget(0),
+      d_thisCallResourceBudget(0),
+      d_isHardLimit(),
+      d_on(false),
+      d_cpuTime(false),
+      d_spendResourceCalls(0),
+      d_hardListeners(),
+      d_softListeners(),
+      d_statistics(new ResourceManager::Statistics(stats)),
+      d_options(options)
+
 {}
 
+ResourceManager::~ResourceManager() {}
 
 void ResourceManager::setResourceLimit(uint64_t units, bool cumulative) {
   d_on = true;
@@ -199,6 +282,72 @@ void ResourceManager::spendResource(unsigned amount)
   }
 }
 
+void ResourceManager::spendResource(Resource r)
+{
+  uint32_t amount = 0;
+  switch (r)
+  {
+    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::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::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);
+}
+
 void ResourceManager::beginCall() {
 
   d_perCallTimer.set(d_timeBudgetPerCall, !d_cpuTime);

diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index 264565a76b421683e8470a49ebe74079e45e8745..659d455f257f8d29fd1d4f8ab0a98d8b126d90c6 100644 (file)
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -20,15 +20,20 @@
 #ifndef CVC4__RESOURCE_MANAGER_H
 #define CVC4__RESOURCE_MANAGER_H
 
-#include <cstddef>
 #include <sys/time.h>
 
+#include <cstddef>
+#include <memory>
+
 #include "base/exception.h"
 #include "base/listener.h"
+#include "options/options.h"
 #include "util/unsafe_interrupt_exception.h"
 
 namespace CVC4 {
 
+class StatisticsRegistry;
+
 /**
  * A helper class to keep track of a time budget and signal
  * the PropEngine when the budget expires.
@@ -74,123 +79,145 @@ class CVC4_PUBLIC Timer {
 
 
 class CVC4_PUBLIC ResourceManager {
-
-  Timer d_cumulativeTimer;
-  Timer d_perCallTimer;
-
-  /** A user-imposed cumulative time budget, in milliseconds. 0 = no limit. */
-  uint64_t d_timeBudgetCumulative;
-  /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */
-  uint64_t d_timeBudgetPerCall;
-  /** A user-imposed cumulative resource budget. 0 = no limit. */
-  uint64_t d_resourceBudgetCumulative;
-  /** A user-imposed per-call resource budget. 0 = no limit. */
-  uint64_t d_resourceBudgetPerCall;
-
-  /** The number of milliseconds used. */
-  uint64_t d_cumulativeTimeUsed;
-  /** The amount of resource used. */
-  uint64_t d_cumulativeResourceUsed;
-
-  /** The amount of resource used during this call. */
-  uint64_t d_thisCallResourceUsed;
-
-  /**
-   * The amount of resource budget for this call (min between per call
-   * budget and left-over cumulative budget.
-   */
-  uint64_t d_thisCallTimeBudget;
-  uint64_t d_thisCallResourceBudget;
-
-  bool d_isHardLimit;
-  bool d_on;
-  bool d_cpuTime;
-  uint64_t d_spendResourceCalls;
-
-  /** Counter indicating how often to check resource manager in loops */
-  static const uint64_t s_resourceCount;
-
-  /** Receives a notification on reaching a hard limit. */
-  ListenerCollection d_hardListeners;
-
-  /** Receives a notification on reaching a hard limit. */
-  ListenerCollection d_softListeners;
-
-  /**
-   * ResourceManagers cannot be copied as they are given an explicit
-   * list of Listeners to respond to.
-   */
-  ResourceManager(const ResourceManager&) = delete;
-
-  /**
-   * ResourceManagers cannot be assigned as they are given an explicit
-   * list of Listeners to respond to.
-   */
-  ResourceManager& operator=(const ResourceManager&) = delete;
-
 public:
-
-  ResourceManager();
-
-  bool limitOn() const { return cumulativeLimitOn() || perCallLimitOn(); }
-  bool cumulativeLimitOn() const;
-  bool perCallLimitOn() const;
-
-  bool outOfResources() const;
-  bool outOfTime() const;
-  bool out() const { return d_on && (outOfResources() || outOfTime()); }
-
-
-  /**
-   * This returns a const uint64_t& to support being used as a ReferenceStat.
-   */
-  const uint64_t& getResourceUsage() const;
-  uint64_t getTimeUsage() const;
-  uint64_t getResourceRemaining() const;
-  uint64_t getTimeRemaining() const;
-
-  uint64_t getResourceBudgetForThisCall() {
-    return d_thisCallResourceBudget;
-  }
-  // Throws an UnsafeInterruptException if there are no remaining resources.
-  void spendResource(unsigned amount);
-
-  void setHardLimit(bool value);
-  void setResourceLimit(uint64_t units, bool cumulative = false);
-  void setTimeLimit(uint64_t millis, bool cumulative = false);
-  void useCPUTime(bool cpu);
-
-  void enable(bool on);
-
-  /**
-   * Resets perCall limits to mark the start of a new call,
-   * updates budget for current call and starts the timer
-   */
-  void beginCall();
-
-  /**
-   * Marks the end of a SmtEngine check call, stops the per
-   * call timer, updates cumulative time used.
-   */
-  void endCall();
-
-  static uint64_t getFrequencyCount() { return s_resourceCount; }
-
-  /**
-   * Registers a listener that is notified on a hard resource out.
-   *
-   * This Registration must be destroyed by the user before this
-   * ResourceManager.
-   */
-  ListenerCollection::Registration* registerHardListener(Listener* listener);
-
-  /**
-   * Registers a listener that is notified on a soft resource out.
-   *
-   * This Registration must be destroyed by the user before this
-   * ResourceManager.
-   */
-  ListenerCollection::Registration* registerSoftListener(Listener* listener);
+ enum class Resource
+ {
+   BitblastStep,
+   BvEagerAssertStep,
+   BvPropagationStep,
+   BvSatConflictsStep,
+   CnfStep,
+   DecisionStep,
+   LemmaStep,
+   ParseStep,
+   PreprocessStep,
+   QuantifierStep,
+   RestartStep,
+   RewriteStep,
+   SatConflictStep,
+   TheoryCheckStep,
+ };
+
+ ResourceManager(StatisticsRegistry& statistics_registry, Options& options);
+ ~ResourceManager();
+
+ bool limitOn() const { return cumulativeLimitOn() || perCallLimitOn(); }
+ bool cumulativeLimitOn() const;
+ bool perCallLimitOn() const;
+
+ bool outOfResources() const;
+ bool outOfTime() const;
+ bool out() const { return d_on && (outOfResources() || outOfTime()); }
+
+ /**
+  * This returns a const uint64_t& to support being used as a ReferenceStat.
+  */
+ const uint64_t& getResourceUsage() const;
+ uint64_t getTimeUsage() const;
+ uint64_t getResourceRemaining() const;
+ uint64_t getTimeRemaining() const;
+
+ uint64_t getResourceBudgetForThisCall() { return d_thisCallResourceBudget; }
+ // Throws an UnsafeInterruptException if there are no remaining resources.
+ void spendResource(Resource r);
+
+ void setHardLimit(bool value);
+ void setResourceLimit(uint64_t units, bool cumulative = false);
+ void setTimeLimit(uint64_t millis, bool cumulative = false);
+ void useCPUTime(bool cpu);
+
+ void enable(bool on);
+
+ /**
+  * Resets perCall limits to mark the start of a new call,
+  * updates budget for current call and starts the timer
+  */
+ void beginCall();
+
+ /**
+  * Marks the end of a SmtEngine check call, stops the per
+  * call timer, updates cumulative time used.
+  */
+ void endCall();
+
+ static uint64_t getFrequencyCount() { return s_resourceCount; }
+
+ /**
+  * Registers a listener that is notified on a hard resource out.
+  *
+  * This Registration must be destroyed by the user before this
+  * ResourceManager.
+  */
+ ListenerCollection::Registration* registerHardListener(Listener* listener);
+
+ /**
+  * Registers a listener that is notified on a soft resource out.
+  *
+  * This Registration must be destroyed by the user before this
+  * ResourceManager.
+  */
+ ListenerCollection::Registration* registerSoftListener(Listener* listener);
+
+private:
+ Timer d_cumulativeTimer;
+ Timer d_perCallTimer;
+
+ /** A user-imposed cumulative time budget, in milliseconds. 0 = no limit. */
+ uint64_t d_timeBudgetCumulative;
+ /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */
+ uint64_t d_timeBudgetPerCall;
+ /** A user-imposed cumulative resource budget. 0 = no limit. */
+ uint64_t d_resourceBudgetCumulative;
+ /** A user-imposed per-call resource budget. 0 = no limit. */
+ uint64_t d_resourceBudgetPerCall;
+
+ /** The number of milliseconds used. */
+ uint64_t d_cumulativeTimeUsed;
+ /** The amount of resource used. */
+ uint64_t d_cumulativeResourceUsed;
+
+ /** The amount of resource used during this call. */
+ uint64_t d_thisCallResourceUsed;
+
+ /**
+  * The amount of resource budget for this call (min between per call
+  * budget and left-over cumulative budget.
+  */
+ uint64_t d_thisCallTimeBudget;
+ uint64_t d_thisCallResourceBudget;
+
+ bool d_isHardLimit;
+ bool d_on;
+ bool d_cpuTime;
+ uint64_t d_spendResourceCalls;
+
+ /** Counter indicating how often to check resource manager in loops */
+ static const uint64_t s_resourceCount;
+
+ /** Receives a notification on reaching a hard limit. */
+ ListenerCollection d_hardListeners;
+
+ /** Receives a notification on reaching a hard limit. */
+ ListenerCollection d_softListeners;
+
+ /**
+  * ResourceManagers cannot be copied as they are given an explicit
+  * list of Listeners to respond to.
+  */
+ ResourceManager(const ResourceManager&) = delete;
+
+ /**
+  * ResourceManagers cannot be assigned as they are given an explicit
+  * list of Listeners to respond to.
+  */
+ ResourceManager& operator=(const ResourceManager&) = delete;
+
+ void spendResource(unsigned amount);
+
+ struct Statistics;
+ std::unique_ptr<Statistics> d_statistics;
+
+ Options& d_options;
 
 };/* class ResourceManager */
 

diff --git a/src/util/resource_manager.i b/src/util/resource_manager.i
deleted file mode 100644 (file)
index 0f55c2b..0000000
--- a/src/util/resource_manager.i
+++ /dev/null
@@ -1,5 +0,0 @@
-%{
-#include "util/resource_manager.h"
-%}
-
-%include "util/resource_manager.h"

diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 3c67218574e56424f95b2d5d0231758d36c6bcb3..5f7543f050fdcafa1ee2c3808f5bbf23e3ae996b 100644 (file)
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -15,6 +15,7 @@
  **/
 
 #include <cxxtest/TestSuite.h>
+
 #include <memory>
 #include <vector>
 
@@ -26,6 +27,7 @@
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
 #include "util/proof.h"
+#include "util/resource_manager.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
@@ -45,7 +47,7 @@ class TestOutputChannel : public OutputChannel {
   TestOutputChannel() {}
   ~TestOutputChannel() override {}
 
-  void safePoint(uint64_t amount) override {}
+  void safePoint(ResourceManager::Resource r) override {}
   void conflict(TNode n, std::unique_ptr<Proof> pf) override
   {
     push(CONFLICT, n);