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

1 files changed, 21 insertions, 1 deletions

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