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 | |
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.
-rw-r--r-- | src/smt/env.cpp | 20 | ||||
-rw-r--r-- | src/smt/env.h | 4 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 5 | ||||
-rw-r--r-- | src/theory/theory_inference_manager.cpp | 4 | ||||
-rw-r--r-- | src/util/resource_manager.cpp | 45 | ||||
-rw-r--r-- | src/util/resource_manager.h | 16 |
6 files changed, 54 insertions, 40 deletions
diff --git a/src/smt/env.cpp b/src/smt/env.cpp index d079682c5..9bb66f649 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -31,7 +31,7 @@ using namespace cvc5::smt; namespace cvc5 { -Env::Env(NodeManager* nm) +Env::Env(NodeManager* nm, Options* opts) : d_context(new context::Context()), d_userContext(new context::UserContext()), d_nodeManager(nm), @@ -40,22 +40,18 @@ Env::Env(NodeManager* nm) d_dumpManager(new DumpManager(d_userContext.get())), d_logic(), d_statisticsRegistry(std::make_unique<StatisticsRegistry>()), - d_resourceManager(std::make_unique<ResourceManager>(*d_statisticsRegistry, d_options)) + d_options(), + d_resourceManager() { -} - -Env::~Env() {} - -void Env::setOptions(Options* optr) -{ - if (optr != nullptr) + if (opts != nullptr) { - // if we provided a set of options, copy their values to the options - // owned by this Env. - d_options.copyValues(*optr); + d_options.copyValues(*opts); } + d_resourceManager = std::make_unique<ResourceManager>(*d_statisticsRegistry, d_options); } +Env::~Env() {} + void Env::setProofNodeManager(ProofNodeManager* pnm) { d_proofNodeManager = pnm; diff --git a/src/smt/env.h b/src/smt/env.h index 09e3238ac..209b6f3e7 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -60,7 +60,7 @@ class Env /** * Construct an Env with the given node manager. */ - Env(NodeManager* nm); + Env(NodeManager* nm, Options* opts); /** Destruct the env. */ ~Env(); @@ -116,8 +116,6 @@ class Env private: /* Private initialization ------------------------------------------------- */ - /** Set options, which makes a deep copy of optr if non-null */ - void setOptions(Options* optr = nullptr); /** Set the statistics registry */ void setStatisticsRegistry(StatisticsRegistry* statReg); /** Set proof node manager if it exists */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 122e69488..3e64c5d23 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -83,7 +83,7 @@ using namespace cvc5::theory; namespace cvc5 { SmtEngine::SmtEngine(NodeManager* nm, Options* optr) - : d_env(new Env(nm)), + : d_env(new Env(nm, optr)), d_state(new SmtEngineState(getContext(), getUserContext(), *this)), d_absValues(new AbstractValues(getNodeManager())), d_asserts(new Assertions(getUserContext(), *d_absValues.get())), @@ -120,9 +120,6 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr) // On the other hand, this hack breaks use cases where multiple SmtEngine // objects are created by the user. d_scope.reset(new SmtScope(this)); - // Set options in the environment, which makes a deep copy of optr if - // non-null. This may throw an options exception. - d_env->setOptions(optr); // set the options manager d_optm.reset(new smt::OptionsManager(&getOptions())); // listen to node manager events diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 3bc7351fe..ad988e534 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -15,6 +15,7 @@ #include "theory/theory_inference_manager.h" +#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/output_channel.h" #include "theory/rewriter.h" @@ -118,6 +119,7 @@ void TheoryInferenceManager::conflict(TNode conf, InferenceId id) void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id) { d_conflictIdStats << id; + smt::currentResourceManager()->spendResource(id); Trace("im") << "(conflict " << id << " " << tconf.getProven() << ")" << std::endl; d_theoryState.notifyInConflict(); @@ -250,6 +252,7 @@ bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem, } } d_lemmaIdStats << id; + smt::currentResourceManager()->spendResource(id); Trace("im") << "(lemma " << id << " " << tlem.getProven() << ")" << std::endl; d_numCurrentLemmas++; d_out.trustedLemma(tlem, p); @@ -370,6 +373,7 @@ bool TheoryInferenceManager::processInternalFact(TNode atom, ProofGenerator* pg) { d_factIdStats << iid; + smt::currentResourceManager()->spendResource(iid); Trace("im") << "(fact " << iid << " " << (pol ? Node(atom) : atom.notNode()) << ")" << std::endl; // make the node corresponding to the explanation 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 */ |