mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-18 22:54:21 +00:00
Code Activity

Refactor decompose function and consolidate value()/value64() into single value() returning int64_t

Browse source 
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-13 14:10:48 +00:00
parent ded37fa012
commit a4e58b1547
2 changed files with 31 additions and 52 deletions
Download patch file Download diff file Expand all files Collapse all files

70
src/util/mpz.cpp
View file

@ -705,7 +705,7 @@ template<bool SYNCH>
void mpz_manager<SYNCH>::neg(mpz & a) { void mpz_manager<SYNCH>::neg(mpz & a) {
STRACE(mpz, tout << "[mpz] 0 - " << to_string(a) << " == ";); STRACE(mpz, tout << "[mpz] 0 - " << to_string(a) << " == ";);
if (is_small(a)) { if (is_small(a)) {
int64_t v = a.value64(); int64_t v = a.value();
if (v == mpz::SMALL_INT_MIN) { if (v == mpz::SMALL_INT_MIN) {
// neg(SMALL_INT_MIN) overflows small range // neg(SMALL_INT_MIN) overflows small range
set_big_i64(a, -v); set_big_i64(a, -v);
@ -728,7 +728,7 @@ void mpz_manager<SYNCH>::neg(mpz & a) {
template<bool SYNCH> template<bool SYNCH>
void mpz_manager<SYNCH>::abs(mpz & a) { void mpz_manager<SYNCH>::abs(mpz & a) {
if (is_small(a)) { if (is_small(a)) {
int64_t v = a.value64(); int64_t v = a.value();
if (v < 0) { if (v < 0) {
if (v == mpz::SMALL_INT_MIN) { if (v == mpz::SMALL_INT_MIN) {
// abs(SMALL_INT_MIN) overflows small range // abs(SMALL_INT_MIN) overflows small range
@ -941,8 +941,8 @@ template<bool SYNCH>
void mpz_manager<SYNCH>::gcd(mpz const & a, mpz const & b, mpz & c) { void mpz_manager<SYNCH>::gcd(mpz const & a, mpz const & b, mpz & c) {
static_assert(sizeof(mpz) <= 16, "mpz size overflow"); static_assert(sizeof(mpz) <= 16, "mpz size overflow");
if (is_small(a) && is_small(b)) { if (is_small(a) && is_small(b)) {
int64_t _a = a.value64(); int64_t _a = a.value();
int64_t _b = b.value64(); int64_t _b = b.value();
// Check if absolute values fit in uint64 (they always do for small integers) // Check if absolute values fit in uint64 (they always do for small integers)
// and won't overflow when negating // and won't overflow when negating
if (_a != mpz::SMALL_INT_MIN && _b != mpz::SMALL_INT_MIN) { if (_a != mpz::SMALL_INT_MIN && _b != mpz::SMALL_INT_MIN) {
@ -1004,7 +1004,7 @@ void mpz_manager<SYNCH>::gcd(mpz const & a, mpz const & b, mpz & c) {
// reset least significant bit // reset least significant bit
if (is_small(v)) if (is_small(v))
v.set64(v.value64() & ~1); v.set64(v.value() & ~1);
else else
v.ptr()->m_digits[0] &= ~static_cast<digit_t>(1); v.ptr()->m_digits[0] &= ~static_cast<digit_t>(1);
k_v = power_of_two_multiple(v); k_v = power_of_two_multiple(v);
@ -1121,7 +1121,7 @@ void mpz_manager<SYNCH>::gcd(mpz const & a, mpz const & b, mpz & c) {
SASSERT(ge(a1, b1)); SASSERT(ge(a1, b1));
if (is_small(b1)) { if (is_small(b1)) {
if (is_small(a1)) { if (is_small(a1)) {
uint64_t r = u64_gcd(static_cast<uint64_t>(a1.value64()), static_cast<uint64_t>(b1.value64())); uint64_t r = u64_gcd(static_cast<uint64_t>(a1.value()), static_cast<uint64_t>(b1.value()));
set(c, r); set(c, r);
break; break;
} }
@ -1401,7 +1401,7 @@ void mpz_manager<SYNCH>::bitwise_or(mpz const & a, mpz const & b, mpz & c) {
SASSERT(is_nonneg(b)); SASSERT(is_nonneg(b));
TRACE(mpz, tout << "is_small(a): " << is_small(a) << ", is_small(b): " << is_small(b) << "\n";); TRACE(mpz, tout << "is_small(a): " << is_small(a) << ", is_small(b): " << is_small(b) << "\n";);
if (is_small(a) && is_small(b)) { if (is_small(a) && is_small(b)) {
c.set64(a.value64() | b.value64()); c.set64(a.value() | b.value());
} }
else { else {
#ifndef _MP_GMP #ifndef _MP_GMP
@ -1446,7 +1446,7 @@ void mpz_manager<SYNCH>::bitwise_and(mpz const & a, mpz const & b, mpz & c) {
SASSERT(is_nonneg(a)); SASSERT(is_nonneg(a));
SASSERT(is_nonneg(b)); SASSERT(is_nonneg(b));
if (is_small(a) && is_small(b)) { if (is_small(a) && is_small(b)) {
c.set64(a.value64() & b.value64()); c.set64(a.value() & b.value());
} }
else { else {
#ifndef _MP_GMP #ifndef _MP_GMP
@ -1676,7 +1676,7 @@ bool mpz_manager<SYNCH>::is_int64(mpz const & a) const {
template<bool SYNCH> template<bool SYNCH>
uint64_t mpz_manager<SYNCH>::get_uint64(mpz const & a) const { uint64_t mpz_manager<SYNCH>::get_uint64(mpz const & a) const {
if (is_small(a)) if (is_small(a))
return static_cast<uint64_t>(a.value64()); return static_cast<uint64_t>(a.value());
#ifndef _MP_GMP #ifndef _MP_GMP
SASSERT(a.ptr()->m_size > 0); SASSERT(a.ptr()->m_size > 0);
return big_abs_to_uint64(a); return big_abs_to_uint64(a);
@ -1703,7 +1703,7 @@ uint64_t mpz_manager<SYNCH>::get_uint64(mpz const & a) const {
template<bool SYNCH> template<bool SYNCH>
int64_t mpz_manager<SYNCH>::get_int64(mpz const & a) const { int64_t mpz_manager<SYNCH>::get_int64(mpz const & a) const {
if (is_small(a)) if (is_small(a))
return a.value64(); return a.value();
#ifndef _MP_GMP #ifndef _MP_GMP
SASSERT(is_int64(a)); SASSERT(is_int64(a));
uint64_t num = big_abs_to_uint64(a); uint64_t num = big_abs_to_uint64(a);
@ -2031,7 +2031,7 @@ void mpz_manager<SYNCH>::ensure_capacity(mpz & a, unsigned capacity) {
capacity = m_init_cell_capacity; capacity = m_init_cell_capacity;
if (is_small(a)) { if (is_small(a)) {
int64_t val = a.value64(); int64_t val = a.value();
allocate_if_needed(a, capacity); allocate_if_needed(a, capacity);
SASSERT(a.ptr()->m_capacity >= capacity); SASSERT(a.ptr()->m_capacity >= capacity);
// Check if this is SMALL_INT_MIN which needs special handling // Check if this is SMALL_INT_MIN which needs special handling
@ -2125,7 +2125,7 @@ void mpz_manager<SYNCH>::machine_div2k(mpz & a, unsigned k) {
if (is_small(a)) { if (is_small(a)) {
if (k < 32) { if (k < 32) {
int64_t twok = 1ull << ((int64_t)k); int64_t twok = 1ull << ((int64_t)k);
int64_t val = a.value64(); int64_t val = a.value();
int64_t result = val / twok; int64_t result = val / twok;
// Division by power of 2 should keep us in small range // Division by power of 2 should keep us in small range
SASSERT(mpz::fits_in_small(result)); SASSERT(mpz::fits_in_small(result));
@ -2133,7 +2133,7 @@ void mpz_manager<SYNCH>::machine_div2k(mpz & a, unsigned k) {
} }
else if (k < 64) { else if (k < 64) {
int64_t twok = 1ull << ((int64_t)k); int64_t twok = 1ull << ((int64_t)k);
int64_t val = a.value64(); int64_t val = a.value();
a.set64(val/twok); a.set64(val/twok);
} }
else { else {
@ -2345,7 +2345,7 @@ unsigned mpz_manager<SYNCH>::mlog2(mpz const & a) {
if (is_nonneg(a)) if (is_nonneg(a))
return 0; return 0;
if (is_small(a)) { if (is_small(a)) {
int64_t v = a.value64(); int64_t v = a.value();
if (v == mpz::SMALL_INT_MIN) { if (v == mpz::SMALL_INT_MIN) {
// Special case: negating SMALL_INT_MIN would overflow // Special case: negating SMALL_INT_MIN would overflow
// For 32-bit: SMALL_INT_MIN = -2^30, so log2(2^30) = 30 // For 32-bit: SMALL_INT_MIN = -2^30, so log2(2^30) = 30
@ -2588,35 +2588,21 @@ template<bool SYNCH>
bool mpz_manager<SYNCH>::decompose(mpz const & a, svector<digit_t> & digits) { bool mpz_manager<SYNCH>::decompose(mpz const & a, svector<digit_t> & digits) {
digits.reset(); digits.reset();
if (is_small(a)) { if (is_small(a)) {
int64_t v = a.value64(); int64_t v = a.value();
if (v < 0) { bool is_neg = v < 0;
// Decompose negative value into digits uint64_t abs_v = is_neg ? static_cast<uint64_t>(-v) : static_cast<uint64_t>(v);
uint64_t abs_v = static_cast<uint64_t>(-v);
if (sizeof(digit_t) == sizeof(uint64_t)) { // Decompose absolute value into digits
digits.push_back(static_cast<digit_t>(abs_v)); if (sizeof(digit_t) == sizeof(uint64_t)) {
} else { digits.push_back(static_cast<digit_t>(abs_v));
// digit_t is 32-bit, need to split 64-bit value } else {
digits.push_back(static_cast<digit_t>(abs_v)); // digit_t is 32-bit, need to split 64-bit value
if (abs_v >> 32) { digits.push_back(static_cast<digit_t>(abs_v));
digits.push_back(static_cast<digit_t>(abs_v >> 32)); if (abs_v >> 32) {
} digits.push_back(static_cast<digit_t>(abs_v >> 32));
} }
return true;
}
else {
// Decompose positive value into digits
uint64_t abs_v = static_cast<uint64_t>(v);
if (sizeof(digit_t) == sizeof(uint64_t)) {
digits.push_back(static_cast<digit_t>(abs_v));
} else {
// digit_t is 32-bit, need to split 64-bit value
digits.push_back(static_cast<digit_t>(abs_v));
if (abs_v >> 32) {
digits.push_back(static_cast<digit_t>(abs_v >> 32));
}
}
return false;
} }
return is_neg;
} }
else { else {
#ifndef _MP_GMP #ifndef _MP_GMP
@ -2646,7 +2632,7 @@ bool mpz_manager<SYNCH>::decompose(mpz const & a, svector<digit_t> & digits) {
template<bool SYNCH> template<bool SYNCH>
bool mpz_manager<SYNCH>::get_bit(mpz const & a, unsigned index) { bool mpz_manager<SYNCH>::get_bit(mpz const & a, unsigned index) {
if (is_small(a)) { if (is_small(a)) {
int64_t v = a.value64(); int64_t v = a.value();
SASSERT(v >= 0); SASSERT(v >= 0);
if (index >= 64) if (index >= 64)
return false; return false;

13
src/util/mpz.h
View file

@ -201,14 +201,7 @@ public:
return (m_value & LARGE_BIT) == 0; return (m_value & LARGE_BIT) == 0;
} }
inline int value() const { inline int64_t value() const {
SASSERT(is_small());
// Decode small integer: shift right by 1 (arithmetic shift to preserve sign)
// Note: On 64-bit platforms, this may truncate if the value doesn't fit in int
return static_cast<int>(static_cast<intptr_t>(m_value) >> 1);
}
inline int64_t value64() const {
SASSERT(is_small()); SASSERT(is_small());
// Decode small integer: shift right by 1 (arithmetic shift to preserve sign) // Decode small integer: shift right by 1 (arithmetic shift to preserve sign)
return static_cast<int64_t>(static_cast<intptr_t>(m_value) >> 1); return static_cast<int64_t>(static_cast<intptr_t>(m_value) >> 1);
@ -334,7 +327,7 @@ class mpz_manager {
mpz m_two64; mpz m_two64;
static int64_t i64(mpz const & a) { return a.value64(); } static int64_t i64(mpz const & a) { return a.value(); }
void set_big_i64(mpz & c, int64_t v); void set_big_i64(mpz & c, int64_t v);
@ -406,7 +399,7 @@ class mpz_manager {
void get_sign_cell(mpz const & a, int & sign, mpz_cell * & cell, mpz_cell* reserve) { void get_sign_cell(mpz const & a, int & sign, mpz_cell * & cell, mpz_cell* reserve) {
if (is_small(a)) { if (is_small(a)) {
int64_t val = a.value64(); int64_t val = a.value();
cell = reserve; cell = reserve;
if (val < 0) { if (val < 0) {
sign = -1; sign = -1;