Fixes for Win32 (closes bugs 488 and 489)

* timer statistics now supported (closes bug 488)
* use of --mmap doesn't crash anymore (closes bug 489)

2 files changed, 2 insertions, 29 deletions

diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index 8f9f05031..b86b557e2 100644
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -17,9 +17,7 @@
 
 #include "util/statistics_registry.h"
 #include "expr/expr_manager.h"
-#ifndef __WIN32__
-#  include "lib/clock_gettime.h"
-#endif /* ! __WIN32__ */
+#include "lib/clock_gettime.h"
 #include "smt/smt_engine.h"
 
 #ifndef __BUILDING_STATISTICS_FOR_EXPORT
@@ -104,17 +102,14 @@ 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;
@@ -122,7 +117,6 @@ 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 32aa33bed..474abfea3 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -23,6 +23,7 @@
 
 #include "util/statistics.h"
 #include "util/exception.h"
+#include "lib/clock_gettime.h"
 
 #include <sstream>
 #include <iomanip>
@@ -612,8 +613,6 @@ public:
 
 };/* class StatisticsRegistry */
 
-#ifndef __WIN32__
-
 /****************************************************************************/
 /* Some utility functions for timespec                                    */
 /****************************************************************************/
@@ -769,26 +768,6 @@ 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
  * code block.  When constructed, it starts the timer.  When