From 508ecb3007a2b6aa8b76b28dc8282247b5dba957 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Wed, 19 Feb 2020 16:59:58 -0800 Subject: 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/util/resource_manager.cpp | 185 ++++++++++++++++++++++++++++++++++++++---- 1 file changed, 167 insertions(+), 18 deletions(-) (limited to 'src/util/resource_manager.cpp') 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); -- cgit v1.2.3