mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-09 10:35:36 +00:00
Code Activity

Revert "mpz: use pointer tagging to save space (#8447)"

Browse source 
This reverts commit 2f4abe2ce6.
This commit is contained in:
Nikolaj Bjorner 2026-02-08 14:48:21 -08:00
parent a1cab09c1c
commit c269421942
2 changed files with 294 additions and 353 deletions
Download patch file Download diff file Expand all files Collapse all files

473
src/util/mpz.cpp
View file

File diff suppressed because it is too large Load diff

174
src/util/mpz.h
View file

@ -68,63 +68,27 @@ class mpz_cell {
/**
\brief Multi-precision integer.
m_value encodes either a small integer (if the least significant bit is 1)
or a pointer to a mpz_cell structure (if the least significant bit is 0).
The last 3 bits of pointers are always 0 due to alignment, so we use them
to store additional information:
- bit 0: small/large info (1 = small, 0 = large)
- bit 1: sign bit (0 = non-negative, 1 = negative)
- bit 2: owner info (0 = owned, 1 = external)
If m_kind == mpz_small, it is a small number and the value is stored in m_val.
If m_kind == mpz_large, the value is stored in m_ptr and m_ptr != nullptr.
m_val contains the sign (-1 negative, 1 positive)
under winodws, m_ptr points to a mpz_cell that store the value.
*/
enum mpz_kind { mpz_small = 0, mpz_large = 1};
enum mpz_owner { mpz_self = 0, mpz_ext = 1};
class mpz {
#ifndef _MP_GMP
typedef mpz_cell mpz_type;
#else
typedef mpz_t mpz_type;
#endif
private:
uintptr_t m_value = 1; // Default to small integer 0: (0 << 1) | 1 = 1
static constexpr uintptr_t SMALL_BIT = 0x1;
static constexpr uintptr_t SIGN_BIT = 0x2;
static constexpr uintptr_t OWNER_BIT = 0x4;
static constexpr uintptr_t MPZ_PTR_MASK = ~static_cast<uintptr_t>(0x7);
mpz_type * ptr() const {
SASSERT(!is_small());
return reinterpret_cast<mpz_type*>(m_value & MPZ_PTR_MASK);
}
void set_ptr(mpz_type* p, bool is_negative, bool is_external) {
SASSERT((reinterpret_cast<uintptr_t>(p) & 0x7) == 0); // Check alignment
m_value = reinterpret_cast<uintptr_t>(p);
if (is_negative)
m_value |= SIGN_BIT;
if (is_external)
m_value |= OWNER_BIT;
}
int get_sign() const {
SASSERT(!is_small());
return (m_value & SIGN_BIT) ? -1 : 1;
}
void set_sign(int s) {
SASSERT(!is_small());
if (s < 0)
m_value |= SIGN_BIT;
else
m_value &= ~SIGN_BIT;
}
bool is_external() const {
SASSERT(!is_small());
return (m_value & OWNER_BIT) != 0;
}
protected:
int m_val;
unsigned m_kind:1;
unsigned m_owner:1;
mpz_type * m_ptr;
friend class mpz_manager<true>;
friend class mpz_manager<false>;
friend class mpq_manager<true>;
@ -134,58 +98,42 @@ protected:
friend class mpbq_manager;
friend class mpz_stack;
public:
mpz(int v = 0) noexcept {
// Encode small integer: shift left by 1 and set bit 0
m_value = (static_cast<uintptr_t>(static_cast<intptr_t>(v)) << 1) | SMALL_BIT;
}
mpz(mpz_type* ptr) noexcept {
SASSERT(ptr);
set_ptr(ptr, false, true); // external pointer, non-negative
}
mpz(mpz && other) noexcept : mpz() {
swap(other);
}
mpz(int v = 0) noexcept : m_val(v), m_kind(mpz_small), m_owner(mpz_self), m_ptr(nullptr) {}
mpz(mpz_type* ptr) noexcept : m_val(0), m_kind(mpz_small), m_owner(mpz_ext), m_ptr(ptr) { SASSERT(ptr); }
mpz(mpz && other) noexcept : mpz() { swap(other); }
mpz& operator=(mpz const& other) = delete;
mpz& operator=(mpz &&other) noexcept {
swap(other);
return *this;
}
void swap(mpz & other) noexcept {
std::swap(m_value, other.m_value);
std::swap(m_val, other.m_val);
std::swap(m_ptr, other.m_ptr);
unsigned o = m_owner; m_owner = other.m_owner; other.m_owner = o;
unsigned k = m_kind; m_kind = other.m_kind; other.m_kind = k;
}
void set(int v) {
m_value = (static_cast<uintptr_t>(static_cast<intptr_t>(v)) << 1) | SMALL_BIT;
m_val = v;
m_kind = mpz_small;
}
inline bool is_small() const {
return (m_value & SMALL_BIT) != 0;
}
inline bool is_small() const { return m_kind == mpz_small; }
inline int value() const {
SASSERT(is_small());
// Decode small integer: shift right by 1 (arithmetic shift to preserve sign)
return static_cast<int>(static_cast<intptr_t>(m_value) >> 1);
}
inline int value() const { SASSERT(is_small()); return m_val; }
inline int sign() const {
SASSERT(!is_small());
return get_sign();
}
inline int sign() const { SASSERT(!is_small()); return m_val; }
};
#ifndef _MP_GMP
class mpz_stack : public mpz {
static const unsigned capacity = 8;
alignas(8) unsigned char m_bytes[sizeof(mpz_cell) + sizeof(digit_t) * capacity];
unsigned char m_bytes[sizeof(mpz_cell) + sizeof(digit_t) * capacity];
public:
mpz_stack():mpz(reinterpret_cast<mpz_cell*>(m_bytes)) {
ptr()->m_capacity = capacity;
m_ptr->m_capacity = capacity;
}
};
#else
@ -221,11 +169,16 @@ class mpz_manager {
// make sure that n is a big number and has capacity equal to at least c.
void allocate_if_needed(mpz & n, unsigned c) {
if (m_init_cell_capacity > c) c = m_init_cell_capacity;
if (n.is_small() || n.ptr() == nullptr || capacity(n) < c) {
if (n.m_ptr == nullptr || capacity(n) < c) {
deallocate(n);
n.set_ptr(allocate(c), false, false); // positive, owned
n.m_val = 1;
n.m_kind = mpz_large;
n.m_owner = mpz_self;
n.m_ptr = allocate(c);
}
else {
n.m_kind = mpz_large;
}
// else already has enough capacity, keep as large
}
void deallocate(bool is_heap, mpz_cell * ptr);
@ -277,16 +230,14 @@ class mpz_manager {
}
}
void clear(mpz& n) { if (!n.is_small() && n.ptr()) { mpz_clear(*n.ptr()); }}
void clear(mpz& n) { if (n.m_ptr) { mpz_clear(*n.m_ptr); }}
#endif
void deallocate(mpz& n) {
if (!n.is_small()) {
typename mpz::mpz_type* p = n.ptr();
if (p) {
deallocate(!n.is_external(), p);
n.set(0); // Reset to small zero
}
if (n.m_ptr) {
deallocate(n.m_owner == mpz_self, n.m_ptr);
n.m_ptr = nullptr;
n.m_kind = mpz_small;
}
}
@ -311,20 +262,11 @@ class mpz_manager {
#ifndef _MP_GMP
static unsigned capacity(mpz const & c) {
SASSERT(!c.is_small());
return c.ptr()->m_capacity;
}
static unsigned capacity(mpz const & c) { return c.m_ptr->m_capacity; }
static unsigned size(mpz const & c) {
SASSERT(!c.is_small());
return c.ptr()->m_size;
}
static unsigned size(mpz const & c) { return c.m_ptr->m_size; }
static digit_t * digits(mpz const & c) {
SASSERT(!c.is_small());
return c.ptr()->m_digits;
}
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) {
@ -340,7 +282,7 @@ class mpz_manager {
static uint64_t big_abs_to_uint64(mpz const & a) {
SASSERT(is_abs_uint64(a));
SASSERT(!is_small(a));
if (a.ptr()->m_size == 1)
if (a.m_ptr->m_size == 1)
return digits(a)[0];
if (sizeof(digit_t) == sizeof(uint64_t))
// 64-bit machine
@ -367,7 +309,7 @@ class mpz_manager {
if (is_small(a)) {
if (a.value() == INT_MIN) {
sign = -1;
cell = m_int_min.ptr();
cell = m_int_min.m_ptr;
}
else {
cell = reserve;
@ -384,7 +326,7 @@ class mpz_manager {
}
else {
sign = a.sign();
cell = a.ptr();
cell = a.m_ptr;
}
}
@ -401,10 +343,12 @@ class mpz_manager {
};
void mk_big(mpz & a) {
if (a.is_small()) {
a.set_ptr(allocate(), false, false); // positive, owned
if (a.m_ptr == nullptr) {
a.m_val = 0;
a.m_ptr = allocate();
a.m_owner = mpz_self;
}
// else already large with valid pointer
a.m_kind = mpz_large;
}
@ -504,17 +448,13 @@ public:
static bool is_zero(mpz const & a) { return sign(a) == 0; }
static int sign(mpz const & a) {
if (is_small(a)) {
int v = a.value();
return (v > 0) - (v < 0); // Returns -1, 0, or 1
}
#ifndef _MP_GMP
else {
return a.sign();
}
return a.m_val;
#else
if (is_small(a))
return a.m_val;
else
return mpz_sgn(*a.ptr());
return mpz_sgn(*a.m_ptr);
#endif
}
@ -685,7 +625,7 @@ public:
#else
if (is_small(a))
return a.value() == 1;
return mpz_cmp_si(*a.ptr(), 1) == 0;
return mpz_cmp_si(*a.m_ptr, 1) == 0;
#endif
}
@ -695,7 +635,7 @@ public:
#else
if (is_small(a))
return a.value() == -1;
return mpz_cmp_si(*a.ptr(), -1) == 0;
return mpz_cmp_si(*a.m_ptr, -1) == 0;
#endif
}
@ -773,7 +713,7 @@ public:
#ifndef _MP_GMP
return !(0x1 & digits(a)[0]);
#else
return mpz_even_p(*a.ptr());
return mpz_even_p(*a.m_ptr);
#endif
}