mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

MSYS2 and cmake based compilation support for clang and gcc

Browse source
This commit is contained in:
Philipp Paulweber 2019-04-12 14:52:00 +02:00
parent a9faf6c4ab
commit 5708379ebc
No known key found for this signature in database
GPG key ID: DAF035D73D07C984
3 changed files with 20 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/shell/main.cpp
View file

@ -39,6 +39,10 @@ Revision History:
#include "util/file_path.h"
#include "shell/lp_frontend.h"
#if defined( _WINDOWS ) && defined( __MINGW32__ ) && ( defined( __GNUG__ ) || defined( __clang__ ) )
#include <crtdbg.h>
#endif
typedef enum { IN_UNSPECIFIED, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_LP, IN_Z3_LOG, IN_MPS } input_kind;
static std::string g_aux_input_file;

14
src/util/hwf.cpp
View file

@ -21,10 +21,12 @@ Revision History:
#include<sstream>
#ifdef _WINDOWS
#if defined(_MSC_VER)
#pragma float_control( except, on ) // exception semantics; this does _not_ mean that exceptions are enabled (we want them off!)
#pragma float_control( precise, on ) // precise semantics (no guessing!)
#pragma fp_contract(off) // contractions off (`contraction' means x*y+z is turned into a fused-mul-add).
#pragma fenv_access(on) // fpu environment sensitivity (needed to be allowed to make FPU mode changes).
#endif
#else
#include<fenv.h>
#endif
@ -267,6 +269,9 @@ void hwf_manager::fma(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf co
// IA64 (Itanium) will do it, if contractions are on.
o.value = x.value * y.value + z.value;
#else
#if defined( __MINGW32__ ) && ( defined( __GNUG__ ) || defined( __clang__ ) )
o.value = ::fma(x.value, y.value, z.value);
#else
#if defined(_WINDOWS)
#if _MSC_VER >= 1800
o.value = ::fma(x.value, y.value, z.value);
@ -283,6 +288,7 @@ void hwf_manager::fma(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf co
o.value = ::fma(x.value, y.value, z.value);
#endif
#endif
#endif
}
#ifdef _M_IA64
@ -306,7 +312,10 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o
// According to the Intel Architecture manual, the x87-instruction FRNDINT is the
// same in 32-bit and 64-bit mode. The _mm_round_* intrinsics are SSE4 extensions.
#ifdef _WINDOWS
#if defined(USE_INTRINSICS) && \
#if defined( __MINGW32__ ) && ( defined( __GNUG__ ) || defined( __clang__ ) )
o.value = nearbyint(x.value);
#else
#if defined(USE_INTRINSICS) && \
(defined(_WINDOWS) && (defined(__AVX__) || defined(_M_X64))) || \
(!defined(_WINDOWS) && defined(__SSE4_1__))
switch (rm) {
@ -320,7 +329,7 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o
default:
UNREACHABLE(); // Unknown rounding mode.
}
#else
#else
double xv = x.value;
double & ov = o.value;
@ -329,6 +338,7 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o
frndint
fstp ov // Store result away.
}
#endif
#endif
#else
// Linux, macOS.

4
src/util/warning.cpp
View file

@ -25,6 +25,10 @@ Revision History:
#include "util/vector.h"
#ifdef _WINDOWS
#if defined( __MINGW32__ ) && ( defined( __GNUG__ ) || defined( __clang__ ) )
#include <crtdbg.h>
#endif
#define VPRF vsprintf_s
void STD_CALL myInvalidParameterHandler(