summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/lib/clock_gettime.c15
-rw-r--r--src/lib/clock_gettime.h22
-rw-r--r--src/parser/antlr_input.cpp9
-rw-r--r--src/util/statistics_registry.cpp8
-rw-r--r--src/util/statistics_registry.h23
5 files changed, 39 insertions, 38 deletions
diff --git a/src/lib/clock_gettime.c b/src/lib/clock_gettime.c
index e9d347438..054a8c112 100644
--- a/src/lib/clock_gettime.c
+++ b/src/lib/clock_gettime.c
@@ -36,7 +36,7 @@ extern "C" {
static double s_clockconv = 0.0;
-long clock_gettime(clockid_t which_clock, struct timespec *tp) {
+long clock_gettime(clockid_t which_clock, struct timespec* tp) {
if( s_clockconv == 0.0 ) {
mach_timebase_info_data_t tb;
kern_return_t err = mach_timebase_info(&tb);
@@ -66,8 +66,17 @@ long clock_gettime(clockid_t which_clock, struct timespec *tp) {
#else /* else we're __WIN32__ */
-long clock_gettime(clockid_t which_clock, struct timespec *tp) {
- // unsupported on Windows
+#include <time.h>
+#include <windows.h>
+
+long clock_gettime(clockid_t which_clock, struct timespec* tp) {
+ if(tp != NULL) {
+ FILETIME ft;
+ GetSystemTimeAsFileTime(&ft);
+ uint64_t nanos = ((((uint64_t)ft.dwHighDateTime) << 32) | ft.dwLowDateTime) * 100;
+ tp->tv_sec = nanos / 1000000000ul;
+ tp->tv_nsec = nanos % 1000000000ul;
+ }
return 0;
}
diff --git a/src/lib/clock_gettime.h b/src/lib/clock_gettime.h
index ea14f885c..6a8dd57ff 100644
--- a/src/lib/clock_gettime.h
+++ b/src/lib/clock_gettime.h
@@ -30,12 +30,27 @@
/* otherwise, we have to define it */
-#ifndef __WIN32__
+#ifdef __WIN32__
+
+#ifdef __cplusplus
+extern "C" {
+#endif /* __cplusplus */
+
+struct timespec {
+ uint64_t tv_sec;
+ int32_t tv_nsec;
+};/* struct timespec */
+
+#ifdef __cplusplus
+}/* extern "C" */
+#endif /* __cplusplus */
+
+#else /* ! __WIN32__ */
/* get timespec from <time.h> */
#include <time.h>
-#endif /* ! __WIN32__ */
+#endif /* __WIN32__ */
#ifdef __cplusplus
extern "C" {
@@ -50,7 +65,7 @@ typedef enum {
CLOCK_MONOTONIC_HR
} clockid_t;
-long clock_gettime(clockid_t which_clock, struct timespec *tp);
+long clock_gettime(clockid_t which_clock, struct timespec* tp);
#ifdef __cplusplus
}/* extern "C" */
@@ -58,4 +73,3 @@ long clock_gettime(clockid_t which_clock, struct timespec *tp);
#endif /* HAVE_CLOCK_GETTIME */
#endif /*__CVC4__LIB__CLOCK_GETTIME_H */
-
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 8987a7572..fbf2b8650 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -63,8 +63,13 @@ AntlrInputStream*
AntlrInputStream::newFileInputStream(const std::string& name,
bool useMmap)
throw (InputStreamException) {
+#ifdef _WIN32
+ if(useMmap) {
+ useMmap = false;
+ }
+#endif
pANTLR3_INPUT_STREAM input = NULL;
- if( useMmap ) {
+ if(useMmap) {
input = MemoryMappedInputBufferNew(name);
} else {
// libantlr3c v3.2 isn't source-compatible with v3.4
@@ -74,7 +79,7 @@ AntlrInputStream::newFileInputStream(const std::string& name,
input = antlr3FileStreamNew((pANTLR3_UINT8) name.c_str(), ANTLR3_ENC_8BIT);
#endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
}
- if( input == NULL ) {
+ if(input == NULL) {
throw InputStreamException("Couldn't open file: " + name);
}
return new AntlrInputStream( name, input );
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback