diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/stats.cpp | 24 | ||||
-rw-r--r-- | src/util/stats.h | 3 |
2 files changed, 19 insertions, 8 deletions
diff --git a/src/util/stats.cpp b/src/util/stats.cpp index b030495c5..96e300197 100644 --- a/src/util/stats.cpp +++ b/src/util/stats.cpp @@ -20,7 +20,10 @@ #include "util/stats.h" #include "expr/node_manager.h" #include "expr/expr_manager_scope.h" +#include "expr/expr_manager.h" #include "lib/clock_gettime.h" +#include "smt/smt_engine_scope.h" +#include "smt/smt_engine.h" #ifdef CVC4_STATISTICS_ON # define __CVC4_USE_STATISTICS true @@ -34,12 +37,12 @@ std::string Stat::s_delim(","); std::string StatisticsRegistry::s_regDelim("::"); StatisticsRegistry* StatisticsRegistry::current() { - return NodeManager::currentNM()->getStatisticsRegistry(); + return smt::currentSmtEngine()->getStatisticsRegistry(); } void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { #ifdef CVC4_STATISTICS_ON - StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats; + StatSet& registeredStats = current()->d_registeredStats; AlwaysAssert(registeredStats.find(s) == registeredStats.end(), "Statistic `%s' was already registered with this registry.", s->getName().c_str()); registeredStats.insert(s); @@ -55,7 +58,7 @@ void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) { void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { #ifdef CVC4_STATISTICS_ON - StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats; + StatSet& registeredStats = current()->d_registeredStats; AlwaysAssert(registeredStats.find(s) != registeredStats.end(), "Statistic `%s' was not registered with this registry.", s->getName().c_str()); registeredStats.erase(s); @@ -91,11 +94,11 @@ void StatisticsRegistry::flushStat(std::ostream &out) const {; } StatisticsRegistry::const_iterator StatisticsRegistry::begin() { - return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.begin(); + return current()->d_registeredStats.begin(); }/* StatisticsRegistry::begin() */ StatisticsRegistry::const_iterator StatisticsRegistry::end() { - return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.end(); + return current()->d_registeredStats.end(); }/* StatisticsRegistry::end() */ void TimerStat::start() { @@ -117,9 +120,14 @@ void TimerStat::stop() { }/* TimerStat::stop() */ RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) : - d_reg(NULL), + d_reg(em.getStatisticsRegistry()), d_stat(stat) { - ExprManagerScope ems(em); - d_reg = StatisticsRegistry::current(); d_reg->registerStat_(d_stat); } + +RegisterStatistic::RegisterStatistic(SmtEngine& smt, Stat* stat) : + d_reg(smt.getStatisticsRegistry()), + d_stat(stat) { + d_reg->registerStat_(d_stat); +} + diff --git a/src/util/stats.h b/src/util/stats.h index 63e732305..aabf04dc0 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -43,6 +43,7 @@ namespace CVC4 { #endif class ExprManager; +class SmtEngine; class CVC4_PUBLIC Stat; @@ -803,6 +804,8 @@ public: RegisterStatistic(ExprManager& em, Stat* stat); + RegisterStatistic(SmtEngine& smt, Stat* stat); + ~RegisterStatistic() { d_reg->unregisterStat_(d_stat); } |