read_only = true
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"
}
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
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 {
return d_resourceManager->getResourceRemaining();
}
-unsigned long SmtEngine::getTimeRemaining() const
-{
- return d_resourceManager->getTimeRemaining();
-}
-
NodeManager* SmtEngine::getNodeManager() const
{
return d_exprManager->getNodeManager();
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.
* 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
*/
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; }
smte->setLogic(smtCurr->getLogicInfo());
if (needsTimeout)
{
- smte->setTimeLimit(timeout, true);
+ smte->setTimeLimit(timeout);
}
smte->setLogic(smt::currentSmtEngine()->getLogicInfo());
}
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;
}
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),
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)
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();
}
-
}
}
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;
}
** 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"
* 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 */
projects / cvc5.git / commitdiff