3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00

Merge branch 'unstable' of https://git01.codeplex.com/z3 into opt

This commit is contained in:
Nikolaj Bjorner 2014-01-27 11:19:19 -08:00
commit aff92f3ac1
16 changed files with 315 additions and 17 deletions

View file

@ -49,8 +49,11 @@ 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/OSX.
#ifdef __clang__
#undef USE_INTRINSICS
#else
#include <emmintrin.h>
#endif
hwf_manager::hwf_manager() :
m_mpz_manager(m_mpq_manager)

View file

@ -1400,6 +1400,10 @@ mpf_exp_t mpf_manager::mk_max_exp(unsigned ebits) {
return m_mpz_manager.get_int64(m_powers2.m1(ebits-1, false));
}
mpf_exp_t mpf_manager::unbias_exp(unsigned ebits, mpf_exp_t biased_exponent) {
return biased_exponent - m_mpz_manager.get_int64(m_powers2.m1(ebits - 1, false));
}
void mpf_manager::mk_nzero(unsigned ebits, unsigned sbits, mpf & o) {
o.sbits = sbits;
o.ebits = ebits;

View file

@ -182,6 +182,8 @@ public:
mpf_exp_t mk_max_exp(unsigned ebits);
mpf_exp_t mk_min_exp(unsigned ebits);
mpf_exp_t unbias_exp(unsigned ebits, mpf_exp_t biased_exponent);
/**
\brief Return the biggest k s.t. 2^k <= a.