diff options
Diffstat (limited to 'src/util/statistics_registry.cpp')
-rw-r--r-- | src/util/statistics_registry.cpp | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index f6a27e20d..67cc3a53c 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -119,6 +119,28 @@ void TimerStat::stop() { } }/* TimerStat::stop() */ +timespec TimerStat::getData() const { + ::timespec data = d_data; + if(__CVC4_USE_STATISTICS && d_running) { + ::timespec end; + clock_gettime(CLOCK_MONOTONIC, &end); + data += end - d_start; + } + return data; +} + +SExpr TimerStat::getValue() const { + ::timespec data = d_data; + if(__CVC4_USE_STATISTICS && d_running) { + ::timespec end; + clock_gettime(CLOCK_MONOTONIC, &end); + data += end - d_start; + } + std::stringstream ss; + ss << std::fixed << std::setprecision(8) << data; + return SExpr(Rational::fromDecimal(ss.str())); +}/* TimerStat::getValue() */ + RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) : d_reg(stats::getStatisticsRegistry(&em)), d_stat(stat) { |