From: Gereon Kremer Date: Tue, 20 Apr 2021 22:10:17 +0000 (+0200) Subject: Add InferenceId as resources (#6339) X-Git-Tag: cvc5-1.0.0~1877 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=93fffd49080e29affbf9d5657046d57add929fa8;p=cvc5.git 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. --- 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()), - d_resourceManager(std::make_unique(*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(*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 d_resourceUnitsUsed; IntStat d_spendResourceCalls; - std::vector d_resourceSteps; + HistogramStat d_inferenceIdSteps; + HistogramStat d_resourceSteps; Statistics(StatisticsRegistry& stats); - - void bump(Resource r, uint64_t amount) - { - bump_impl(static_cast(r), amount, d_resourceSteps); - } - - private: - void bump_impl(std::size_t id, uint64_t amount, std::vector& stats) - { - Assert(stats.size() > id); - stats[id] += amount; - } }; ResourceManager::Statistics::Statistics(StatisticsRegistry& stats) : d_resourceUnitsUsed( stats.registerReference("resource::resourceUnitsUsed")), - d_spendResourceCalls(stats.registerInt("resource::spendResourceCalls")) + d_spendResourceCalls(stats.registerInt("resource::spendResourceCalls")), + d_inferenceIdSteps(stats.registerHistogram( + "resource::steps::inference-id")), + d_resourceSteps( + stats.registerHistogram("resource::steps::resource")) { - for (std::size_t id = 0; id <= resman_detail::ResourceMax; ++id) - { - Resource r = static_cast(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 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(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(name, weight, d_infidWeights)) + continue; if (setWeight(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(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(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 #include +#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(theory::InferenceId::UNKNOWN); +/** The upper bound of values from the Resource enum */ constexpr std::size_t ResourceMax = static_cast(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 d_infidWeights; + /** Weights for Resource resources */ std::array d_resourceWeights; struct Statistics; + /** The statistics object */ std::unique_ptr d_statistics; }; /* class ResourceManager */