Add win32 support (merge from mdeters/win32, with some cleanup).

2 files changed, 28 insertions, 2 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) :
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 3bf990dbb..0a5450b8a 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -612,6 +612,8 @@ public:
 
 };/* class StatisticsRegistry */
 
+#ifndef __WIN32__
+
 /****************************************************************************/
 /* Some utility functions for timespec                                    */
 /****************************************************************************/
@@ -765,6 +767,25 @@ public:
 
 };/* class TimerStat */
 
+#else /* __WIN32__ */
+
+class CodeTimer;
+
+class TimerStat : public IntStat {
+public:
+
+  typedef CVC4::CodeTimer CodeTimer;
+
+  TimerStat(const std::string& name) :
+    IntStat(name, 0) {
+  }
+
+  void start();
+  void stop();
+
+};/* class TimerStat */
+
+#endif /* __WIN32__ */
 
 /**
  * Utility class to make it easier to call stop() at the end of a
@@ -788,7 +809,6 @@ public:
   }
 };/* class CodeTimer */
 
-
 /**
  * To use a statistic, you need to declare it, initialize it in your
  * constructor, register it in your constructor, and deregister it in