mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

remove suport for VS 2013

Browse source
This commit is contained in:
Nuno Lopes 2019-06-19 15:06:39 +01:00
parent 88d51d3377
commit e603bc1ea1
2 changed files with 0 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

35
src/util/hwf.cpp
View file

@ -255,46 +255,11 @@ void hwf_manager::div(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf &
#endif #endif
} }
#ifdef _M_IA64
#pragma fp_contract(on)
#endif
void hwf_manager::fma(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf const &z, hwf & o) { void hwf_manager::fma(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf const &z, hwf & o) {
// CMW: fused_mul_add is not available on most CPUs. As of 2012, only Itanium,
// Intel Sandybridge and AMD Bulldozers support that (via AVX).
set_rounding_mode(rm); set_rounding_mode(rm);
#ifdef _M_IA64
// 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); 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);
#else // Windows, older than VS 2013
#ifdef USE_INTRINSICS
_mm_store_sd(&o.value, _mm_fmadd_sd(_mm_set_sd(x.value), _mm_set_sd(y.value), _mm_set_sd(z.value)));
#else
// If all else fails, we are imprecise.
o.value = (x.value * y.value) + z;
#endif
#endif
#else
// Linux, macOS
o.value = ::fma(x.value, y.value, z.value);
#endif
#endif
#endif
} }
#ifdef _M_IA64
#pragma fp_contract(off)
#endif
void hwf_manager::sqrt(mpf_rounding_mode rm, hwf const & x, hwf & o) { void hwf_manager::sqrt(mpf_rounding_mode rm, hwf const & x, hwf & o) {
set_rounding_mode(rm); set_rounding_mode(rm);
#ifdef USE_INTRINSICS #ifdef USE_INTRINSICS

7
src/util/memory_manager.cpp
View file

@ -220,15 +220,8 @@ void * memory::allocate(char const* file, int line, char const* obj, size_t s) {
// when the local counter > SYNCH_THRESHOLD // when the local counter > SYNCH_THRESHOLD
#define SYNCH_THRESHOLD 100000 #define SYNCH_THRESHOLD 100000
#ifdef _WINDOWS
// This is VS2013 specific instead of Windows specific.
// It can go away with VS2017 builds
__declspec(thread) long long g_memory_thread_alloc_size = 0;
__declspec(thread) long long g_memory_thread_alloc_count = 0;
#else
thread_local long long g_memory_thread_alloc_size = 0; thread_local long long g_memory_thread_alloc_size = 0;
thread_local long long g_memory_thread_alloc_count = 0; thread_local long long g_memory_thread_alloc_count = 0;
#endif
static void synchronize_counters(bool allocating) { static void synchronize_counters(bool allocating) {
#ifdef PROFILE_MEMORY #ifdef PROFILE_MEMORY