diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2012-12-18 15:33:43 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-24 16:22:42 -0500 |
| commit | 73760b3c213733fc98d67f9ceeb74d06b01a3777 (patch) | |
| tree | 8840f595428560499bc6739513ac3a1fbb2746ca /src/util/statistics_registry.cpp | |
| parent | 1435948e241d3134d44662b9476935fe635b4166 (diff) | |
Add win32 support (merge from mdeters/win32, with some cleanup).
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) : |