diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-06-29 10:34:42 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-29 17:34:42 +0000 |
commit | c6ea00f789ef354e93c67740016709d4105fc3be (patch) | |
tree | e50bd796cbf01d332291de54318ef6f502ac4744 /src | |
parent | 877b75447b27da04d81ff3ee91eaad7bf00ea083 (diff) |
Fix statistics in AigBitblaster. (#6810)
Fixes #6788
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/bv/bitblast/aig_bitblaster.cpp | 28 | ||||
-rw-r--r-- | src/theory/bv/bitblast/aig_bitblaster.h | 1 |
2 files changed, 10 insertions, 19 deletions
diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp index 0907e8005..8fece032c 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.cpp +++ b/src/theory/bv/bitblast/aig_bitblaster.cpp @@ -473,25 +473,17 @@ Abc_Obj_t* AigBitblaster::getBBAtom(TNode atom) const { } AigBitblaster::Statistics::Statistics() - : d_numClauses("theory::bv::AigBitblaster::numClauses", 0) - , d_numVariables("theory::bv::AigBitblaster::numVariables", 0) - , d_simplificationTime("theory::bv::AigBitblaster::simplificationTime") - , d_cnfConversionTime("theory::bv::AigBitblaster::cnfConversionTime") - , d_solveTime("theory::bv::AigBitblaster::solveTime") + : d_numClauses(smtStatisticsRegistry().registerInt( + "theory::bv::AigBitblaster::numClauses")), + d_numVariables(smtStatisticsRegistry().registerInt( + "theory::bv::AigBitblaster::numVariables")), + d_simplificationTime(smtStatisticsRegistry().registerTimer( + "theory::bv::AigBitblaster::simplificationTime")), + d_cnfConversionTime(smtStatisticsRegistry().registerTimer( + "theory::bv::AigBitblaster::cnfConversionTime")), + d_solveTime(smtStatisticsRegistry().registerTimer( + "theory::bv::AigBitblaster::solveTime")) { - smtStatisticsRegistry()->registerStat(&d_numClauses); - smtStatisticsRegistry()->registerStat(&d_numVariables); - smtStatisticsRegistry()->registerStat(&d_simplificationTime); - smtStatisticsRegistry()->registerStat(&d_cnfConversionTime); - smtStatisticsRegistry()->registerStat(&d_solveTime); -} - -AigBitblaster::Statistics::~Statistics() { - smtStatisticsRegistry()->unregisterStat(&d_numClauses); - smtStatisticsRegistry()->unregisterStat(&d_numVariables); - smtStatisticsRegistry()->unregisterStat(&d_simplificationTime); - smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime); - smtStatisticsRegistry()->unregisterStat(&d_solveTime); } } // namespace bv diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h index 39ecbc12c..bf184585f 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.h +++ b/src/theory/bv/bitblast/aig_bitblaster.h @@ -99,7 +99,6 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*> TimerStat d_cnfConversionTime; TimerStat d_solveTime; Statistics(); - ~Statistics(); }; Statistics d_statistics; |