diff options
Diffstat (limited to 'src/util/stats.cpp')
-rw-r--r-- | src/util/stats.cpp | 48 |
1 files changed, 33 insertions, 15 deletions
diff --git a/src/util/stats.cpp b/src/util/stats.cpp index 474d8fa7a..709f80b04 100644 --- a/src/util/stats.cpp +++ b/src/util/stats.cpp @@ -31,6 +31,7 @@ using namespace CVC4; std::string Stat::s_delim(","); +std::string StatisticsRegistry::s_regDelim("::"); StatisticsRegistry* StatisticsRegistry::current() { return NodeManager::currentNM()->getStatisticsRegistry(); @@ -45,6 +46,14 @@ void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::registerStat() */ +void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) +{ +#ifdef CVC4_STATISTICS_ON + AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end()); + d_registeredStats.insert(s); +#endif /* CVC4_STATISTICS_ON */ +}/* StatisticsRegistry::registerStat_() */ + void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { #ifdef CVC4_STATISTICS_ON StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats; @@ -54,17 +63,33 @@ void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::unregisterStat() */ -void StatisticsRegistry::flushStatistics(std::ostream& out) { +void StatisticsRegistry::unregisterStat_(Stat* s) throw(AssertionException) { +#ifdef CVC4_STATISTICS_ON + AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end()); + d_registeredStats.erase(s); +#endif /* CVC4_STATISTICS_ON */ +}/* StatisticsRegistry::unregisterStat_() */ + +void StatisticsRegistry::flushInformation(std::ostream& out) const { #ifdef CVC4_STATISTICS_ON for(StatSet::iterator i = d_registeredStats.begin(); i != d_registeredStats.end(); ++i) { Stat* s = *i; + if(d_name != "") { + out << d_name << s_regDelim; + } s->flushStat(out); out << std::endl; } #endif /* CVC4_STATISTICS_ON */ -}/* StatisticsRegistry::flushStatistics() */ +}/* StatisticsRegistry::flushInformation() */ + +void StatisticsRegistry::flushStat(std::ostream &out) const {; +#ifdef CVC4_STATISTICS_ON + flushInformation(out); +#endif /* CVC4_STATISTICS_ON */ +} StatisticsRegistry::const_iterator StatisticsRegistry::begin() { return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.begin(); @@ -93,16 +118,9 @@ void TimerStat::stop() { }/* TimerStat::stop() */ RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) : - d_em(&em), d_stat(stat) { - ExprManagerScope ems(*d_em); - StatisticsRegistry::registerStat(d_stat); -}/* RegisterStatistic::RegisterStatistic(ExprManager&, Stat*) */ - -RegisterStatistic::~RegisterStatistic() { - if(d_em != NULL) { - ExprManagerScope ems(*d_em); - StatisticsRegistry::unregisterStat(d_stat); - } else { - StatisticsRegistry::unregisterStat(d_stat); - } -}/* RegisterStatistic::~RegisterStatistic() */ + d_reg(NULL), + d_stat(stat) { + ExprManagerScope ems(em); + d_reg = StatisticsRegistry::current(); + d_reg->registerStat_(d_stat); +} |