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.
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),
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;
/**
* Construct an Env with the given node manager.
*/
- Env(NodeManager* nm);
+ Env(NodeManager* nm, Options* opts);
/** Destruct the env. */
~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 */
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())),
// 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
#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"
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();
}
}
d_lemmaIdStats << id;
+ smt::currentResourceManager()->spendResource(id);
Trace("im") << "(lemma " << id << " " << tlem.getProven() << ")" << std::endl;
d_numCurrentLemmas++;
d_out.trustedLemma(tlem, p);
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
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)
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)))
{
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()])
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);
}
{
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());
#include <memory>
#include <vector>
+#include "theory/inference_id.h"
+
namespace cvc5 {
class Listener;
};
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
* 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,
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 */
projects / cvc5.git / commitdiff