diff options
Diffstat (limited to 'src/util/stats.cpp')
| -rw-r--r-- | src/util/stats.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/util/stats.cpp b/src/util/stats.cpp index 96e300197..7ac430da8 100644 --- a/src/util/stats.cpp +++ b/src/util/stats.cpp @@ -93,10 +93,18 @@ void StatisticsRegistry::flushStat(std::ostream &out) const {; #endif /* CVC4_STATISTICS_ON */ } +StatisticsRegistry::const_iterator StatisticsRegistry::begin_() const { + return d_registeredStats.begin(); +}/* StatisticsRegistry::begin() */ + StatisticsRegistry::const_iterator StatisticsRegistry::begin() { return current()->d_registeredStats.begin(); }/* StatisticsRegistry::begin() */ +StatisticsRegistry::const_iterator StatisticsRegistry::end_() const { + return d_registeredStats.end(); +}/* StatisticsRegistry::end() */ + StatisticsRegistry::const_iterator StatisticsRegistry::end() { return current()->d_registeredStats.end(); }/* StatisticsRegistry::end() */ |