diff options
Diffstat (limited to 'src/util/statistics_registry.cpp')
-rw-r--r-- | src/util/statistics_registry.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index b86b557e2..8f9f05031 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -17,7 +17,9 @@ #include "util/statistics_registry.h" #include "expr/expr_manager.h" -#include "lib/clock_gettime.h" +#ifndef __WIN32__ +# include "lib/clock_gettime.h" +#endif /* ! __WIN32__ */ #include "smt/smt_engine.h" #ifndef __BUILDING_STATISTICS_FOR_EXPORT @@ -102,14 +104,17 @@ void StatisticsRegistry::flushInformation(std::ostream &out) const { } void TimerStat::start() { +#ifndef __WIN32__ if(__CVC4_USE_STATISTICS) { CheckArgument(!d_running, *this, "timer already running"); clock_gettime(CLOCK_MONOTONIC, &d_start); d_running = true; } +#endif /* ! __WIN32__ */ }/* TimerStat::start() */ void TimerStat::stop() { +#ifndef __WIN32__ if(__CVC4_USE_STATISTICS) { CheckArgument(d_running, *this, "timer not running"); ::timespec end; @@ -117,6 +122,7 @@ void TimerStat::stop() { d_data += end - d_start; d_running = false; } +#endif /* ! __WIN32__ */ }/* TimerStat::stop() */ RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) : |