diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2020-02-19 16:59:58 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-19 16:59:58 -0800 |
commit | 508ecb3007a2b6aa8b76b28dc8282247b5dba957 (patch) | |
tree | b80cab956e6b40b4cd783ceb78393006c09782b5 /src/theory | |
parent | 9705504973f6f85c6be4944c615984df7b614f67 (diff) |
resource manager: Add statistic for every resource. (#3772)
This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`).
Fixes #3751.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bitblast/bitblaster.h | 7 | ||||
-rw-r--r-- | src/theory/bv/bitblast/eager_bitblaster.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.cpp | 10 | ||||
-rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.h | 4 | ||||
-rw-r--r-- | src/theory/bv/bv_eager_solver.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_inequality.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 2 | ||||
-rw-r--r-- | src/theory/output_channel.h | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 2 | ||||
-rw-r--r-- | src/theory/rewriter.cpp | 2 | ||||
-rw-r--r-- | src/theory/sep/theory_sep.cpp | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 4 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 13 | ||||
-rw-r--r-- | src/theory/theory_test_utils.h | 3 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 2 |
20 files changed, 39 insertions, 34 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 6943c5546..8986e6894 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -83,7 +83,7 @@ void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) { } void TheoryArith::check(Effort effortLevel){ - getOutputChannel().spendResource(options::theoryCheckStep()); + getOutputChannel().spendResource(ResourceManager::Resource::TheoryCheckStep); d_internal->check(effortLevel); } diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index f2beec0b8..534a019c3 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1319,7 +1319,7 @@ void TheoryArrays::check(Effort e) { return; } - getOutputChannel().spendResource(options::theoryCheckStep()); + getOutputChannel().spendResource(ResourceManager::Resource::TheoryCheckStep); TimerStat::CodeTimer checkTimer(d_checkTime); diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index df7cc4f11..a16a8bbbf 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -109,11 +109,12 @@ class MinisatEmptyNotify : public prop::BVSatSolverNotify MinisatEmptyNotify() {} bool notify(prop::SatLiteral lit) override { return true; } void notify(prop::SatClause& clause) override {} - void spendResource(unsigned amount) override + void spendResource(ResourceManager::Resource r) override { - NodeManager::currentResourceManager()->spendResource(amount); + NodeManager::currentResourceManager()->spendResource(r); } - void safePoint(unsigned amount) override {} + + void safePoint(ResourceManager::Resource r) override {} }; // Bitblaster implementation diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index cd906769d..c4e3513bf 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -152,7 +152,7 @@ void EagerBitblaster::bbTerm(TNode node, Bits& bits) { return; } - d_bv->spendResource(options::bitblastStep()); + d_bv->spendResource(ResourceManager::Resource::BitblastStep); Debug("bitvector-bitblast") << "Bitblasting node " << node << "\n"; d_termBBStrategies[node.getKind()](node, bits, this); diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index 2018590f7..06afa126d 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -234,7 +234,7 @@ void TLazyBitblaster::bbTerm(TNode node, Bits& bits) { } Assert(node.getType().isBitVector()); - d_bv->spendResource(options::bitblastStep()); + d_bv->spendResource(ResourceManager::Resource::BitblastStep); Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n"; ++d_statistics.d_numTerms; @@ -426,14 +426,14 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) { } } -void TLazyBitblaster::MinisatNotify::spendResource(unsigned amount) +void TLazyBitblaster::MinisatNotify::spendResource(ResourceManager::Resource r) { - d_bv->spendResource(amount); + d_bv->spendResource(r); } -void TLazyBitblaster::MinisatNotify::safePoint(unsigned amount) +void TLazyBitblaster::MinisatNotify::safePoint(ResourceManager::Resource r) { - d_bv->d_out->safePoint(amount); + d_bv->d_out->safePoint(r); } EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h index ac5cd5c7f..3fe2398f1 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.h +++ b/src/theory/bv/bitblast/lazy_bitblaster.h @@ -120,8 +120,8 @@ class TLazyBitblaster : public TBitblaster<Node> bool notify(prop::SatLiteral lit) override; void notify(prop::SatClause& clause) override; - void spendResource(unsigned amount) override; - void safePoint(unsigned amount) override; + void spendResource(ResourceManager::Resource r) override; + void safePoint(ResourceManager::Resource r) override; }; TheoryBV* d_bv; diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index dd0458a70..d743a6023 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -70,7 +70,7 @@ bool EagerBitblastSolver::isInitialized() { } void EagerBitblastSolver::assertFormula(TNode formula) { - d_bv->spendResource(1); + d_bv->spendResource(ResourceManager::Resource::BvEagerAssertStep); Assert(isInitialized()); Debug("bitvector-eager") << "EagerBitblastSolver::assertFormula " << formula << "\n"; diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index 25fe7002e..b5e4b7c85 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -173,7 +173,7 @@ bool BitblastSolver::check(Theory::Effort e) // We need to ensure we are fully propagated, so propagate now if (d_useSatPropagation) { - d_bv->spendResource(1); + d_bv->spendResource(ResourceManager::Resource::BvPropagationStep); bool ok = d_bitblaster->propagate(); if (!ok) { diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index bf9bfa480..5d9c297f1 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -171,7 +171,7 @@ bool CoreSolver::decomposeFact(TNode fact) { bool CoreSolver::check(Theory::Effort e) { Trace("bitvector::core") << "CoreSolver::check \n"; - d_bv->spendResource(options::theoryCheckStep()); + d_bv->spendResource(ResourceManager::Resource::TheoryCheckStep); d_checkCalled = true; Assert(!d_bv->inConflict()); diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 332f96aa2..8a895e9eb 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -33,7 +33,7 @@ bool InequalitySolver::check(Theory::Effort e) { Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n"; TimerStat::CodeTimer inequalityTimer(d_statistics.d_solveTime); ++(d_statistics.d_numCallstoCheck); - d_bv->spendResource(options::theoryCheckStep()); + d_bv->spendResource(ResourceManager::Resource::TheoryCheckStep); bool ok = true; while (!done() && ok) { diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 48168d7d6..a35176a93 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -122,9 +122,9 @@ void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { } } -void TheoryBV::spendResource(unsigned amount) +void TheoryBV::spendResource(ResourceManager::Resource r) { - getOutputChannel().spendResource(amount); + getOutputChannel().spendResource(r); } TheoryBV::Statistics::Statistics(): diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 7ca98f2ea..196535a19 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -131,7 +131,7 @@ public: Statistics d_statistics; - void spendResource(unsigned amount); + void spendResource(ResourceManager::Resource r); /** * Return the uninterpreted function symbol corresponding to division-by-zero diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index bcbbfa274..dc5dfc388 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -82,7 +82,7 @@ class OutputChannel { * * @throws Interrupted if the theory can be safely interrupted. */ - virtual void safePoint(uint64_t amount) {} + virtual void safePoint(ResourceManager::Resource r) {} /** * Indicate a theory conflict has arisen. @@ -172,7 +172,7 @@ class OutputChannel { * long-running operations, they cannot rely on resource() to break * out of infinite or intractable computations. */ - virtual void spendResource(unsigned amount) {} + virtual void spendResource(ResourceManager::Resource r) {} /** * Handle user attribute. diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index aec648037..1d1eb9751 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -110,7 +110,7 @@ bool Instantiate::addInstantiation( Node q, std::vector<Node>& terms, bool mkRep, bool modEq, bool doVts) { // For resource-limiting (also does a time check). - d_qe->getOutputChannel().safePoint(options::quantifierStep()); + d_qe->getOutputChannel().safePoint(ResourceManager::Resource::QuantifierStep); Assert(!d_qe->inConflict()); Assert(terms.size() == q[0].getNumChildren()); Assert(d_term_db != nullptr); diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 7a99ed2d9..2a7c3ff0d 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -131,7 +131,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { if (hasSmtEngine && d_iterationCount % ResourceManager::getFrequencyCount() == 0) { - rm->spendResource(options::rewriteStep()); + rm->spendResource(ResourceManager::Resource::RewriteStep); d_iterationCount = 0; } diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 1392f8fab..b5fc1cbc9 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -308,7 +308,7 @@ void TheorySep::check(Effort e) { return; } - getOutputChannel().spendResource(options::theoryCheckStep()); + getOutputChannel().spendResource(ResourceManager::Resource::TheoryCheckStep); TimerStat::CodeTimer checkTimer(d_checkTime); Trace("sep-check") << "Sep::check(): " << e << endl; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index b43e55364..9cd226ba1 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -2313,9 +2313,9 @@ std::pair<bool, Node> TheoryEngine::entailmentCheck( } } -void TheoryEngine::spendResource(unsigned amount) +void TheoryEngine::spendResource(ResourceManager::Resource r) { - d_resourceManager->spendResource(amount); + d_resourceManager->spendResource(r); } void TheoryEngine::enableTheoryAlternative(const std::string& name){ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 5506b0120..0770efc7b 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -47,6 +47,7 @@ #include "theory/uf/equality_engine.h" #include "theory/valuation.h" #include "util/hash.h" +#include "util/resource_manager.h" #include "util/statistics_registry.h" #include "util/unsafe_interrupt_exception.h" @@ -281,8 +282,9 @@ class TheoryEngine { EngineOutputChannel(TheoryEngine* engine, theory::TheoryId theory) : d_engine(engine), d_statistics(theory), d_theory(theory) {} - void safePoint(uint64_t amount) override { - spendResource(amount); + void safePoint(ResourceManager::Resource r) override + { + spendResource(r); if (d_engine->d_interrupted) { throw theory::Interrupted(); } @@ -323,8 +325,9 @@ class TheoryEngine { d_engine->setIncomplete(d_theory); } - void spendResource(unsigned amount) override { - d_engine->spendResource(amount); + void spendResource(ResourceManager::Resource r) override + { + d_engine->spendResource(r); } void handleUserAttribute(const char* attr, theory::Theory* t) override { @@ -481,7 +484,7 @@ public: void interrupt(); /** "Spend" a resource during a search or preprocessing.*/ - void spendResource(unsigned amount); + void spendResource(ResourceManager::Resource r); /** * Adds a theory. Only one theory per TheoryId can be present, so if diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index dbb42f2bc..17b47d2d3 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -28,6 +28,7 @@ #include "theory/interrupted.h" #include "theory/output_channel.h" #include "util/proof.h" +#include "util/resource_manager.h" #include "util/unsafe_interrupt_exception.h" namespace CVC4 { @@ -67,7 +68,7 @@ public: TestOutputChannel() {} ~TestOutputChannel() override {} - void safePoint(uint64_t amount) override {} + void safePoint(ResourceManager::Resource r) override {} void conflict(TNode n, std::unique_ptr<Proof> pf) override { push(CONFLICT, n); diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 4d13bf3f2..e336d1630 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -117,7 +117,7 @@ void TheoryUF::check(Effort level) { if (done() && !fullEffort(level)) { return; } - getOutputChannel().spendResource(options::theoryCheckStep()); + getOutputChannel().spendResource(ResourceManager::Resource::TheoryCheckStep); TimerStat::CodeTimer checkTimer(d_checkTime); while (!done() && !d_conflict) |