diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-10 23:17:13 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-10 23:25:29 -0500 |
commit | b1dc477acf7eab8e40705ad20f910be91782cd02 (patch) | |
tree | d95d543c3f65e08971fc816ae63c187f998d382a /src | |
parent | 027d650400c1e5e6d0b942ccb42783ee7b5e9060 (diff) |
Fix timer statistics to report correct time even on process abort.
Diffstat (limited to 'src')
-rw-r--r-- | src/util/statistics_registry.cpp | 22 | ||||
-rw-r--r-- | src/util/statistics_registry.h | 16 |
2 files changed, 29 insertions, 9 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) { diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 8ffc60d17..eb5245e25 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -179,7 +179,7 @@ public: } /** Get the value of the statistic. */ - virtual const T& getData() const = 0; + virtual T getData() const = 0; /** Flush the value of the statistic to the given output stream. */ void flushInformation(std::ostream& out) const { @@ -270,7 +270,7 @@ public: } /** Get the value of the referenced data cell. */ - const T& getData() const { + T getData() const { return *d_data; } @@ -312,7 +312,7 @@ public: } /** Get the underlying data value. */ - const T& getData() const { + T getData() const { return d_data; } @@ -354,7 +354,7 @@ public: } /** Get the data of the underlying (wrapped) statistic. */ - const T& getData() const { + T getData() const { return d_stat.getData(); } @@ -808,11 +808,9 @@ public: */ void stop(); - SExpr getValue() const { - std::stringstream ss; - ss << std::fixed << std::setprecision(8) << d_data; - return SExpr(Rational::fromDecimal(ss.str())); - } + timespec getData() const; + + SExpr getValue() const; };/* class TimerStat */ |