From 3564c3345d7fa53744661d815cbd463cc02567d7 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 15 Apr 2021 23:05:44 +0200 Subject: [PATCH] Avoid options listener for resource manager. (#6366) 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. --- src/options/smt_options.toml | 24 +++++--------- src/smt/options_manager.cpp | 17 +--------- src/smt/options_manager.h | 4 +-- src/smt/smt_engine.cpp | 17 +++++++--- src/smt/smt_engine.h | 4 +-- src/util/resource_manager.cpp | 61 +++++++++-------------------------- src/util/resource_manager.h | 12 ------- 7 files changed, 40 insertions(+), 99 deletions(-) diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index c6e42477b..83b83f3be 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -440,40 +440,32 @@ header = "options/smt_options.h" 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 diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp index 68ee629dc..c84854992 100644 --- a/src/smt/options_manager.cpp +++ b/src/smt/options_manager.cpp @@ -28,8 +28,7 @@ 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)) @@ -125,20 +124,6 @@ void OptionsManager::notifySetOption(const std::string& key) 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); } diff --git a/src/smt/options_manager.h b/src/smt/options_manager.h index 4705b4273..2201ceb40 100644 --- a/src/smt/options_manager.h +++ b/src/smt/options_manager.h @@ -42,7 +42,7 @@ namespace smt { 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 @@ -65,8 +65,6 @@ class OptionsManager : public OptionsListener 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. */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c877b7ce3..88cb078ae 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -123,7 +123,7 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr) // 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 @@ -1841,13 +1841,20 @@ void SmtEngine::interrupt() 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 diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 151b6106b..ff1a955ee 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -776,7 +776,7 @@ class CVC4_EXPORT SmtEngine * 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. @@ -801,7 +801,7 @@ class CVC4_EXPORT SmtEngine * * @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 diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index 461c523df..40cc415be 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -160,13 +160,9 @@ bool setWeight(const std::string& name, uint64_t weight, Weights& weights) 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); @@ -187,32 +183,6 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options) 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; @@ -222,8 +192,8 @@ uint64_t ResourceManager::getTimeUsage() const { return d_cumulativeTimeUsed; } 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) @@ -261,21 +231,21 @@ void ResourceManager::spendResource(Resource r) 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(); } } } @@ -289,24 +259,25 @@ void ResourceManager::endCall() 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; } @@ -316,7 +287,7 @@ bool ResourceManager::outOfResources() const bool ResourceManager::outOfTime() const { - if (d_timeBudgetPerCall == 0) return false; + if (options::perCallMillisecondLimit() == 0) return false; return d_perCallTimer.expired(); } diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index f43f5b429..1ed7ee0d9 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -142,11 +142,6 @@ class ResourceManager */ 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 @@ -169,13 +164,6 @@ class ResourceManager /** 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. */ -- 2.30.2