Fix statistics in AigBitblaster. (#6810)

Fixes #6788

diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
index 0907e80057c20eb9b77e7230937557619916f695..8fece032c07e7d7665e5c5206a72753f97223482 100644 (file)
--- 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 39ecbc12c93d8a05e86c582f8622eb77f4282cac..bf184585f75208531d4f19c4002dd1b2d43616a0 100644 (file)
--- 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;