From b1dc477acf7eab8e40705ad20f910be91782cd02 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 10 Dec 2013 23:17:13 -0500
Subject: Fix timer statistics to report correct time even on process abort.

---
 src/util/statistics_registry.cpp | 22 ++++++++++++++++++++++
 src/util/statistics_registry.h   | 16 +++++++---------
 2 files changed, 29 insertions(+), 9 deletions(-)

(limited to 'src')

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 */
 
-- 
cgit v1.2.3