mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 04:03:39 +00:00
trying to compile Z3 using cygwin/gcc...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
4dc834d5ee
commit
1f61381172
|
@ -54,6 +54,7 @@ AS_IF([test "$host_os" = "Darwin"], [
|
||||||
SLIBFLAGS="-shared -fopenmp"
|
SLIBFLAGS="-shared -fopenmp"
|
||||||
COMP_VERSIONS=
|
COMP_VERSIONS=
|
||||||
STATIC_FLAGS=-static
|
STATIC_FLAGS=-static
|
||||||
|
CPPFLAGS+=" -D_CYGWIN"
|
||||||
],
|
],
|
||||||
[
|
[
|
||||||
AC_MSG_ERROR([Unknown host platform: $host_os])
|
AC_MSG_ERROR([Unknown host platform: $host_os])
|
||||||
|
|
|
@ -17,6 +17,8 @@ Revision History:
|
||||||
|
|
||||||
--*/
|
--*/
|
||||||
#include"dimacs.h"
|
#include"dimacs.h"
|
||||||
|
#undef max
|
||||||
|
#undef min
|
||||||
#include"sat_solver.h"
|
#include"sat_solver.h"
|
||||||
|
|
||||||
class stream_buffer {
|
class stream_buffer {
|
||||||
|
|
|
@ -19,6 +19,10 @@ Revision History:
|
||||||
#ifndef _DL_CONTEXT_H_
|
#ifndef _DL_CONTEXT_H_
|
||||||
#define _DL_CONTEXT_H_
|
#define _DL_CONTEXT_H_
|
||||||
|
|
||||||
|
#ifdef _CYGWIN
|
||||||
|
#undef min
|
||||||
|
#undef max
|
||||||
|
#endif
|
||||||
#include"arith_decl_plugin.h"
|
#include"arith_decl_plugin.h"
|
||||||
#include"front_end_params.h"
|
#include"front_end_params.h"
|
||||||
#include"map.h"
|
#include"map.h"
|
||||||
|
|
|
@ -21,11 +21,9 @@ Revision History:
|
||||||
|
|
||||||
#include<algorithm>
|
#include<algorithm>
|
||||||
|
|
||||||
#ifndef _WINDOWS
|
|
||||||
#ifndef __fallthrough
|
#ifndef __fallthrough
|
||||||
#define __fallthrough
|
#define __fallthrough
|
||||||
#endif
|
#endif
|
||||||
#endif
|
|
||||||
|
|
||||||
#define mix(a,b,c) \
|
#define mix(a,b,c) \
|
||||||
{ \
|
{ \
|
||||||
|
|
|
@ -20,6 +20,10 @@ Revision History:
|
||||||
#ifndef _PDR_CONTEXT_H_
|
#ifndef _PDR_CONTEXT_H_
|
||||||
#define _PDR_CONTEXT_H_
|
#define _PDR_CONTEXT_H_
|
||||||
|
|
||||||
|
#ifdef _CYGWIN
|
||||||
|
#undef min
|
||||||
|
#undef max
|
||||||
|
#endif
|
||||||
#include <deque>
|
#include <deque>
|
||||||
#include "pdr_manager.h"
|
#include "pdr_manager.h"
|
||||||
#include "dl_base.h"
|
#include "dl_base.h"
|
||||||
|
|
|
@ -18,7 +18,7 @@ Revision History:
|
||||||
--*/
|
--*/
|
||||||
#include"z3_exception.h"
|
#include"z3_exception.h"
|
||||||
#include"z3_omp.h"
|
#include"z3_omp.h"
|
||||||
#ifdef _WINDOWS
|
#if defined(_WINDOWS) || defined(_CYGWIN)
|
||||||
// Windows
|
// Windows
|
||||||
#include<windows.h>
|
#include<windows.h>
|
||||||
#elif defined(__APPLE__) && defined(__MACH__)
|
#elif defined(__APPLE__) && defined(__MACH__)
|
||||||
|
@ -40,12 +40,16 @@ Revision History:
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
#include"scoped_timer.h"
|
#include"scoped_timer.h"
|
||||||
|
#ifdef _CYGWIN
|
||||||
|
#undef min
|
||||||
|
#undef max
|
||||||
|
#endif
|
||||||
#include"util.h"
|
#include"util.h"
|
||||||
#include<limits.h>
|
#include<limits.h>
|
||||||
|
|
||||||
struct scoped_timer::imp {
|
struct scoped_timer::imp {
|
||||||
event_handler * m_eh;
|
event_handler * m_eh;
|
||||||
#ifdef _WINDOWS
|
#if defined(_WINDOWS) || defined(_CYGWIN)
|
||||||
HANDLE m_timer;
|
HANDLE m_timer;
|
||||||
bool m_first;
|
bool m_first;
|
||||||
#elif defined(__APPLE__) && defined(__MACH__)
|
#elif defined(__APPLE__) && defined(__MACH__)
|
||||||
|
@ -62,7 +66,7 @@ struct scoped_timer::imp {
|
||||||
timer_t m_timerid;
|
timer_t m_timerid;
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
#ifdef _WINDOWS
|
#if defined(_WINDOWS) || defined(_CYGWIN)
|
||||||
static void CALLBACK abort_proc(PVOID param, BOOLEAN timer_or_wait_fired) {
|
static void CALLBACK abort_proc(PVOID param, BOOLEAN timer_or_wait_fired) {
|
||||||
imp * obj = static_cast<imp*>(param);
|
imp * obj = static_cast<imp*>(param);
|
||||||
if (obj->m_first) {
|
if (obj->m_first) {
|
||||||
|
@ -117,7 +121,7 @@ struct scoped_timer::imp {
|
||||||
|
|
||||||
imp(unsigned ms, event_handler * eh):
|
imp(unsigned ms, event_handler * eh):
|
||||||
m_eh(eh) {
|
m_eh(eh) {
|
||||||
#ifdef _WINDOWS
|
#if defined(_WINDOWS) || defined(_CYGWIN)
|
||||||
m_first = true;
|
m_first = true;
|
||||||
CreateTimerQueueTimer(&m_timer,
|
CreateTimerQueueTimer(&m_timer,
|
||||||
NULL,
|
NULL,
|
||||||
|
@ -167,7 +171,7 @@ struct scoped_timer::imp {
|
||||||
}
|
}
|
||||||
|
|
||||||
~imp() {
|
~imp() {
|
||||||
#ifdef _WINDOWS
|
#if defined(_WINDOWS) || defined(_CYGWIN)
|
||||||
DeleteTimerQueueTimer(NULL,
|
DeleteTimerQueueTimer(NULL,
|
||||||
m_timer,
|
m_timer,
|
||||||
INVALID_HANDLE_VALUE);
|
INVALID_HANDLE_VALUE);
|
||||||
|
@ -191,7 +195,7 @@ struct scoped_timer::imp {
|
||||||
|
|
||||||
};
|
};
|
||||||
|
|
||||||
#ifdef _WINDOWS
|
#if defined(_WINDOWS) || defined(_CYGWIN)
|
||||||
#elif defined(__APPLE__) && defined(__MACH__)
|
#elif defined(__APPLE__) && defined(__MACH__)
|
||||||
// Mac OS X
|
// Mac OS X
|
||||||
#else
|
#else
|
||||||
|
|
|
@ -20,7 +20,7 @@ Revision History:
|
||||||
#ifndef _STOPWATCH_H_
|
#ifndef _STOPWATCH_H_
|
||||||
#define _STOPWATCH_H_
|
#define _STOPWATCH_H_
|
||||||
|
|
||||||
#ifdef _WINDOWS
|
#if defined(_WINDOWS) || defined(_CYGWIN)
|
||||||
|
|
||||||
// Does this redefinition work?
|
// Does this redefinition work?
|
||||||
#define ARRAYSIZE_TEMP ARRAYSIZE
|
#define ARRAYSIZE_TEMP ARRAYSIZE
|
||||||
|
|
|
@ -19,6 +19,11 @@ Revision History:
|
||||||
|
|
||||||
#ifndef _TRACE_H_
|
#ifndef _TRACE_H_
|
||||||
#define _TRACE_H_
|
#define _TRACE_H_
|
||||||
|
|
||||||
|
#ifdef _CYGWIN
|
||||||
|
#undef max
|
||||||
|
#undef min
|
||||||
|
#endif
|
||||||
#include<fstream>
|
#include<fstream>
|
||||||
|
|
||||||
#ifdef _TRACE
|
#ifdef _TRACE
|
||||||
|
|
Loading…
Reference in a new issue