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/bv | |
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/bv')
-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 |
10 files changed, 19 insertions, 18 deletions
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 |