This PR simplifies how the resource manager interacts with the options. Instead of using some notification mechanism, the resource manager simply retrieves the options via options::xyz(). This simplifies the options handler, the resource manager interface and the options.
When instructed to do so by the API, the SmtEngine now overwrites the respective option instead of calling out to the resource manager.
smt_name = "tlimit"
category = "common"
long = "tlimit=MS"
- type = "unsigned long"
- handler = "limitHandler"
- read_only = true
- help = "enable time limiting of wall clock time (give milliseconds)"
+ type = "uint64_t"
+ help = "set time limit in milliseconds of wall clock time"
[[option]]
name = "perCallMillisecondLimit"
smt_name = "tlimit-per"
category = "common"
long = "tlimit-per=MS"
- type = "unsigned long"
- handler = "limitHandler"
- read_only = true
- help = "enable time limiting per query (give milliseconds)"
+ type = "uint64_t"
+ help = "set time limit per query in milliseconds"
[[option]]
name = "cumulativeResourceLimit"
smt_name = "rlimit"
category = "common"
long = "rlimit=N"
- type = "unsigned long"
- handler = "limitHandler"
- read_only = true
- help = "enable resource limiting (currently, roughly the number of SAT conflicts)"
+ type = "uint64_t"
+ help = "set resource limit"
[[option]]
name = "perCallResourceLimit"
smt_name = "reproducible-resource-limit"
category = "common"
long = "rlimit-per=N"
- type = "unsigned long"
- handler = "limitHandler"
- read_only = true
- help = "enable resource limiting per query"
+ type = "uint64_t"
+ help = "set resource limit per query"
# --rweight is used to override the default of one particular resource weight.
# It can be given multiple times to override multiple weights. When options are
namespace cvc5 {
namespace smt {
-OptionsManager::OptionsManager(Options* opts, ResourceManager* rm)
- : d_options(opts), d_resourceManager(rm)
+OptionsManager::OptionsManager(Options* opts) : d_options(opts)
{
// set options that must take effect immediately
if (opts->wasSetByUser(options::defaultExprDepth))
void OptionsManager::finishInit(LogicInfo& logic, bool isInternalSubsolver)
{
- // set up the timeouts and resource limits
- if ((*d_options)[options::perCallResourceLimit] != 0)
- {
- d_resourceManager->setResourceLimit(options::perCallResourceLimit(), false);
- }
- if ((*d_options)[options::cumulativeResourceLimit] != 0)
- {
- d_resourceManager->setResourceLimit(options::cumulativeResourceLimit(),
- true);
- }
- if ((*d_options)[options::perCallMillisecondLimit] != 0)
- {
- d_resourceManager->setTimeLimit(options::perCallMillisecondLimit());
- }
// ensure that our heuristics are properly set up
setDefaults(logic, isInternalSubsolver);
}
class OptionsManager : public OptionsListener
{
public:
- OptionsManager(Options* opts, ResourceManager* rm = nullptr);
+ OptionsManager(Options* opts);
~OptionsManager();
/**
* Called when a set option call is made on the options object associated
private:
/** Reference to the options object */
Options* d_options;
- /** Pointer to the resource manager */
- ResourceManager* d_resourceManager;
/** Manager for the memory of regular-output-channel. */
ManagedRegularOutputChannel d_managedRegularChannel;
/** Manager for the memory of diagnostic-output-channel. */
// non-null. This may throw an options exception.
d_env->setOptions(optr);
// set the options manager
- d_optm.reset(new smt::OptionsManager(&getOptions(), getResourceManager()));
+ d_optm.reset(new smt::OptionsManager(&getOptions()));
// listen to node manager events
getNodeManager()->subscribeEvents(d_snmListener.get());
// listen to resource out
d_smtSolver->interrupt();
}
-void SmtEngine::setResourceLimit(unsigned long units, bool cumulative)
+void SmtEngine::setResourceLimit(uint64_t units, bool cumulative)
{
- getResourceManager()->setResourceLimit(units, cumulative);
+ if (cumulative)
+ {
+ d_env->d_options.set(options::cumulativeResourceLimit__option_t(), units);
+ }
+ else
+ {
+ d_env->d_options.set(options::perCallResourceLimit__option_t(), units);
+ }
}
-void SmtEngine::setTimeLimit(unsigned long milis)
+void SmtEngine::setTimeLimit(uint64_t millis)
{
- getResourceManager()->setTimeLimit(milis);
+ d_env->d_options.set(options::perCallMillisecondLimit__option_t(), millis);
}
unsigned long SmtEngine::getResourceUsage() const
* resource limit for all remaining calls into the SmtEngine (true), or
* whether it's a per-call resource limit (false); the default is false
*/
- void setResourceLimit(unsigned long units, bool cumulative = false);
+ void setResourceLimit(uint64_t units, bool cumulative = false);
/**
* Set a per-call time limit for SmtEngine operations.
*
* @param millis the time limit in milliseconds, or 0 for no limit
*/
- void setTimeLimit(unsigned long millis);
+ void setTimeLimit(uint64_t millis);
/**
* Get the current resource usage count for this SmtEngine. This
ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options)
: d_perCallTimer(),
- d_timeBudgetPerCall(0),
- d_resourceBudgetCumulative(0),
- d_resourceBudgetPerCall(0),
d_cumulativeTimeUsed(0),
d_cumulativeResourceUsed(0),
d_thisCallResourceUsed(0),
- d_thisCallResourceBudget(0),
d_statistics(new ResourceManager::Statistics(stats))
{
d_statistics->d_resourceUnitsUsed.set(d_cumulativeResourceUsed);
ResourceManager::~ResourceManager() {}
-void ResourceManager::setResourceLimit(uint64_t units, bool cumulative)
-{
- 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;
- d_resourceBudgetPerCall = units;
- }
-}
-
-void ResourceManager::setTimeLimit(uint64_t millis)
-{
- Trace("limit") << "ResourceManager: setting per-call time limit to " << millis
- << " ms" << endl;
- d_timeBudgetPerCall = millis;
- // perCall timer will be set in beginCall
-}
-
uint64_t ResourceManager::getResourceUsage() const
{
return d_cumulativeResourceUsed;
uint64_t ResourceManager::getResourceRemaining() const
{
- if (d_resourceBudgetCumulative <= d_cumulativeResourceUsed) return 0;
- return d_resourceBudgetCumulative - d_cumulativeResourceUsed;
+ if (options::cumulativeResourceLimit() <= d_cumulativeResourceUsed) return 0;
+ return options::cumulativeResourceLimit() - d_cumulativeResourceUsed;
}
void ResourceManager::spendResource(uint64_t amount)
void ResourceManager::beginCall()
{
- d_perCallTimer.set(d_timeBudgetPerCall);
+ d_perCallTimer.set(options::perCallMillisecondLimit());
d_thisCallResourceUsed = 0;
- if (d_resourceBudgetCumulative > 0)
+ if (options::cumulativeResourceLimit() > 0)
{
// Compute remaining cumulative resource budget
d_thisCallResourceBudget =
- d_resourceBudgetCumulative - d_cumulativeResourceUsed;
+ options::cumulativeResourceLimit() - d_cumulativeResourceUsed;
}
- if (d_resourceBudgetPerCall > 0)
+ if (options::perCallResourceLimit() > 0)
{
// Check if per-call resource budget is even smaller
- if (d_resourceBudgetPerCall < d_thisCallResourceBudget)
+ if (options::perCallResourceLimit() < d_thisCallResourceBudget)
{
- d_thisCallResourceBudget = d_resourceBudgetPerCall;
+ d_thisCallResourceBudget = options::perCallResourceLimit();
}
}
}
bool ResourceManager::limitOn() const
{
- return (d_resourceBudgetCumulative > 0) || (d_timeBudgetPerCall > 0)
- || (d_resourceBudgetPerCall > 0);
+ return (options::cumulativeResourceLimit() > 0)
+ || (options::perCallMillisecondLimit() > 0)
+ || (options::perCallResourceLimit() > 0);
}
bool ResourceManager::outOfResources() const
{
- if (d_resourceBudgetPerCall > 0)
+ if (options::perCallResourceLimit() > 0)
{
// Check if per-call resources are exhausted
- if (d_thisCallResourceUsed >= d_resourceBudgetPerCall)
+ if (d_thisCallResourceUsed >= options::perCallResourceLimit())
{
return true;
}
}
- if (d_resourceBudgetCumulative > 0)
+ if (options::cumulativeResourceLimit() > 0)
{
// Check if cumulative resources are exhausted
- if (d_cumulativeResourceUsed >= d_resourceBudgetCumulative)
+ if (d_cumulativeResourceUsed >= options::cumulativeResourceLimit())
{
return true;
}
bool ResourceManager::outOfTime() const
{
- if (d_timeBudgetPerCall == 0) return false;
+ if (options::perCallMillisecondLimit() == 0) return false;
return d_perCallTimer.expired();
}
*/
void spendResource(Resource r);
- /** Sets the resource limit. */
- void setResourceLimit(uint64_t units, bool cumulative = false);
- /** Sets the time limit. */
- void setTimeLimit(uint64_t millis);
-
/**
* Resets perCall limits to mark the start of a new call,
* updates budget for current call and starts the timer
/** 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 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 total number of milliseconds used. */
uint64_t d_cumulativeTimeUsed;
/** The total amount of resources used. */
projects / cvc5.git / commitdiff