From 508ecb3007a2b6aa8b76b28dc8282247b5dba957 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Wed, 19 Feb 2020 16:59:58 -0800 Subject: [PATCH] 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. --- src/bindings/java/CMakeLists.txt | 2 - src/cvc4.i | 1 - src/decision/decision_engine.h | 3 +- src/expr/expr_manager.i | 1 + src/expr/node_manager.cpp | 54 ++-- src/options/smt_options.toml | 18 ++ src/parser/parser.cpp | 6 +- src/preprocessing/passes/apply_substs.cpp | 3 +- src/preprocessing/passes/bool_to_bv.cpp | 2 +- src/preprocessing/passes/bv_to_bool.cpp | 2 +- src/preprocessing/passes/ite_removal.cpp | 2 +- src/preprocessing/passes/ite_simp.cpp | 4 +- src/preprocessing/passes/non_clausal_simp.cpp | 2 +- src/preprocessing/passes/static_learning.cpp | 2 +- .../passes/unconstrained_simplifier.cpp | 2 +- .../preprocessing_pass_context.h | 4 +- src/prop/bv_sat_solver_notify.h | 5 +- src/prop/bvminisat/bvminisat.h | 12 +- src/prop/bvminisat/core/Solver.cc | 10 +- src/prop/bvminisat/core/Solver.h | 8 +- src/prop/cnf_stream.cpp | 3 +- src/prop/minisat/core/Solver.cc | 24 +- src/prop/minisat/core/Solver.h | 3 +- src/prop/prop_engine.cpp | 4 +- src/prop/prop_engine.h | 3 +- src/prop/theory_proxy.cpp | 6 +- src/prop/theory_proxy.h | 3 +- src/smt/smt_engine.cpp | 13 +- src/theory/arith/theory_arith.cpp | 2 +- src/theory/arrays/theory_arrays.cpp | 2 +- src/theory/bv/bitblast/bitblaster.h | 7 +- src/theory/bv/bitblast/eager_bitblaster.cpp | 2 +- src/theory/bv/bitblast/lazy_bitblaster.cpp | 10 +- src/theory/bv/bitblast/lazy_bitblaster.h | 4 +- src/theory/bv/bv_eager_solver.cpp | 2 +- src/theory/bv/bv_subtheory_bitblast.cpp | 2 +- src/theory/bv/bv_subtheory_core.cpp | 2 +- src/theory/bv/bv_subtheory_inequality.cpp | 2 +- src/theory/bv/theory_bv.cpp | 4 +- src/theory/bv/theory_bv.h | 2 +- src/theory/output_channel.h | 4 +- src/theory/quantifiers/instantiate.cpp | 2 +- src/theory/rewriter.cpp | 2 +- src/theory/sep/theory_sep.cpp | 2 +- src/theory/theory_engine.cpp | 4 +- src/theory/theory_engine.h | 13 +- src/theory/theory_test_utils.h | 3 +- src/theory/uf/theory_uf.cpp | 2 +- src/util/resource_manager.cpp | 185 +++++++++++-- src/util/resource_manager.h | 261 ++++++++++-------- src/util/resource_manager.i | 5 - test/unit/theory/theory_white.h | 4 +- 52 files changed, 468 insertions(+), 262 deletions(-) delete mode 100644 src/util/resource_manager.i diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt index 7c2985e5c..589890ead 100644 --- 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 bed988b32..6ed620960 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -321,7 +321,6 @@ std::set 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 41d439d4f..5ebcda8fe 100644 --- 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 7cc635259..dbfd01242 100644 --- 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 39be675ec..367162420 100644 --- 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 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 cd8a530fc..f78dbb3b8 100644 --- 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 681b2a1c9..32d555718 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -640,8 +640,7 @@ Command* Parser::nextCommand() dynamic_cast(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 791bb2dc7..98313efda 100644 --- 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 7787d7631..30b64fd74 100644 --- 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 3d3762ecd..0637c541f 100644 --- 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 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 bda38a6df..6ad97f4a3 100644 --- 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 ad00ec204..7f7c4c95f 100644 --- 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()) diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index 139bf96a9..03f38370b 100644 --- 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 7af9f7fac..ec3982e03 100644 --- 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 1695ae2ff..8a2c58b99 100644 --- 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& assertions = assertionsToPreprocess->ref(); diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index 37744151c..70b1f70c2 100644 --- 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 77163cfe6..eca6bdfd6 100644 --- 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 70e0b9157..f71dac3e5 100644 --- 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& 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 d_minisat; diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 04658fc38..25b6a3da2 100644 --- 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 eef1c4e4c..2197d030f 100644 --- 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& 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 6d60bfafc..6690f12db 100644 --- 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 6126983fa..83f6fb897 100644 --- 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 aa3b96c57..0cec30d24 100644 --- 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 8a0cc9f15..bac584236 100644 --- 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 aaa65b85a..efbd82947 100644 --- 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 1258d2ee2..cf7c9f0d9 100644 --- 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 3bb15aa4e..61c556f34 100644 --- 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 f1d602bc6..2dc20cc31 100644 --- 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_mapd_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 6943c5546..8986e6894 100644 --- 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 f2beec0b8..534a019c3 100644 --- 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 df7cc4f11..a16a8bbbf 100644 --- 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 cd906769d..c4e3513bf 100644 --- 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 2018590f7..06afa126d 100644 --- 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 ac5cd5c7f..3fe2398f1 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.h +++ b/src/theory/bv/bitblast/lazy_bitblaster.h @@ -120,8 +120,8 @@ class TLazyBitblaster : public TBitblaster 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 dd0458a70..d743a6023 100644 --- 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 25fe7002e..b5e4b7c85 100644 --- 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 bf9bfa480..5d9c297f1 100644 --- 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 332f96aa2..8a895e9eb 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -33,7 +33,7 @@ bool InequalitySolver::check(Theory::Effort e) { Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n"; TimerStat::CodeTimer inequalityTimer(d_statistics.d_solveTime); ++(d_statistics.d_numCallstoCheck); - d_bv->spendResource(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 48168d7d6..a35176a93 100644 --- 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 7ca98f2ea..196535a19 100644 --- 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 bcbbfa274..dc5dfc388 100644 --- 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 aec648037..1d1eb9751 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -110,7 +110,7 @@ bool Instantiate::addInstantiation( Node q, std::vector& 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 7a99ed2d9..2a7c3ff0d 100644 --- 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 1392f8fab..b5fc1cbc9 100644 --- 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 b43e55364..9cd226ba1 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -2313,9 +2313,9 @@ std::pair 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 5506b0120..0770efc7b 100644 --- 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 dbb42f2bc..17b47d2d3 100644 --- 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 pf) override { push(CONFLICT, n); diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 4d13bf3f2..e336d1630 100644 --- 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 8f00a23ea..2667d8513 100644 --- 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 264565a76..659d455f2 100644 --- 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 #include +#include +#include + #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 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 index 0f55c2bce..000000000 --- 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 3c6721857..5f7543f05 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -15,6 +15,7 @@ **/ #include + #include #include @@ -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 pf) override { push(CONFLICT, n); -- 2.30.2