Fix timer statistics to report correct time even on process abort.

diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index f6a27e20d898a5d62c0062692659b992d418eb3f..67cc3a53cfc84d48c2a46255a3f2387a59da854b 100644 (file)
--- 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 8ffc60d17ecac1a8fb06ab57bfcf6920c0ba915f..eb5245e2588055146afd33f58a145d072be97d46 100644 (file)
--- 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 */
 

diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h
index 3e3f6b9424bcf42fbf80e599ff573627552d4eee..1367a62c11eec97a76a3ded96dd6e4493a646092 100644 (file)
--- a/test/unit/util/stats_black.h
+++ b/test/unit/util/stats_black.h
@@ -94,7 +94,7 @@ public:
 
     sTimer.start();
     timespec zero = { 0, 0 };
-    TS_ASSERT_EQUALS(zero, sTimer.getData());
+    //TS_ASSERT_EQUALS(zero, sTimer.getData());
     sTimer.stop();
     TS_ASSERT_LESS_THAN(zero, sTimer.getData());
 #endif /* CVC4_STATISTICS_ON */