Improve platform detection, in particular MSVC ARM64

Z3Prover · Oct 24, 2019 · 3feb147 · 3feb147
1 parent 907ffde
commit 3feb147
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 7 deletions.
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
@@ -30,7 +30,7 @@ Revision History:
 #include "sat/sat_unit_walk.h"
 #include "sat/sat_ddfw.h"
 #include "sat/sat_prob.h"
-#ifdef _MSC_VER
+#if defined(_MSC_VER) && !defined(_M_ARM) && !defined(_M_ARM64)
 # include <xmmintrin.h>
 #endif
 
@@ -895,7 +895,9 @@ namespace sat {
 #if defined(__GNUC__) || defined(__clang__)
             __builtin_prefetch((const char*)((m_watches[l.index()].c_ptr())));
 #else
+    #if !defined(_M_ARM) && !defined(_M_ARM64)
             _mm_prefetch((const char*)((m_watches[l.index()].c_ptr())), _MM_HINT_T1);
+    #endif
 #endif
         }
 

diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp
@@ -48,7 +48,7 @@ Revision History:
 // clear to the compiler what instructions should be used. E.g., for sqrt(), the Windows compiler selects
 // the x87 FPU, even when /arch:SSE2 is on.
 // Luckily, these are kind of standardized, at least for Windows/Linux/macOS.
-#ifdef __clang__
+#if defined(__clang__) || defined(_M_ARM) && defined(_M_ARM64)
 #undef USE_INTRINSICS
 #endif
 
@@ -276,7 +276,7 @@ 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(_WINDOWS) && !defined(_M_ARM) && !defined(_M_ARM64)
 #if defined( __MINGW32__ ) && ( defined( __GNUG__ ) || defined( __clang__ ) )
     o.value = nearbyint(x.value);
 #else

diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
@@ -46,18 +46,17 @@ Revision History:
 #define LEHMER_GCD
 #endif
 
-#ifdef _WINDOWS
+#if defined(_WINDOWS) && !defined(_M_ARM) && !defined(_M_ARM64)
 // This is needed for _tzcnt_u32 and friends.
 #include <immintrin.h>
+#define _trailing_zeros32(X) _tzcnt_u32(X)
 #endif
 
 #if defined(__GNUC__)
 #define _trailing_zeros32(X) __builtin_ctz(X)
-#else
-#define _trailing_zeros32(X) _tzcnt_u32(X)
 #endif
 
-#if defined(__LP64__) || defined(_WIN64)
+#if (defined(__LP64__) || defined(_WIN64)) && !defined(_M_ARM) && !defined(_M_ARM64)
  #if defined(__GNUC__)
  #define _trailing_zeros64(X) __builtin_ctzll(X)
  #else
@@ -69,6 +68,11 @@ inline uint64_t _trailing_zeros64(uint64_t x) {
     for (; 0 == (x & 1) && r < 64; ++r, x >>= 1);
     return r;
 }
+inline uint32_t _trailing_zeros32(uint32_t x) {
+    uint32_t r = 0;
+    for (; 0 == (x & 1) && r < 32; ++r, x >>= 1);
+    return r;
+}
 #endif