mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

Fix get_int64 and is_int64 methods in mpz. Fix INT64_MAX constant definition.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-04-08 14:25:25 -07:00
parent 1ef17cbe67
commit 03c1b24dea
3 changed files with 29 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/util/mpz.cpp
View file

@ -1299,9 +1299,9 @@ bool mpz_manager<SYNCH>::is_int64(mpz const & a) const {
if (is_small(a))
return true;
#ifndef _MP_GMP
if (!is_uint64(a))
if (!is_abs_uint64(a))
return false;
uint64 num = get_uint64(a);
uint64 num = big_abs_to_uint64(a);
uint64 msb = static_cast<uint64>(1) << 63;
uint64 msb_val = msb & num;
if (a.m_val >= 0) {
@ -1327,14 +1327,7 @@ uint64 mpz_manager<SYNCH>::get_uint64(mpz const & a) const {
return static_cast<uint64>(a.m_val);
#ifndef _MP_GMP
SASSERT(a.m_ptr->m_size > 0);
if (a.m_ptr->m_size == 1)
return digits(a)[0];
if (sizeof(digit_t) == sizeof(uint64))
// 64-bit machine
return digits(a)[0];
else
// 32-bit machine
return ((static_cast<uint64>(digits(a)[1]) << 32) | (static_cast<uint64>(digits(a)[0])));
return big_abs_to_uint64(a);
#else
// GMP version
if (sizeof(uint64) == sizeof(unsigned long)) {
@ -1359,7 +1352,7 @@ int64 mpz_manager<SYNCH>::get_int64(mpz const & a) const {
return static_cast<int64>(a.m_val);
#ifndef _MP_GMP
SASSERT(is_int64(a));
uint64 num = get_uint64(a);
uint64 num = big_abs_to_uint64(a);
if (a.m_val < 0) {
if (num != 0 && (num << 1) == 0)
return INT64_MIN;

24
src/util/mpz.h
View file

@ -211,6 +211,30 @@ class mpz_manager {
static digit_t * digits(mpz const & c) { return c.m_ptr->m_digits; }
// Return true if the absolute value fits in a UINT64
static bool is_abs_uint64(mpz const & a) {
if (is_small(a))
return true;
if (sizeof(digit_t) == sizeof(uint64))
return size(a) <= 1;
else
return size(a) <= 2;
}
// CAST the absolute value into a UINT64
static uint64 big_abs_to_uint64(mpz const & a) {
SASSERT(is_abs_uint64(a));
SASSERT(!is_small(a));
if (a.m_ptr->m_size == 1)
return digits(a)[0];
if (sizeof(digit_t) == sizeof(uint64))
// 64-bit machine
return digits(a)[0];
else
// 32-bit machine
return ((static_cast<uint64>(digits(a)[1]) << 32) | (static_cast<uint64>(digits(a)[0])));
}
template<int IDX>
void get_sign_cell(mpz const & a, int & sign, mpz_cell * & cell) {
if (is_small(a)) {

2
src/util/util.h
View file

@ -45,7 +45,7 @@ COMPILE_TIME_ASSERT(sizeof(int64) == 8);
#define INT64_MIN static_cast<int64>(0x8000000000000000ull)
#endif
#ifndef INT64_MAX
#define INT64_MAX static_cast<int64>(0x0fffffffffffffffull)
#define INT64_MAX static_cast<int64>(0x7fffffffffffffffull)
#endif
#ifndef UINT64_MAX
#define UINT64_MAX 0xffffffffffffffffull