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/bitblast | |
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/bitblast')
-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 |
4 files changed, 12 insertions, 11 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; |