diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-04-21 00:10:17 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-20 22:10:17 +0000 |
commit | 93fffd49080e29affbf9d5657046d57add929fa8 (patch) | |
tree | 62c0f2de79b61a1e1df13d9da136c062baa0ec80 /src/util | |
parent | cc8ce1bcdf8d6a4b508723063879e891a6cbd8c3 (diff) |
Add InferenceId as resources (#6339)
This PR extends the resource manager to consider theory::InferenceId a resource we can spend. This should give us a robust way to have the resource limiting cover a lot of theory reasoning. To make use of this, TheoryInferenceManager now spends these resources.
Also, it makes the ResourceManager properly use the options from the Env class.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/resource_manager.cpp | 45 | ||||
-rw-r--r-- | src/util/resource_manager.h | 16 |
2 files changed, 40 insertions, 21 deletions
diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index 40cc415be..f65f938b5 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -93,38 +93,29 @@ const char* toString(Resource r) default: return "?Resource?"; } } +std::ostream& operator<<(std::ostream& os, Resource r) +{ + return os << toString(r); +} struct ResourceManager::Statistics { ReferenceStat<uint64_t> d_resourceUnitsUsed; IntStat d_spendResourceCalls; - std::vector<IntStat> d_resourceSteps; + HistogramStat<theory::InferenceId> d_inferenceIdSteps; + HistogramStat<Resource> d_resourceSteps; Statistics(StatisticsRegistry& stats); - - void bump(Resource r, uint64_t amount) - { - bump_impl(static_cast<std::size_t>(r), amount, d_resourceSteps); - } - - private: - void bump_impl(std::size_t id, uint64_t amount, std::vector<IntStat>& stats) - { - Assert(stats.size() > id); - stats[id] += amount; - } }; ResourceManager::Statistics::Statistics(StatisticsRegistry& stats) : d_resourceUnitsUsed( stats.registerReference<uint64_t>("resource::resourceUnitsUsed")), - d_spendResourceCalls(stats.registerInt("resource::spendResourceCalls")) + d_spendResourceCalls(stats.registerInt("resource::spendResourceCalls")), + d_inferenceIdSteps(stats.registerHistogram<theory::InferenceId>( + "resource::steps::inference-id")), + d_resourceSteps( + stats.registerHistogram<Resource>("resource::steps::resource")) { - for (std::size_t id = 0; id <= resman_detail::ResourceMax; ++id) - { - Resource r = static_cast<Resource>(id); - d_resourceSteps.emplace_back( - stats.registerInt("resource::res::" + std::string(toString(r)))); - } } bool parseOption(const std::string& optarg, std::string& name, uint64_t& weight) @@ -145,6 +136,7 @@ bool parseOption(const std::string& optarg, std::string& name, uint64_t& weight) template <typename T, typename Weights> bool setWeight(const std::string& name, uint64_t weight, Weights& weights) { + using theory::toString; for (std::size_t i = 0; i < weights.size(); ++i) { if (name == toString(static_cast<T>(i))) @@ -167,6 +159,7 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options) { d_statistics->d_resourceUnitsUsed.set(d_cumulativeResourceUsed); + d_infidWeights.fill(1); d_resourceWeights.fill(1); for (const auto& opt : options[cvc5::options::resourceWeightHolder__option_t()]) @@ -175,6 +168,8 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options) uint64_t weight; if (parseOption(opt, name, weight)) { + if (setWeight<theory::InferenceId>(name, weight, d_infidWeights)) + continue; if (setWeight<Resource>(name, weight, d_resourceWeights)) continue; throw OptionException("Did not recognize resource type " + name); } @@ -225,10 +220,18 @@ void ResourceManager::spendResource(Resource r) { std::size_t i = static_cast<std::size_t>(r); Assert(d_resourceWeights.size() > i); - d_statistics->bump(r, d_resourceWeights[i]); + d_statistics->d_resourceSteps << r; spendResource(d_resourceWeights[i]); } +void ResourceManager::spendResource(theory::InferenceId iid) +{ + std::size_t i = static_cast<std::size_t>(iid); + Assert(d_infidWeights.size() > i); + d_statistics->d_inferenceIdSteps << iid; + spendResource(d_infidWeights[i]); +} + void ResourceManager::beginCall() { d_perCallTimer.set(options::perCallMillisecondLimit()); diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index 1ed7ee0d9..2590799fc 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -27,6 +27,8 @@ #include <memory> #include <vector> +#include "theory/inference_id.h" + namespace cvc5 { class Listener; @@ -93,8 +95,13 @@ enum class Resource }; const char* toString(Resource r); +std::ostream& operator<<(std::ostream& os, Resource r); namespace resman_detail { +/** The upper bound of values from the theory::InferenceId enum */ +constexpr std::size_t InferenceIdMax = + static_cast<std::size_t>(theory::InferenceId::UNKNOWN); +/** The upper bound of values from the Resource enum */ constexpr std::size_t ResourceMax = static_cast<std::size_t>(Resource::Unknown); }; // namespace resman_detail @@ -141,6 +148,11 @@ class ResourceManager * no remaining resources. */ void spendResource(Resource r); + /** + * Spends a given resource. Throws an UnsafeInterruptException if there are + * no remaining resources. + */ + void spendResource(theory::InferenceId iid); /** * Resets perCall limits to mark the start of a new call, @@ -183,9 +195,13 @@ class ResourceManager void spendResource(uint64_t amount); + /** Weights for InferenceId resources */ + std::array<uint64_t, resman_detail::InferenceIdMax + 1> d_infidWeights; + /** Weights for Resource resources */ std::array<uint64_t, resman_detail::ResourceMax + 1> d_resourceWeights; struct Statistics; + /** The statistics object */ std::unique_ptr<Statistics> d_statistics; }; /* class ResourceManager */ |