diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-02-20 08:57:39 -0500 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-02-20 08:57:39 -0500 |
commit | 531ec6e52b75cd2f600a3fc781383e7539f2335a (patch) | |
tree | 2a78deb202f6886b6524f3852dc81f46c0eff36a /src/util | |
parent | 046fd1e02c1330b207bda99f8121b11562dd619c (diff) |
portfolio: add stat to track time spent waiting for interrupted threads to stop
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/statistics_registry.cpp | 4 | ||||
-rw-r--r-- | src/util/statistics_registry.h | 3 |
2 files changed, 7 insertions, 0 deletions
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index 67cc3a53c..61762b84d 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -119,6 +119,10 @@ void TimerStat::stop() { } }/* TimerStat::stop() */ +bool TimerStat::running() const { + return d_running; +}/* TimerStat::running() */ + timespec TimerStat::getData() const { ::timespec data = d_data; if(__CVC4_USE_STATISTICS && d_running) { diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index eb5245e25..bd33557d9 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -808,6 +808,9 @@ public: */ void stop(); + /** If the timer is currently running */ + bool running() const; + timespec getData() const; SExpr getValue() const; |