diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/resource_manager.cpp | 185 | ||||
-rw-r--r-- | src/util/resource_manager.h | 261 | ||||
-rw-r--r-- | src/util/resource_manager.i | 5 |
3 files changed, 311 insertions, 140 deletions
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 <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 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" |