diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-01 21:35:31 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-01 21:35:31 +0000 |
commit | 96d1c3daff7efdd2d853864fb820bc7cf413624e (patch) | |
tree | b995c98a2be18182d6cb52e81de5bf712b475f06 /src/util | |
parent | d0b49d588033ab8140bdf297c9cdf73b1088fe68 (diff) |
replacement implementation for clock_gettime() on mac os x, build portability (resolving mac os x issues), code cleanup, fix compiler warnings
Diffstat (limited to 'src/util')
-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 |