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

merge with pull request #1557

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-04-07 17:22:49 -07:00
commit 2dc92e2b94
93 changed files with 526 additions and 548 deletions
Download patch file Download diff file Expand all files Collapse all files

40
src/util/hwf.cpp
View file

@ -91,8 +91,8 @@ hwf_manager::~hwf_manager()
{
}
uint64 RAW(double X) { uint64 tmp; memcpy(&tmp, &(X), sizeof(uint64)); return tmp; }
double DBL(uint64 X) { double tmp; memcpy(&tmp, &(X), sizeof(double)); return tmp; }
uint64_t RAW(double X) { uint64_t tmp; memcpy(&tmp, &(X), sizeof(uint64_t)); return tmp; }
double DBL(uint64_t X) { double tmp; memcpy(&tmp, &(X), sizeof(double)); return tmp; }
void hwf_manager::set(hwf & o, int value) {
o.value = (double) value;
@ -147,7 +147,7 @@ void hwf_manager::set(hwf & o, mpf_rounding_mode rm, mpq const & significand, mp
mpq sig;
m_mpq_manager.set(sig, significand);
int64 exp = m_mpz_manager.get_int64(exponent);
int64_t exp = m_mpz_manager.get_int64(exponent);
if (m_mpq_manager.is_zero(significand))
o.value = 0.0;
@ -160,17 +160,17 @@ void hwf_manager::set(hwf & o, mpf_rounding_mode rm, mpq const & significand, mp
}
hwf s; s.value = m_mpq_manager.get_double(sig);
uint64 r = (RAW(s.value) & 0x800FFFFFFFFFFFFFull) | ((exp + 1023) << 52);
uint64_t r = (RAW(s.value) & 0x800FFFFFFFFFFFFFull) | ((exp + 1023) << 52);
o.value = DBL(r);
}
}
void hwf_manager::set(hwf & o, bool sign, uint64 significand, int exponent) {
void hwf_manager::set(hwf & o, bool sign, uint64_t significand, int exponent) {
// Assumption: this represents (sign * -1) * (significand/2^sbits) * 2^exponent.
SASSERT(significand <= 0x000FFFFFFFFFFFFFull);
SASSERT(-1022 <= exponent && exponent <= 1023);
uint64 raw = (sign?0x8000000000000000ull:0);
raw |= (((uint64)exponent) + 1023) << 52;
uint64_t raw = (sign?0x8000000000000000ull:0);
raw |= (((uint64_t)exponent) + 1023) << 52;
raw |= significand;
memcpy(&o.value, &raw, sizeof(double));
}
@ -413,12 +413,12 @@ void hwf_manager::to_rational(hwf const & x, unsynch_mpq_manager & qm, mpq & o)
scoped_mpz n(qm), d(qm);
if (is_normal(x))
qm.set(n, (uint64)(sig(x) | 0x0010000000000000ull));
qm.set(n, (uint64_t)(sig(x) | 0x0010000000000000ull));
else
qm.set(n, sig(x));
if (sgn(x))
qm.neg(n);
qm.set(d, (uint64)0x0010000000000000ull);
qm.set(d, (uint64_t)0x0010000000000000ull);
int e = exp(x);
if (e >= 0)
qm.mul2k(n, (unsigned)e);
@ -428,7 +428,7 @@ void hwf_manager::to_rational(hwf const & x, unsynch_mpq_manager & qm, mpq & o)
}
bool hwf_manager::is_zero(hwf const & x) {
uint64 t = RAW(x.value) & 0x7FFFFFFFFFFFFFFFull;
uint64_t t = RAW(x.value) & 0x7FFFFFFFFFFFFFFFull;
return (t == 0x0ull);
// CMW: I tried, and these are slower:
// return (t != 0x0ull) ? false : true;
@ -483,12 +483,12 @@ bool hwf_manager::is_ninf(hwf const & x) {
}
bool hwf_manager::is_normal(hwf const & x) {
uint64 t = RAW(x.value) & 0x7FF0000000000000ull;
uint64_t t = RAW(x.value) & 0x7FF0000000000000ull;
return (t != 0x0ull && t != 0x7FF0000000000000ull);
}
bool hwf_manager::is_denormal(hwf const & x) {
uint64 t = RAW(x.value);
uint64_t t = RAW(x.value);
return ((t & 0x7FF0000000000000ull) == 0x0 &&
(t & 0x000FFFFFFFFFFFFFull) != 0x0);
}
@ -498,7 +498,7 @@ bool hwf_manager::is_regular(hwf const & x) {
// Note that +-0.0 and denormal numbers have exponent==0; these are regular.
// All normal numbers are also regular. What remains is +-Inf and NaN, they are
// not regular and they are the only numbers that have exponent 7FF.
uint64 e = RAW(x.value) & 0x7FF0000000000000ull; // the exponent
uint64_t e = RAW(x.value) & 0x7FF0000000000000ull; // the exponent
return (e != 0x7FF0000000000000ull);
}
@ -513,15 +513,15 @@ bool hwf_manager::is_int(hwf const & x) {
return false;
else
{
uint64 t = sig(x);
uint64_t t = sig(x);
unsigned shift = 52 - ((unsigned)e);
uint64 mask = (0x1ull << shift) - 1;
uint64_t mask = (0x1ull << shift) - 1;
return (t & mask) == 0;
}
}
void hwf_manager::mk_nzero(hwf & o) {
uint64 raw = 0x8000000000000000ull;
uint64_t raw = 0x8000000000000000ull;
o.value = DBL(raw);
}
@ -537,22 +537,22 @@ void hwf_manager::mk_zero(bool sign, hwf & o) {
}
void hwf_manager::mk_nan(hwf & o) {
uint64 raw = 0x7FF0000000000001ull;
uint64_t raw = 0x7FF0000000000001ull;
o.value = DBL(raw);
}
void hwf_manager::mk_inf(bool sign, hwf & o) {
uint64 raw = (sign) ? 0xFFF0000000000000ull : 0x7FF0000000000000ull;
uint64_t raw = (sign) ? 0xFFF0000000000000ull : 0x7FF0000000000000ull;
o.value = DBL(raw);
}
void hwf_manager::mk_pinf(hwf & o) {
uint64 raw = 0x7FF0000000000000ull;
uint64_t raw = 0x7FF0000000000000ull;
o.value = DBL(raw);
}
void hwf_manager::mk_ninf(hwf & o) {
uint64 raw = 0xFFF0000000000000ull;
uint64_t raw = 0xFFF0000000000000ull;
o.value = DBL(raw);
}