diff options
| -rw-r--r-- | src/options/smt_options.toml | 9 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 21 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 31 | ||||
| -rw-r--r-- | src/theory/smt_engine_subsolver.cpp | 2 | ||||
| -rw-r--r-- | src/util/resource_manager.cpp | 270 | ||||
| -rw-r--r-- | src/util/resource_manager.h | 327 |
6 files changed, 287 insertions, 373 deletions
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index e4847716a..96fccdcdb 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -492,15 +492,6 @@ header = "options/smt_options.h" help = "the resource limit is hard potentially leaving the smtEngine in an unsafe state (should be destroyed and rebuild after resourcing out)" [[option]] - name = "cpuTime" - category = "common" - long = "cpu-time" - type = "bool" - default = "false" - read_only = true - help = "measures CPU time if set to true and wall time if false (default false)" - -[[option]] name = "rewriteStep" category = "expert" long = "rewrite-step=N" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ff5cff5b6..d80c01035 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -727,16 +727,7 @@ void SmtEngine::finishInit() } if (options::perCallMillisecondLimit() != 0) { - d_resourceManager->setTimeLimit(options::perCallMillisecondLimit(), false); - } - if (options::cumulativeMillisecondLimit() != 0) - { - d_resourceManager->setTimeLimit(options::cumulativeMillisecondLimit(), - true); - } - if (options::cpuTime()) - { - d_resourceManager->useCPUTime(true); + d_resourceManager->setTimeLimit(options::perCallMillisecondLimit()); } // set the random seed @@ -3430,8 +3421,9 @@ void SmtEngine::interrupt() void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) { d_resourceManager->setResourceLimit(units, cumulative); } -void SmtEngine::setTimeLimit(unsigned long milis, bool cumulative) { - d_resourceManager->setTimeLimit(milis, cumulative); +void SmtEngine::setTimeLimit(unsigned long milis) +{ + d_resourceManager->setTimeLimit(milis); } unsigned long SmtEngine::getResourceUsage() const { @@ -3447,11 +3439,6 @@ unsigned long SmtEngine::getResourceRemaining() const return d_resourceManager->getResourceRemaining(); } -unsigned long SmtEngine::getTimeRemaining() const -{ - return d_resourceManager->getTimeRemaining(); -} - NodeManager* SmtEngine::getNodeManager() const { return d_exprManager->getNodeManager(); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 3ed2b987c..738a6c22a 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -775,18 +775,14 @@ class CVC4_PUBLIC SmtEngine void setResourceLimit(unsigned long units, bool cumulative = false); /** - * Set a time limit for SmtEngine operations. + * Set a per-call time limit for SmtEngine operations. * - * A cumulative and non-cumulative (per-call) time limit can be - * set at the same time. A call to setTimeLimit() with - * cumulative==true replaces any cumulative time limit currently - * in effect; a call with cumulative==false replaces any per-call - * time limit currently in effect. Resource limits can be set in - * addition to time limits; the SmtEngine obeys both. That means - * that up to four independent limits can control the SmtEngine - * at the same time. + * A per-call time limit can be set at the same time and replaces + * any per-call time limit currently in effect. + * Resource limits (either per-call or cumulative) can be set in + * addition to a time limit; the SmtEngine obeys all three of them. * - * Note that the cumulative timer only ticks away when one of the + * Note that the per-call timer only ticks away when one of the * SmtEngine's workhorse functions (things like assertFormula(), * checkEntailed(), checkSat(), and simplify()) are running. * Between calls, the timer is still. @@ -800,11 +796,8 @@ class CVC4_PUBLIC SmtEngine * We reserve the right to change this in the future. * * @param millis the time limit in milliseconds, or 0 for no limit - * @param cumulative whether this time limit is to be a cumulative - * time limit for all remaining calls into the SmtEngine (true), or - * whether it's a per-call time limit (false); the default is false */ - void setTimeLimit(unsigned long millis, bool cumulative = false); + void setTimeLimit(unsigned long millis); /** * Get the current resource usage count for this SmtEngine. This @@ -826,16 +819,6 @@ class CVC4_PUBLIC SmtEngine */ unsigned long getResourceRemaining() const; - /** - * Get the remaining number of milliseconds that can be consumed by - * this SmtEngine according to the currently-set cumulative time limit. - * If there is not a cumulative resource limit set, this function - * throws a ModalException. - * - * @throw ModalException - */ - unsigned long getTimeRemaining() const; - /** Permit access to the underlying ExprManager. */ ExprManager* getExprManager() const { return d_exprManager; } diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp index 41526c30d..2419962aa 100644 --- a/src/theory/smt_engine_subsolver.cpp +++ b/src/theory/smt_engine_subsolver.cpp @@ -53,7 +53,7 @@ void initializeSubsolver(std::unique_ptr<SmtEngine>& smte, smte->setLogic(smtCurr->getLogicInfo()); if (needsTimeout) { - smte->setTimeLimit(timeout, true); + smte->setTimeLimit(timeout); } smte->setLogic(smt::currentSmtEngine()->getLogicInfo()); } diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index eddf9e5c9..7080d5040 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -25,79 +25,59 @@ using namespace std; namespace CVC4 { -void Timer::set(uint64_t millis, bool wallTime) { +void Timer::set(uint64_t millis) +{ d_ms = millis; Trace("limit") << "Timer::set(" << d_ms << ")" << std::endl; // keep track of when it was set, even if it's disabled (i.e. == 0) - d_wall_time = wallTime; - if (d_wall_time) { - // Wall time - gettimeofday(&d_wall_limit, NULL); - Trace("limit") << "Timer::set(): it's " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl; - d_wall_limit.tv_sec += millis / 1000; - d_wall_limit.tv_usec += (millis % 1000) * 1000; - if(d_wall_limit.tv_usec > 1000000) { - ++d_wall_limit.tv_sec; - d_wall_limit.tv_usec -= 1000000; - } - Trace("limit") << "Timer::set(): limit is at " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl; - } else { - // CPU time - d_cpu_start_time = ((double)clock())/(CLOCKS_PER_SEC *0.001); - d_cpu_limit = d_cpu_start_time + d_ms; + // Wall time + gettimeofday(&d_wall_limit, NULL); + Trace("limit") << "Timer::set(): it's " << d_wall_limit.tv_sec << "," + << d_wall_limit.tv_usec << std::endl; + d_wall_limit.tv_sec += millis / 1000; + d_wall_limit.tv_usec += (millis % 1000) * 1000; + if (d_wall_limit.tv_usec > 1000000) + { + ++d_wall_limit.tv_sec; + d_wall_limit.tv_usec -= 1000000; } + Trace("limit") << "Timer::set(): limit is at " << d_wall_limit.tv_sec << "," + << d_wall_limit.tv_usec << std::endl; } /** Return the milliseconds elapsed since last set(). */ -uint64_t Timer::elapsedWall() const { - Assert(d_wall_time); +uint64_t Timer::elapsed() const +{ timeval tv; gettimeofday(&tv, NULL); - Trace("limit") << "Timer::elapsedWallTime(): it's now " << tv.tv_sec << "," << tv.tv_usec << std::endl; + Trace("limit") << "Timer::elapsedWallTime(): it's now " << tv.tv_sec << "," + << tv.tv_usec << std::endl; tv.tv_sec -= d_wall_limit.tv_sec - d_ms / 1000; tv.tv_usec -= d_wall_limit.tv_usec - (d_ms % 1000) * 1000; - Trace("limit") << "Timer::elapsedWallTime(): elapsed time is " << tv.tv_sec << "," << tv.tv_usec << std::endl; + Trace("limit") << "Timer::elapsedWallTime(): elapsed time is " << tv.tv_sec + << "," << tv.tv_usec << std::endl; return tv.tv_sec * 1000 + tv.tv_usec / 1000; } -uint64_t Timer::elapsedCPU() const { - Assert(!d_wall_time); - clock_t elapsed = ((double)clock())/(CLOCKS_PER_SEC *0.001)- d_cpu_start_time; - Trace("limit") << "Timer::elapsedCPUTime(): elapsed time is " << elapsed << " ms" <<std::endl; - return elapsed; -} - -uint64_t Timer::elapsed() const { - if (d_wall_time) - return elapsedWall(); - return elapsedCPU(); -} - -bool Timer::expired() const { +bool Timer::expired() const +{ if (!on()) return false; - if (d_wall_time) { - timeval tv; - gettimeofday(&tv, NULL); - Debug("limit") << "Timer::expired(): current wall time is " << tv.tv_sec << "," << tv.tv_usec << std::endl; - Debug("limit") << "Timer::expired(): limit wall time is " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl; - if(d_wall_limit.tv_sec < tv.tv_sec || - (d_wall_limit.tv_sec == tv.tv_sec && d_wall_limit.tv_usec <= tv.tv_usec)) { - Debug("limit") << "Timer::expired(): OVER LIMIT!" << std::endl; - return true; - } - Debug("limit") << "Timer::expired(): within limit" << std::endl; - return false; - } - - // cpu time - double current = ((double)clock())/(CLOCKS_PER_SEC*0.001); - Debug("limit") << "Timer::expired(): current cpu time is " << current << std::endl; - Debug("limit") << "Timer::expired(): limit cpu time is " << d_cpu_limit << std::endl; - if (current >= d_cpu_limit) { - Debug("limit") << "Timer::expired(): OVER LIMIT!" << current << std::endl; + timeval tv; + gettimeofday(&tv, NULL); + Debug("limit") << "Timer::expired(): current wall time is " << tv.tv_sec + << "," << tv.tv_usec << std::endl; + Debug("limit") << "Timer::expired(): limit wall time is " + << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec + << std::endl; + if (d_wall_limit.tv_sec < tv.tv_sec + || (d_wall_limit.tv_sec == tv.tv_sec + && d_wall_limit.tv_usec <= tv.tv_usec)) + { + Debug("limit") << "Timer::expired(): OVER LIMIT!" << std::endl; return true; } + Debug("limit") << "Timer::expired(): within limit" << std::endl; return false; } @@ -182,9 +162,7 @@ ResourceManager::Statistics::~Statistics() const uint64_t ResourceManager::s_resourceCount = 1000; ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options) - : d_cumulativeTimer(), - d_perCallTimer(), - d_timeBudgetCumulative(0), + : d_perCallTimer(), d_timeBudgetPerCall(0), d_resourceBudgetCumulative(0), d_resourceBudgetPerCall(0), @@ -195,65 +173,56 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options) 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) { +void ResourceManager::setResourceLimit(uint64_t units, bool cumulative) +{ d_on = true; - if(cumulative) { - Trace("limit") << "ResourceManager: setting cumulative resource limit to " << units << endl; - d_resourceBudgetCumulative = (units == 0) ? 0 : (d_cumulativeResourceUsed + units); + if (cumulative) + { + Trace("limit") << "ResourceManager: setting cumulative resource limit to " + << units << endl; + d_resourceBudgetCumulative = + (units == 0) ? 0 : (d_cumulativeResourceUsed + units); d_thisCallResourceBudget = d_resourceBudgetCumulative; - } else { - Trace("limit") << "ResourceManager: setting per-call resource limit to " << units << endl; + } + else + { + Trace("limit") << "ResourceManager: setting per-call resource limit to " + << units << endl; d_resourceBudgetPerCall = units; } } -void ResourceManager::setTimeLimit(uint64_t millis, bool cumulative) { +void ResourceManager::setTimeLimit(uint64_t millis) +{ d_on = true; - if(cumulative) { - Trace("limit") << "ResourceManager: setting cumulative time limit to " << millis << " ms" << endl; - d_timeBudgetCumulative = (millis == 0) ? 0 : (d_cumulativeTimeUsed + millis); - d_cumulativeTimer.set(millis, !d_cpuTime); - } else { - Trace("limit") << "ResourceManager: setting per-call time limit to " << millis << " ms" << endl; - d_timeBudgetPerCall = millis; - // perCall timer will be set in beginCall - } - + Trace("limit") << "ResourceManager: setting per-call time limit to " << millis + << " ms" << endl; + d_timeBudgetPerCall = millis; + // perCall timer will be set in beginCall } -const uint64_t& ResourceManager::getResourceUsage() const { +const uint64_t& ResourceManager::getResourceUsage() const +{ return d_cumulativeResourceUsed; } -uint64_t ResourceManager::getTimeUsage() const { - if (d_timeBudgetCumulative) { - return d_cumulativeTimer.elapsed(); - } - return d_cumulativeTimeUsed; -} +uint64_t ResourceManager::getTimeUsage() const { return d_cumulativeTimeUsed; } -uint64_t ResourceManager::getResourceRemaining() const { - if (d_thisCallResourceBudget <= d_thisCallResourceUsed) - return 0; - return d_thisCallResourceBudget - d_thisCallResourceUsed; -} - -uint64_t ResourceManager::getTimeRemaining() const { - uint64_t time_passed = d_cumulativeTimer.elapsed(); - if (time_passed >= d_thisCallTimeBudget) - return 0; - return d_thisCallTimeBudget - time_passed; +uint64_t ResourceManager::getResourceRemaining() const +{ + if (d_resourceBudgetCumulative <= d_cumulativeResourceUsed) return 0; + return d_resourceBudgetCumulative - d_cumulativeResourceUsed; } void ResourceManager::spendResource(unsigned amount) @@ -264,21 +233,25 @@ void ResourceManager::spendResource(unsigned amount) Debug("limit") << "ResourceManager::spendResource()" << std::endl; d_thisCallResourceUsed += amount; - if(out()) { + if (out()) + { Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl; Trace("limit") << " on call " << d_spendResourceCalls << std::endl; - if (outOfTime()) { + if (outOfTime()) + { Trace("limit") << "ResourceManager::spendResource: elapsed time" - << d_cumulativeTimer.elapsed() << std::endl; + << d_perCallTimer.elapsed() << std::endl; } - if (d_isHardLimit) { + if (d_isHardLimit) + { d_hardListeners.notify(); throw UnsafeInterruptException(); - } else { + } + else + { d_softListeners.notify(); } - } } @@ -348,88 +321,89 @@ void ResourceManager::spendResource(Resource r) spendResource(amount); } -void ResourceManager::beginCall() { - - d_perCallTimer.set(d_timeBudgetPerCall, !d_cpuTime); +void ResourceManager::beginCall() +{ + d_perCallTimer.set(d_timeBudgetPerCall); d_thisCallResourceUsed = 0; if (!d_on) return; - if (cumulativeLimitOn()) { - if (d_resourceBudgetCumulative) { - d_thisCallResourceBudget = d_resourceBudgetCumulative <= d_cumulativeResourceUsed ? 0 : - d_resourceBudgetCumulative - d_cumulativeResourceUsed; - } - - if (d_timeBudgetCumulative) { - AlwaysAssert(d_cumulativeTimer.on()); - // timer was on since the option was set - d_cumulativeTimeUsed = d_cumulativeTimer.elapsed(); - d_thisCallTimeBudget = d_timeBudgetCumulative <= d_cumulativeTimeUsed? 0 : - d_timeBudgetCumulative - d_cumulativeTimeUsed; - d_cumulativeTimer.set(d_thisCallTimeBudget, d_cpuTime); + if (cumulativeLimitOn()) + { + if (d_resourceBudgetCumulative) + { + d_thisCallResourceBudget = + d_resourceBudgetCumulative <= d_cumulativeResourceUsed + ? 0 + : d_resourceBudgetCumulative - d_cumulativeResourceUsed; } // we are out of resources so we shouldn't update the // budget for this call to the per call budget - if (d_thisCallTimeBudget == 0 || - d_thisCallResourceUsed == 0) - return; + if (d_thisCallTimeBudget == 0 || d_thisCallResourceUsed == 0) return; } - if (perCallLimitOn()) { + if (perCallLimitOn()) + { // take min of what's left and per-call budget - if (d_resourceBudgetPerCall) { - d_thisCallResourceBudget = d_thisCallResourceBudget < d_resourceBudgetPerCall && d_thisCallResourceBudget != 0 ? d_thisCallResourceBudget : d_resourceBudgetPerCall; + if (d_resourceBudgetPerCall) + { + d_thisCallResourceBudget = + d_thisCallResourceBudget < d_resourceBudgetPerCall + && d_thisCallResourceBudget != 0 + ? d_thisCallResourceBudget + : d_resourceBudgetPerCall; } - if (d_timeBudgetPerCall) { - d_thisCallTimeBudget = d_thisCallTimeBudget < d_timeBudgetPerCall && d_thisCallTimeBudget != 0 ? d_thisCallTimeBudget : d_timeBudgetPerCall; + if (d_timeBudgetPerCall) + { + d_thisCallTimeBudget = d_thisCallTimeBudget < d_timeBudgetPerCall + && d_thisCallTimeBudget != 0 + ? d_thisCallTimeBudget + : d_timeBudgetPerCall; } } } -void ResourceManager::endCall() { - uint64_t usedInCall = d_perCallTimer.elapsed(); +void ResourceManager::endCall() +{ + d_cumulativeTimeUsed += d_perCallTimer.elapsed(); d_perCallTimer.set(0); - d_cumulativeTimeUsed += usedInCall; } -bool ResourceManager::cumulativeLimitOn() const { - return d_timeBudgetCumulative || d_resourceBudgetCumulative; +bool ResourceManager::cumulativeLimitOn() const +{ + return d_resourceBudgetCumulative; } -bool ResourceManager::perCallLimitOn() const { +bool ResourceManager::perCallLimitOn() const +{ return d_timeBudgetPerCall || d_resourceBudgetPerCall; } -bool ResourceManager::outOfResources() const { +bool ResourceManager::outOfResources() const +{ // resource limiting not enabled - if (d_resourceBudgetPerCall == 0 && - d_resourceBudgetCumulative == 0) + if (d_resourceBudgetPerCall == 0 && d_resourceBudgetCumulative == 0) return false; return getResourceRemaining() == 0; } -bool ResourceManager::outOfTime() const { - if (d_timeBudgetPerCall == 0 && - d_timeBudgetCumulative == 0) - return false; - - return d_cumulativeTimer.expired() || d_perCallTimer.expired(); -} +bool ResourceManager::outOfTime() const +{ + if (d_timeBudgetPerCall == 0) return false; -void ResourceManager::useCPUTime(bool cpu) { - Trace("limit") << "ResourceManager::useCPUTime("<< cpu <<")\n"; - d_cpuTime = cpu; + return d_perCallTimer.expired(); } -void ResourceManager::setHardLimit(bool value) { - Trace("limit") << "ResourceManager::setHardLimit("<< value <<")\n"; +void ResourceManager::setHardLimit(bool value) +{ + Trace("limit") << "ResourceManager::setHardLimit(" << value << ")\n"; d_isHardLimit = value; } -void ResourceManager::enable(bool on) { - Trace("limit") << "ResourceManager::enable("<< on <<")\n"; +void ResourceManager::enable(bool on) +{ + Trace("limit") << "ResourceManager::enable(" << on << ")\n"; d_on = on; } diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index 39fceb7ec..822f17713 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -9,11 +9,12 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** [[ Add lengthier description here ]] - - ** \todo document this file - -**/ + ** \brief Provides mechanisms to limit resources. + ** + ** This file provides the ResourceManager class. It can be used to impose + ** (cumulative and per-call) resource limits on the solver, as well as per-call + ** time limits. + **/ #include "cvc4_public.h" @@ -38,190 +39,168 @@ class StatisticsRegistry; * A helper class to keep track of a time budget and signal * the PropEngine when the budget expires. */ -class CVC4_PUBLIC Timer { +class CVC4_PUBLIC Timer +{ public: /** Construct a Timer. */ - Timer() - : d_ms(0), - d_cpu_start_time(0), - d_cpu_limit(0), - d_wall_time(true) + Timer() : d_ms(0) { d_wall_limit.tv_sec = 0; d_wall_limit.tv_usec = 0; } /** Is the timer currently active? */ - bool on() const { - return d_ms != 0; - } + bool on() const { return d_ms != 0; } /** Set a millisecond timer (0==off). */ - void set(uint64_t millis, bool wall_time = true); - /** Return the milliseconds elapsed since last set() wall/cpu time - depending on d_wall_time*/ + void set(uint64_t millis); + /** Return the milliseconds elapsed since last set() wall time. */ uint64_t elapsed() const; bool expired() const; private: - - /** Return the milliseconds elapsed since last set() cpu time. */ - uint64_t elapsedCPU() const; - /** Return the milliseconds elapsed since last set() wall time. */ - uint64_t elapsedWall() const; - uint64_t d_ms; - clock_t d_cpu_start_time; - clock_t d_cpu_limit; - bool d_wall_time; timeval d_wall_limit; -};/* class Timer */ - - -class CVC4_PUBLIC ResourceManager { -public: - 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 */ - - -}/* CVC4 namespace */ +}; /* class Timer */ + +class CVC4_PUBLIC ResourceManager +{ + public: + 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 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); + + 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. + */ + 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_perCallTimer; + + /** 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; + 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 */ + +} // namespace CVC4 #endif /* CVC4__RESOURCE_MANAGER_H */ |