From 541e19463a0a5dc44dc97a494ca295aae296091e Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 28 Apr 2021 21:50:23 +0200 Subject: [PATCH] Refactor resource manager options (#6446) This PR refactors how the resource manager options are used. It moves options relevant for the resource manager into its own file (making the number of smt options a bit smaller) and uses the Options object directly instead of using the old static accessors. --- src/options/CMakeLists.txt | 1 + src/options/options.h | 2 +- src/options/options_public_functions.cpp | 7 +-- src/options/resource_manager_options.toml | 56 +++++++++++++++++++++++ src/options/smt_options.toml | 55 ---------------------- src/smt/smt_engine.cpp | 1 + src/util/resource_manager.cpp | 44 +++++++++--------- src/util/resource_manager.h | 4 +- 8 files changed, 89 insertions(+), 81 deletions(-) create mode 100644 src/options/resource_manager_options.toml diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index df632224c..38f68461b 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -55,6 +55,7 @@ set(options_toml_files proof_options.toml prop_options.toml quantifiers_options.toml + resource_manager_options.toml sep_options.toml sets_options.toml smt_options.toml diff --git a/src/options/options.h b/src/options/options.h index 4d8a979c6..324850c43 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -192,7 +192,7 @@ public: bool getStatsEveryQuery() const; bool getStrictParsing() const; int getTearDownIncremental() const; - unsigned long getCumulativeTimeLimit() const; + uint64_t getCumulativeTimeLimit() const; bool getVersion() const; const std::string& getForceLogicString() const; int getVerbosity() const; diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp index 6ad537240..8c55a19eb 100644 --- a/src/options/options_public_functions.cpp +++ b/src/options/options_public_functions.cpp @@ -16,8 +16,6 @@ * Options::wasSetByUser for different option types T. */ -#include "options.h" - #include #include #include @@ -25,6 +23,7 @@ #include "base/listener.h" #include "base/modal_exception.h" +#include "options.h" #include "options/base_options.h" #include "options/language.h" #include "options/main_options.h" @@ -33,6 +32,7 @@ #include "options/printer_modes.h" #include "options/printer_options.h" #include "options/quantifiers_options.h" +#include "options/resource_manager_options.h" #include "options/smt_options.h" #include "options/uf_options.h" @@ -141,7 +141,8 @@ int Options::getTearDownIncremental() const{ return (*this)[options::tearDownIncremental]; } -unsigned long Options::getCumulativeTimeLimit() const { +uint64_t Options::getCumulativeTimeLimit() const +{ return (*this)[options::cumulativeMillisecondLimit]; } diff --git a/src/options/resource_manager_options.toml b/src/options/resource_manager_options.toml new file mode 100644 index 000000000..05dd613f1 --- /dev/null +++ b/src/options/resource_manager_options.toml @@ -0,0 +1,56 @@ +id = "resource_manager" +name = "Resource Manager options" +header = "options/resource_manager_options.h" + +[[option]] + name = "cumulativeMillisecondLimit" + smt_name = "tlimit" + category = "common" + long = "tlimit=MS" + 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 = "uint64_t" + help = "set time limit per query in milliseconds" + +[[option]] + name = "cumulativeResourceLimit" + smt_name = "rlimit" + category = "common" + long = "rlimit=N" + type = "uint64_t" + help = "set resource limit" + +[[option]] + name = "perCallResourceLimit" + smt_name = "reproducible-resource-limit" + category = "common" + long = "rlimit-per=N" + 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 +# parsed, the resource manager might now be created yet, and it is not clear +# how an option handler would access it in a reasonable way. The option handler +# thus merely puts the data in another option that holds a vector of strings. +# This other option "resourceWeightHolder" has the sole purpose of storing +# this data in a way so that the resource manager can access it in its +# constructor. +[[option]] + category = "expert" + long = "rweight=VAL=N" + type = "std::string" + handler = "setResourceWeight" + read_only = true + help = "set a single resource weight" + +[[option]] + name = "resourceWeightHolder" + category = "undocumented" + type = "std::vector" diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index bb5cc1abe..24ae162da 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -444,60 +444,6 @@ header = "options/smt_options.h" read_only = true help = "set the diagnostic output channel of the solver" -[[option]] - name = "cumulativeMillisecondLimit" - smt_name = "tlimit" - category = "common" - long = "tlimit=MS" - 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 = "uint64_t" - help = "set time limit per query in milliseconds" - -[[option]] - name = "cumulativeResourceLimit" - smt_name = "rlimit" - category = "common" - long = "rlimit=N" - type = "uint64_t" - help = "set resource limit" - -[[option]] - name = "perCallResourceLimit" - smt_name = "reproducible-resource-limit" - category = "common" - long = "rlimit-per=N" - 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 -# parsed, the resource manager might now be created yet, and it is not clear -# how an option handler would access it in a reasonable way. The option handler -# thus merely puts the data in another option that holds a vector of strings. -# This other option "resourceWeightHolder" has the sole purpose of storing -# this data in a way so that the resource manager can access it in its -# constructor. -[[option]] - smt_name = "resourceWeight" - category = "expert" - long = "rweight=VAL=N" - type = "std::string" - handler = "setResourceWeight" - read_only = true - help = "set a single resource weight" - -[[option]] - name = "resourceWeightHolder" - category = "undocumented" - type = "std::vector" - [[option]] name = "forceNoLimitCpuWhileDump" category = "regular" @@ -516,7 +462,6 @@ header = "options/smt_options.h" read_only = true help = "Cross-theory rewrites" - [[option]] name = "solveBVAsInt" category = "undocumented" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 46e11af20..ef338fdfe 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -29,6 +29,7 @@ #include "options/option_exception.h" #include "options/printer_options.h" #include "options/proof_options.h" +#include "options/resource_manager_options.h" #include "options/smt_options.h" #include "options/theory_options.h" #include "printer/printer.h" diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index 872b23ac4..de9a32248 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -24,7 +24,7 @@ #include "base/output.h" #include "options/option_exception.h" #include "options/options.h" -#include "options/smt_options.h" +#include "options/resource_manager_options.h" #include "util/statistics_registry.h" using namespace std; @@ -151,8 +151,10 @@ bool setWeight(const std::string& name, uint64_t weight, Weights& weights) /*---------------------------------------------------------------------------*/ -ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options) - : d_perCallTimer(), +ResourceManager::ResourceManager(StatisticsRegistry& stats, + const Options& options) + : d_options(options), + d_perCallTimer(), d_cumulativeTimeUsed(0), d_cumulativeResourceUsed(0), d_thisCallResourceUsed(0), @@ -162,8 +164,7 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options) d_infidWeights.fill(1); d_resourceWeights.fill(1); - for (const auto& opt : - options[cvc5::options::resourceWeightHolder__option_t()]) + for (const auto& opt : d_options[options::resourceWeightHolder]) { std::string name; uint64_t weight; @@ -188,8 +189,9 @@ uint64_t ResourceManager::getTimeUsage() const { return d_cumulativeTimeUsed; } uint64_t ResourceManager::getResourceRemaining() const { - if (options::cumulativeResourceLimit() <= d_cumulativeResourceUsed) return 0; - return options::cumulativeResourceLimit() - d_cumulativeResourceUsed; + if (d_options[options::cumulativeResourceLimit] <= d_cumulativeResourceUsed) + return 0; + return d_options[options::cumulativeResourceLimit] - d_cumulativeResourceUsed; } void ResourceManager::spendResource(uint64_t amount) @@ -235,21 +237,21 @@ void ResourceManager::spendResource(theory::InferenceId iid) void ResourceManager::beginCall() { - d_perCallTimer.set(options::perCallMillisecondLimit()); + d_perCallTimer.set(d_options[options::perCallMillisecondLimit]); d_thisCallResourceUsed = 0; - if (options::cumulativeResourceLimit() > 0) + if (d_options[options::cumulativeResourceLimit] > 0) { // Compute remaining cumulative resource budget d_thisCallResourceBudget = - options::cumulativeResourceLimit() - d_cumulativeResourceUsed; + d_options[options::cumulativeResourceLimit] - d_cumulativeResourceUsed; } - if (options::perCallResourceLimit() > 0) + if (d_options[options::perCallResourceLimit] > 0) { // Check if per-call resource budget is even smaller - if (options::perCallResourceLimit() < d_thisCallResourceBudget) + if (d_options[options::perCallResourceLimit] < d_thisCallResourceBudget) { - d_thisCallResourceBudget = options::perCallResourceLimit(); + d_thisCallResourceBudget = d_options[options::perCallResourceLimit]; } } } @@ -263,25 +265,25 @@ void ResourceManager::endCall() bool ResourceManager::limitOn() const { - return (options::cumulativeResourceLimit() > 0) - || (options::perCallMillisecondLimit() > 0) - || (options::perCallResourceLimit() > 0); + return (d_options[options::cumulativeResourceLimit] > 0) + || (d_options[options::perCallMillisecondLimit] > 0) + || (d_options[options::perCallResourceLimit] > 0); } bool ResourceManager::outOfResources() const { - if (options::perCallResourceLimit() > 0) + if (d_options[options::perCallResourceLimit] > 0) { // Check if per-call resources are exhausted - if (d_thisCallResourceUsed >= options::perCallResourceLimit()) + if (d_thisCallResourceUsed >= d_options[options::perCallResourceLimit]) { return true; } } - if (options::cumulativeResourceLimit() > 0) + if (d_options[options::cumulativeResourceLimit] > 0) { // Check if cumulative resources are exhausted - if (d_cumulativeResourceUsed >= options::cumulativeResourceLimit()) + if (d_cumulativeResourceUsed >= d_options[options::cumulativeResourceLimit]) { return true; } @@ -291,7 +293,7 @@ bool ResourceManager::outOfResources() const bool ResourceManager::outOfTime() const { - if (options::perCallMillisecondLimit() == 0) return false; + if (d_options[options::perCallMillisecondLimit] == 0) return false; return d_perCallTimer.expired(); } diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index 2590799fc..3dd337058 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -114,7 +114,8 @@ class ResourceManager { public: /** Construct a resource manager. */ - ResourceManager(StatisticsRegistry& statistics_registry, Options& options); + ResourceManager(StatisticsRegistry& statistics_registry, + const Options& options); /** Default destructor. */ ~ResourceManager(); /** Can not be copied. */ @@ -173,6 +174,7 @@ class ResourceManager void registerListener(Listener* listener); private: + const Options& d_options; /** The per-call wall clock timer. */ WallClockTimer d_perCallTimer; -- 2.30.2