This PR performs some general cleanup in and around the ResourceManager class. In detail, it does
remove --hard-limit (we decided to always leave the solver in a usable state, i.e. always do a soft limit),
remove --cpu-time (we decided to always use wall-clock time for time limiting)
replace old gettimeofday-based Timer by new std::chrono-based WallClockTimer
clean up the logic around beginCall() and endCall()
read_only = true
help = "enable resource limiting per query"
-[[option]]
- name = "hardLimit"
- category = "common"
- long = "hard-limit"
- type = "bool"
- default = "false"
- 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 = "rewriteStep"
category = "expert"
commands.clear();
}
-class SoftResourceOutListener : public Listener {
+class ResourceOutListener : public Listener {
public:
- SoftResourceOutListener(SmtEngine& smt) : d_smt(&smt) {}
+ ResourceOutListener(SmtEngine& smt) : d_smt(&smt) {}
void notify() override
{
SmtScope scope(d_smt);
}
private:
SmtEngine* d_smt;
-}; /* class SoftResourceOutListener */
-
-
-class HardResourceOutListener : public Listener {
- public:
- HardResourceOutListener(SmtEngine& smt) : d_smt(&smt) {}
- void notify() override
- {
- SmtScope scope(d_smt);
- theory::Rewriter::clearCaches();
- }
- private:
- SmtEngine* d_smt;
-}; /* class HardResourceOutListener */
+}; /* class ResourceOutListener */
class BeforeSearchListener : public Listener {
public:
ResourceManager* rm = d_smt.getResourceManager();
d_listenerRegistrations->add(
- rm->registerSoftListener(new SoftResourceOutListener(d_smt)));
-
- d_listenerRegistrations->add(
- rm->registerHardListener(new HardResourceOutListener(d_smt)));
+ rm->registerListener(new ResourceOutListener(d_smt)));
try
{
new ResourceManager(*d_statisticsRegistry.get(), d_options));
d_private.reset(new smt::SmtEnginePrivate(*this));
d_stats.reset(new SmtEngineStatistics());
- d_stats->d_resourceUnitsUsed.setData(d_resourceManager->getResourceUsage());
-
+
// The ProofManager is constructed before any other proof objects such as
// SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
// initialized in TheoryEngine and PropEngine respectively.
// of SMT-LIB 2.6 standard.
// Inialize the resource manager based on the options.
- d_resourceManager->setHardLimit(options::hardLimit());
if (options::perCallResourceLimit() != 0)
{
d_resourceManager->setResourceLimit(options::perCallResourceLimit(), false);
Trace("smt") << "SmtEngine::check()" << endl;
- d_resourceManager->beginCall();
- // Only way we can be out of resource is if cumulative budget is on
- if (d_resourceManager->cumulativeLimitOn() && d_resourceManager->out())
+ if (d_resourceManager->out())
{
Result::UnknownExplanation why = d_resourceManager->outOfResources()
? Result::RESOURCEOUT
: Result::TIMEOUT;
return Result(Result::ENTAILMENT_UNKNOWN, why, d_filename);
}
+ d_resourceManager->beginCall();
// Make sure the prop layer has all of the assertions
Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
d_solveTime("smt::SmtEngine::solveTime"),
d_pushPopTime("smt::SmtEngine::pushPopTime"),
d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
- d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0),
- d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed")
+ d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0)
{
smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime);
smtStatisticsRegistry()->registerStat(&d_numConstantProps);
smtStatisticsRegistry()->registerStat(&d_pushPopTime);
smtStatisticsRegistry()->registerStat(&d_processAssertionsTime);
smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse);
- smtStatisticsRegistry()->registerStat(&d_resourceUnitsUsed);
}
SmtEngineStatistics::~SmtEngineStatistics()
smtStatisticsRegistry()->unregisterStat(&d_pushPopTime);
smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime);
smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse);
- smtStatisticsRegistry()->unregisterStat(&d_resourceUnitsUsed);
}
} // namespace smt
/** Has something simplified to false? */
IntStat d_simplifiedToFalse;
- /** Number of resource units spent. */
- ReferenceStat<uint64_t> d_resourceUnitsUsed;
}; /* struct SmtEngineStatistics */
} // namespace smt
namespace CVC4 {
-void Timer::set(uint64_t millis)
+bool WallClockTimer::on() const
{
- 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)
- // 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)
+ // default-constructed time points are at the respective epoch
+ return d_limit.time_since_epoch().count() != 0;
+}
+void WallClockTimer::set(uint64_t millis)
+{
+ if (millis == 0)
+ {
+ // reset / deactivate
+ d_start = time_point();
+ d_limit = time_point();
+ }
+ else
{
- ++d_wall_limit.tv_sec;
- d_wall_limit.tv_usec -= 1000000;
+ // set to now() + millis
+ d_start = clock::now();
+ d_limit = d_start + std::chrono::milliseconds(millis);
}
- 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::elapsed() const
+uint64_t WallClockTimer::elapsed() const
{
- timeval tv;
- gettimeofday(&tv, NULL);
- 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;
- return tv.tv_sec * 1000 + tv.tv_usec / 1000;
+ if (!on()) return 0;
+ // now() - d_start casted to milliseconds
+ return std::chrono::duration_cast<std::chrono::milliseconds>(clock::now()
+ - d_start)
+ .count();
}
-
-bool Timer::expired() const
+bool WallClockTimer::expired() const
{
+ // whether d_limit is in the past
if (!on()) return false;
-
- 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;
+ return d_limit <= clock::now();
}
/*---------------------------------------------------------------------------*/
struct ResourceManager::Statistics
{
+ ReferenceStat<std::uint64_t> d_resourceUnitsUsed;
+ IntStat d_spendResourceCalls;
IntStat d_numBitblastStep;
IntStat d_numBvEagerAssertStep;
IntStat d_numBvPropagationStep;
};
ResourceManager::Statistics::Statistics(StatisticsRegistry& stats)
- : d_numBitblastStep("resource::BitblastStep", 0),
+ : d_resourceUnitsUsed("resource::resourceUnitsUsed"),
+ d_spendResourceCalls("resource::spendResourceCalls", 0),
+ d_numBitblastStep("resource::BitblastStep", 0),
d_numBvEagerAssertStep("resource::BvEagerAssertStep", 0),
d_numBvPropagationStep("resource::BvPropagationStep", 0),
d_numBvSatConflictsStep("resource::BvSatConflictsStep", 0),
d_numTheoryCheckStep("resource::TheoryCheckStep", 0),
d_statisticsRegistry(stats)
{
+ d_statisticsRegistry.registerStat(&d_resourceUnitsUsed);
+ d_statisticsRegistry.registerStat(&d_spendResourceCalls);
d_statisticsRegistry.registerStat(&d_numBitblastStep);
d_statisticsRegistry.registerStat(&d_numBvEagerAssertStep);
d_statisticsRegistry.registerStat(&d_numBvPropagationStep);
ResourceManager::Statistics::~Statistics()
{
+ d_statisticsRegistry.unregisterStat(&d_resourceUnitsUsed);
+ d_statisticsRegistry.unregisterStat(&d_spendResourceCalls);
d_statisticsRegistry.unregisterStat(&d_numBitblastStep);
d_statisticsRegistry.unregisterStat(&d_numBvEagerAssertStep);
d_statisticsRegistry.unregisterStat(&d_numBvPropagationStep);
d_cumulativeTimeUsed(0),
d_cumulativeResourceUsed(0),
d_thisCallResourceUsed(0),
- d_thisCallTimeBudget(0),
d_thisCallResourceBudget(0),
- d_isHardLimit(),
d_on(false),
- d_spendResourceCalls(0),
- d_hardListeners(),
- d_softListeners(),
+ d_listeners(),
d_statistics(new ResourceManager::Statistics(stats)),
d_options(options)
{
+ d_statistics->d_resourceUnitsUsed.setData(d_cumulativeResourceUsed);
}
ResourceManager::~ResourceManager() {}
// perCall timer will be set in beginCall
}
-const uint64_t& ResourceManager::getResourceUsage() const
+uint64_t ResourceManager::getResourceUsage() const
{
return d_cumulativeResourceUsed;
}
void ResourceManager::spendResource(unsigned amount)
{
- ++d_spendResourceCalls;
+ ++d_statistics->d_spendResourceCalls;
d_cumulativeResourceUsed += amount;
if (!d_on) return;
if (out())
{
Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl;
- Trace("limit") << " on call " << d_spendResourceCalls << std::endl;
+ Trace("limit") << " on call " << d_statistics->d_spendResourceCalls.getData() << std::endl;
if (outOfTime())
{
Trace("limit") << "ResourceManager::spendResource: elapsed time"
<< d_perCallTimer.elapsed() << std::endl;
}
- if (d_isHardLimit)
- {
- d_hardListeners.notify();
- throw UnsafeInterruptException();
- }
- else
- {
- d_softListeners.notify();
- }
+ d_listeners.notify();
}
}
d_thisCallResourceUsed = 0;
if (!d_on) return;
- if (cumulativeLimitOn())
+ if (d_resourceBudgetCumulative > 0)
{
- 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;
+ // Compute remaining cumulative resource budget
+ d_thisCallResourceBudget =
+ d_resourceBudgetCumulative - d_cumulativeResourceUsed;
}
-
- if (perCallLimitOn())
+ if (d_resourceBudgetPerCall > 0)
{
- // 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_timeBudgetPerCall)
+ // Check if per-call resource budget is even smaller
+ if (d_resourceBudgetPerCall < d_thisCallResourceBudget)
{
- d_thisCallTimeBudget = d_thisCallTimeBudget < d_timeBudgetPerCall
- && d_thisCallTimeBudget != 0
- ? d_thisCallTimeBudget
- : d_timeBudgetPerCall;
+ d_thisCallResourceBudget = d_resourceBudgetPerCall;
}
}
}
{
d_cumulativeTimeUsed += d_perCallTimer.elapsed();
d_perCallTimer.set(0);
+ d_thisCallResourceUsed = 0;
}
bool ResourceManager::cumulativeLimitOn() const
{
- return d_resourceBudgetCumulative;
+ return d_resourceBudgetCumulative > 0;
}
bool ResourceManager::perCallLimitOn() const
{
- return d_timeBudgetPerCall || d_resourceBudgetPerCall;
+ return (d_timeBudgetPerCall > 0) || (d_resourceBudgetPerCall > 0);
}
bool ResourceManager::outOfResources() const
{
- // resource limiting not enabled
- if (d_resourceBudgetPerCall == 0 && d_resourceBudgetCumulative == 0)
- return false;
-
- return getResourceRemaining() == 0;
+ if (d_resourceBudgetPerCall > 0)
+ {
+ // Check if per-call resources are exhausted
+ if (d_thisCallResourceUsed >= d_resourceBudgetPerCall)
+ {
+ return true;
+ }
+ }
+ if (d_resourceBudgetCumulative > 0)
+ {
+ // Check if cumulative resources are exhausted
+ if (d_cumulativeResourceUsed >= d_resourceBudgetCumulative)
+ {
+ return true;
+ }
+ }
+ return false;
}
bool ResourceManager::outOfTime() const
{
if (d_timeBudgetPerCall == 0) return false;
-
return d_perCallTimer.expired();
}
-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";
d_on = on;
}
-ListenerCollection::Registration* ResourceManager::registerHardListener(
- Listener* listener)
-{
- return d_hardListeners.registerListener(listener);
-}
-
-ListenerCollection::Registration* ResourceManager::registerSoftListener(
+ListenerCollection::Registration* ResourceManager::registerListener(
Listener* listener)
{
- return d_softListeners.registerListener(listener);
+ return d_listeners.registerListener(listener);
}
} /* namespace CVC4 */
#include <sys/time.h>
+#include <chrono>
#include <cstddef>
#include <memory>
class StatisticsRegistry;
/**
- * A helper class to keep track of a time budget and signal
- * the PropEngine when the budget expires.
+ * This class implements a easy to use wall clock timer based on std::chrono.
*/
-class CVC4_PUBLIC Timer
+class CVC4_PUBLIC WallClockTimer
{
- public:
- /** Construct a Timer. */
- 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; }
+ /**
+ * The underlying clock that is used.
+ * std::chrono::system_clock represents wall clock time.
+ */
+ using clock = std::chrono::system_clock;
+ /** A time point of the clock we use. */
+ using time_point = std::chrono::time_point<clock>;
- /** Set a millisecond timer (0==off). */
+ public:
+ /** Checks whether this timer is active. */
+ bool on() const;
+ /**
+ * Activates this timer with a timeout in milliseconds.
+ * If millis is zero, the timer is deactivated.
+ */
void set(uint64_t millis);
- /** Return the milliseconds elapsed since last set() wall time. */
+ /** Returns the number of elapsed milliseconds since the last call to set().
+ */
uint64_t elapsed() const;
+ /** Checks whether the current timeout has expired. */
bool expired() const;
private:
- uint64_t d_ms;
- timeval d_wall_limit;
-}; /* class Timer */
+ /** The start of this timer. */
+ time_point d_start;
+ /** The point in time when this timer expires. */
+ time_point d_limit;
+};
+/**
+ * This class manages resource limits (cumulative or per call) and (per call)
+ * time limits. The available resources are listed in ResourceManager::Resource
+ * and their individual costs are configured via command line options.
+ */
class CVC4_PUBLIC ResourceManager
{
public:
+ /** Types of resources. */
enum class Resource
{
BitblastStep,
TheoryCheckStep,
};
+ /** Construst a resource manager. */
ResourceManager(StatisticsRegistry& statistics_registry, Options& options);
+ /** Default destructor. */
~ResourceManager();
+ /** Can not be copied. */
+ ResourceManager(const ResourceManager&) = delete;
+ /** Can not be moved. */
+ ResourceManager(ResourceManager&&) = delete;
+ /** Can not be copied. */
+ ResourceManager& operator=(const ResourceManager&) = delete;
+ /** Can not be moved. */
+ ResourceManager& operator=(ResourceManager&&) = delete;
+ /** Checks whether any limit is active. */
bool limitOn() const { return cumulativeLimitOn() || perCallLimitOn(); }
+ /** Checks whether any cumulative limit is active. */
bool cumulativeLimitOn() const;
+ /** Checks whether any per-call limit is active. */
bool perCallLimitOn() const;
+ /** Checks whether resources have been exhausted. */
bool outOfResources() const;
+ /** Checks whether time has been exhausted. */
bool outOfTime() const;
+ /** Checks whether any limit has been exhausted. */
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;
+ /** Retrieves amount of resources used overall. */
+ uint64_t getResourceUsage() const;
+ /** Retrieves time used over all calls. */
uint64_t getTimeUsage() const;
+ /** Retrieves the remaining number of cumulative resources. */
uint64_t getResourceRemaining() const;
+ /** Retrieves resource budget for this call. */
uint64_t getResourceBudgetForThisCall() { return d_thisCallResourceBudget; }
- // Throws an UnsafeInterruptException if there are no remaining resources.
+
+ /**
+ * Spends a given resources. Throws an UnsafeInterruptException if there are
+ * no remaining resources.
+ */
void spendResource(Resource r);
- void setHardLimit(bool value);
+ /** Sets the resource limit. */
void setResourceLimit(uint64_t units, bool cumulative = false);
+ /** Sets the time limit. */
void setTimeLimit(uint64_t millis);
-
+ /** Sets whether resource limitation is enabled. */
void enable(bool on);
/**
static uint64_t getFrequencyCount() { return s_resourceCount; }
/**
- * Registers a listener that is notified on a hard resource out.
+ * Registers a listener that is notified on a 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);
+ ListenerCollection::Registration* registerListener(Listener* listener);
private:
- Timer d_perCallTimer;
+ /** The per-call wall clock timer. */
+ WallClockTimer d_perCallTimer;
/** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */
uint64_t d_timeBudgetPerCall;
/** A user-imposed per-call resource budget. 0 = no limit. */
uint64_t d_resourceBudgetPerCall;
- /** The number of milliseconds used. */
+ /** The total number of milliseconds used. */
uint64_t d_cumulativeTimeUsed;
- /** The amount of resource used. */
+ /** The total amount of resources used. */
uint64_t d_cumulativeResourceUsed;
- /** The amount of resource used during this call. */
+ /** The amount of resources 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.
+ * The 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;
+ /** A flag indicating whether resource limitation is active. */
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;
+ /** Receives a notification on reaching a limit. */
+ ListenerCollection d_listeners;
void spendResource(unsigned amount);
projects / cvc5.git / commitdiff