diff options
Diffstat (limited to 'src/util/stats.h')
-rw-r--r-- | src/util/stats.h | 32 |
1 files changed, 1 insertions, 31 deletions
diff --git a/src/util/stats.h b/src/util/stats.h index f8c10c79f..3a1b85506 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -29,6 +29,7 @@ #include <ctime> #include "util/Assert.h" +#include "lib/clock_gettime.h" namespace CVC4 { @@ -310,36 +311,6 @@ inline std::ostream& operator<<(std::ostream& os, const ::timespec& t) { } -#ifdef __APPLE__ - -class TimerStat : public BackedStat< ::timespec > { - bool d_running; - -public: - - TimerStat(const std::string& s) : - BackedStat< ::timespec >(s, ::timespec()), - d_running(false) { - } - - void start() { - if(__CVC4_USE_STATISTICS) { - AlwaysAssert(!d_running); - d_running = true; - } - } - - void stop() { - if(__CVC4_USE_STATISTICS) { - AlwaysAssert(d_running); - ++d_data.tv_sec; - d_running = false; - } - } -};/* class TimerStat */ - -#else /* __APPLE__ */ - class TimerStat : public BackedStat< ::timespec > { // strange: timespec isn't placed in 'std' namespace ?! ::timespec d_start; @@ -371,7 +342,6 @@ public: } };/* class TimerStat */ -#endif /* __APPLE__ */ #undef __CVC4_USE_STATISTICS |