From 1f61381172121b58821fcd9ed5cb3e8945d8c429 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 12 Oct 2012 00:07:16 -0700
Subject: [PATCH] trying to compile Z3 using cygwin/gcc...

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 configure.in         |  1 +
 lib/dimacs.cpp       |  2 ++
 lib/dl_context.h     |  4 ++++
 lib/hash.h           |  2 --
 lib/pdr_context.h    |  4 ++++
 lib/scoped_timer.cpp | 16 ++++++++++------
 lib/stopwatch.h      |  2 +-
 lib/trace.h          |  5 +++++
 8 files changed, 27 insertions(+), 9 deletions(-)

diff --git a/configure.in b/configure.in
index 2b403a421..fc0e55e1e 100644
--- a/configure.in
+++ b/configure.in
@@ -54,6 +54,7 @@ AS_IF([test "$host_os" = "Darwin"], [
    SLIBFLAGS="-shared -fopenmp"
    COMP_VERSIONS=
    STATIC_FLAGS=-static
+   CPPFLAGS+=" -D_CYGWIN"
 ],
 [
   AC_MSG_ERROR([Unknown host platform: $host_os])
diff --git a/lib/dimacs.cpp b/lib/dimacs.cpp
index 51b964dd3..3aa8591f9 100644
--- a/lib/dimacs.cpp
+++ b/lib/dimacs.cpp
@@ -17,6 +17,8 @@ Revision History:
 
 --*/
 #include"dimacs.h"
+#undef max
+#undef min
 #include"sat_solver.h"
 
 class stream_buffer {
diff --git a/lib/dl_context.h b/lib/dl_context.h
index 5db3c22b7..462e83ede 100644
--- a/lib/dl_context.h
+++ b/lib/dl_context.h
@@ -19,6 +19,10 @@ Revision History:
 #ifndef _DL_CONTEXT_H_
 #define _DL_CONTEXT_H_
 
+#ifdef _CYGWIN
+#undef min
+#undef max
+#endif
 #include"arith_decl_plugin.h"
 #include"front_end_params.h"
 #include"map.h"
diff --git a/lib/hash.h b/lib/hash.h
index 581f8e4d2..3c7e50a6c 100644
--- a/lib/hash.h
+++ b/lib/hash.h
@@ -21,11 +21,9 @@ Revision History:
 
 #include<algorithm>
 
-#ifndef _WINDOWS
 #ifndef __fallthrough
 #define __fallthrough
 #endif
-#endif
 
 #define mix(a,b,c)              \
 {                               \
diff --git a/lib/pdr_context.h b/lib/pdr_context.h
index e0ac2c53d..801ee6103 100644
--- a/lib/pdr_context.h
+++ b/lib/pdr_context.h
@@ -20,6 +20,10 @@ Revision History:
 #ifndef _PDR_CONTEXT_H_
 #define _PDR_CONTEXT_H_
 
+#ifdef _CYGWIN
+#undef min
+#undef max
+#endif
 #include <deque>
 #include "pdr_manager.h"
 #include "dl_base.h"
diff --git a/lib/scoped_timer.cpp b/lib/scoped_timer.cpp
index 008529308..c2583921d 100644
--- a/lib/scoped_timer.cpp
+++ b/lib/scoped_timer.cpp
@@ -18,7 +18,7 @@ Revision History:
 --*/
 #include"z3_exception.h"
 #include"z3_omp.h"
-#ifdef _WINDOWS
+#if defined(_WINDOWS) || defined(_CYGWIN)
 // Windows
 #include<windows.h>
 #elif defined(__APPLE__) && defined(__MACH__)
@@ -40,12 +40,16 @@ Revision History:
 #endif 
 
 #include"scoped_timer.h"
+#ifdef _CYGWIN
+#undef min
+#undef max
+#endif
 #include"util.h"
 #include<limits.h>
 
 struct scoped_timer::imp {
     event_handler *  m_eh;
-#ifdef _WINDOWS
+#if defined(_WINDOWS) || defined(_CYGWIN)
     HANDLE           m_timer;
     bool             m_first;
 #elif defined(__APPLE__) && defined(__MACH__)
@@ -62,7 +66,7 @@ struct scoped_timer::imp {
     timer_t         m_timerid;
 #endif
 
-#ifdef _WINDOWS
+#if defined(_WINDOWS) || defined(_CYGWIN)
     static void CALLBACK abort_proc(PVOID param, BOOLEAN timer_or_wait_fired) {
         imp * obj = static_cast<imp*>(param);
         if (obj->m_first) {
@@ -117,7 +121,7 @@ struct scoped_timer::imp {
 
     imp(unsigned ms, event_handler * eh):
         m_eh(eh) {
-#ifdef _WINDOWS
+#if defined(_WINDOWS) || defined(_CYGWIN)
         m_first = true;
         CreateTimerQueueTimer(&m_timer,			
                               NULL,				
@@ -167,7 +171,7 @@ struct scoped_timer::imp {
     }
 
     ~imp() {
-#ifdef _WINDOWS
+#if defined(_WINDOWS) || defined(_CYGWIN)
         DeleteTimerQueueTimer(NULL,
                               m_timer,
                               INVALID_HANDLE_VALUE);
@@ -191,7 +195,7 @@ struct scoped_timer::imp {
 
 };
 
-#ifdef _WINDOWS
+#if defined(_WINDOWS) || defined(_CYGWIN)
 #elif defined(__APPLE__) && defined(__MACH__)
 // Mac OS X
 #else
diff --git a/lib/stopwatch.h b/lib/stopwatch.h
index e27141924..661d3762b 100644
--- a/lib/stopwatch.h
+++ b/lib/stopwatch.h
@@ -20,7 +20,7 @@ Revision History:
 #ifndef _STOPWATCH_H_
 #define _STOPWATCH_H_
 
-#ifdef _WINDOWS
+#if defined(_WINDOWS) || defined(_CYGWIN)
 
 // Does this redefinition work?
 #define ARRAYSIZE_TEMP ARRAYSIZE
diff --git a/lib/trace.h b/lib/trace.h
index ac87dbb7a..941520f87 100644
--- a/lib/trace.h
+++ b/lib/trace.h
@@ -19,6 +19,11 @@ Revision History:
 
 #ifndef _TRACE_H_
 #define _TRACE_H_
+
+#ifdef _CYGWIN
+#undef max
+#undef min
+#endif
 #include<fstream>
 
 #ifdef _TRACE