mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-07 22:04:53 +00:00
Code Activity

fix

Browse source
This commit is contained in:
Nuno Lopes 2026-02-15 17:10:08 +00:00
parent bd993ca963
commit ac748d973c
4 changed files with 60 additions and 57 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/util/mpq.h
View file

@ -673,20 +673,17 @@ public:
}
void set(mpz & a, int val) { mpz_manager<SYNCH>::set(a, val); }
void set(mpz & a, int64_t val) { mpz_manager<SYNCH>::set(a, val); }
void set(mpq & a, int val) { set(a, (int64_t)val); }
void set(mpq & a, int64_t val) {
void set(mpq & a, int val) {
set(a.m_num, val);
reset_denominator(a);
}
void set(mpq & a, int64_t n, int64_t d) {
void set(mpq & a, int n, int d) {
SASSERT(d != 0);
if (d < 0) {
SASSERT(d != std::numeric_limits<int64_t>());
SASSERT(n != std::numeric_limits<int64_t>());
SASSERT(d != INT_MIN);
SASSERT(n != INT_MIN);
n = -n;
d = -d;
}
@ -727,6 +724,13 @@ public:
void set(mpq & a, char const * val);
void set(mpz & a, int64_t val) { mpz_manager<SYNCH>::set(a, val); }
void set(mpq & a, int64_t val) {
set(a.m_num, val);
reset_denominator(a);
}
void set(mpz & a, uint64_t val) { mpz_manager<SYNCH>::set(a, val); }
void set(mpq & a, uint64_t val) {

38
src/util/mpz.cpp
View file

@ -236,7 +236,7 @@ template<bool SYNCH>
void mpz_manager<SYNCH>::add(mpz const & a, mpz const & b, mpz & c) {
STRACE(mpz, tout << "[mpz] " << to_string(a) << " + " << to_string(b) << " == ";);
if (is_small(a) && is_small(b)) {
set_i64(c, i64(a) + i64(b));
set(c, a.value() + b.value());
}
else {
big_add(a, b, c);
@ -248,7 +248,7 @@ template<bool SYNCH>
void mpz_manager<SYNCH>::sub(mpz const & a, mpz const & b, mpz & c) {
STRACE(mpz, tout << "[mpz] " << to_string(a) << " - " << to_string(b) << " == ";);
if (is_small(a) && is_small(b)) {
set_i64(c, i64(a) - i64(b));
set(c, a.value() - b.value());
}
else {
big_sub(a, b, c);
@ -425,7 +425,7 @@ void mpz_manager<SYNCH>::set_digits(mpz & target, unsigned sz, digit_t const * d
#ifndef _MP_GMP
allocate_if_needed(target, sz);
memcpy(target.ptr()->m_digits, digits, sizeof(digit_t) * sz);
target.set_sign(1):
target.set_sign(1);
#else
mk_big(target);
// reset
@ -448,7 +448,7 @@ template<bool SYNCH>
void mpz_manager<SYNCH>::mul(mpz const & a, mpz const & b, mpz & c) {
STRACE(mpz, tout << "[mpz] " << to_string(a) << " * " << to_string(b) << " == ";);
if (is_small(a) && is_small(b)) {
set_i64(c, i64(a) * i64(b));
set(c, a.value() * b.value());
}
else {
big_mul(a, b, c);
@ -496,10 +496,10 @@ template<bool SYNCH>
void mpz_manager<SYNCH>::machine_div_rem(mpz const & a, mpz const & b, mpz & q, mpz & r) {
STRACE(mpz, tout << "[mpz-ext] divrem(" << to_string(a) << ", " << to_string(b) << ") == ";);
if (is_small(a) && is_small(b)) {
int64_t _a = i64(a);
int64_t _b = i64(b);
set_i64(q, _a / _b);
set_i64(r, _a % _b);
int64_t _a = a.value();
int64_t _b = b.value();
set(q, _a / _b);
set(r, _a % _b);
}
else {
big_div_rem(a, b, q, r);
@ -510,11 +510,11 @@ void mpz_manager<SYNCH>::machine_div_rem(mpz const & a, mpz const & b, mpz & q,
template<bool SYNCH>
void mpz_manager<SYNCH>::machine_div(mpz const & a, mpz const & b, mpz & c) {
STRACE(mpz, tout << "[mpz-ext] machine-div(" << to_string(a) << ", " << to_string(b) << ") == ";);
if (is_small(b) && i64(b) == 0)
if (is_small(b) && b.value() == 0)
throw default_exception("division by 0");
if (is_small(a) && is_small(b))
set_i64(c, i64(a) / i64(b));
set(c, a.value() / b.value());
else
big_div(a, b, c);
STRACE(mpz, tout << to_string(c) << "\n";);
@ -530,7 +530,7 @@ template<bool SYNCH>
void mpz_manager<SYNCH>::rem(mpz const & a, mpz const & b, mpz & c) {
STRACE(mpz, tout << "[mpz-ext] rem(" << to_string(a) << ", " << to_string(b) << ") == ";);
if (is_small(a) && is_small(b)) {
set_i64(c, i64(a) % i64(b));
set(c, a.value() % b.value());
}
else {
big_rem(a, b, c);
@ -597,8 +597,8 @@ mpz mpz_manager<SYNCH>::mod2k(mpz const & a, unsigned k) {
if (is_small(a) && k < 64) {
uint64_t mask = ((1ULL << k) - 1);
uint64_t uval = static_cast<uint64_t>(i64(a));
set_i64(result, static_cast<int64_t>(uval & mask));
uint64_t uval = static_cast<uint64_t>(a.value());
set(result, static_cast<int64_t>(uval & mask));
return result;
}
@ -1425,7 +1425,7 @@ void mpz_manager<SYNCH>::bitwise_xor(mpz const & a, mpz const & b, mpz & c) {
SASSERT(is_nonneg(a));
SASSERT(is_nonneg(b));
if (is_small(a) && is_small(b)) {
set_i64(c, i64(a) ^ i64(b));
set(c, a.value() ^ b.value());
}
else {
#ifndef _MP_GMP
@ -1902,9 +1902,9 @@ bool mpz_manager<SYNCH>::is_power_of_two(mpz const & a, unsigned & shift) {
if (is_nonpos(a))
return false;
if (is_small(a)) {
int64_t v = a.value();
auto v = static_cast<uint64_t>(a.value());
if (::is_power_of_two(v)) {
shift = log2(static_cast<uint64_t>(v));
shift = ::log2(v);
return true;
}
else {
@ -1968,7 +1968,7 @@ void mpz_manager<SYNCH>::ensure_capacity(mpz & a, unsigned capacity) {
unsigned old_sz = a.ptr()->m_size;
SASSERT(capacity >= old_sz);
new_cell->m_size = old_sz;
memcpy(new_cell->m_digits, digits(a), sizeof(digit_t) * old_sz)
memcpy(new_cell->m_digits, digits(a), sizeof(digit_t) * old_sz);
bool is_neg = a.sign() < 0;
deallocate(a);
a.set_ptr(new_cell, is_neg, false);
@ -2063,7 +2063,7 @@ void mpz_manager<SYNCH>::mul2k(mpz & a, unsigned k) {
if (k == 0 || is_zero(a))
return;
if (is_small(a) && k < 32) {
set_i64(a, i64(a) * (static_cast<int64_t>(1) << k));
set(a, a.value() * (static_cast<int64_t>(1) << k));
return;
}
#ifndef _MP_GMP
@ -2177,7 +2177,7 @@ unsigned mpz_manager<SYNCH>::mlog2(mpz const & a) {
if (is_nonneg(a))
return 0;
if (is_small(a)) {
return ::log2(static_cast<uint64_t>(-va.value()));
return ::log2(static_cast<uint64_t>(-a.value()));
}
#ifndef _MP_GMP
static_assert(sizeof(digit_t) == 8 || sizeof(digit_t) == 4, "");

2
src/util/mpz.h
View file

@ -317,8 +317,6 @@ class mpz_manager {
mpz m_two64;
static int64_t i64(mpz const & a) { return a.value(); }
void set_big_i64(mpz & c, int64_t v);
void set_big_ui64(mpz & c, uint64_t v);

59
src/util/rational.h
View file

@ -51,7 +51,7 @@ public:
explicit rational(int64_t n) { m().set(m_val, n); }
explicit rational(uint64_t n) { m().set(m_val, n); }
rational(int64_t n, int64_t d) { m().set(m_val, n, d); }
rational(int n, int d) { m().set(m_val, n, d); }
rational(mpq const & q) { m().set(m_val, q); }
rational(mpq && q) noexcept : m_val(std::move(q)) {}
rational(mpz const & z) { m().set(m_val, z); }
@ -173,6 +173,7 @@ public:
rational & operator=(bool) = delete;
rational operator*(bool r1) const = delete;
rational & operator=(int v) { return *this = (int64_t)v; }
rational & operator=(int64_t v) {
m().set(m_val, v);
return *this;
@ -194,7 +195,7 @@ public:
return *this;
}
rational & operator+=(int64_t r) {
rational & operator+=(int r) {
(*this) += rational(r);
return *this;
}
@ -204,7 +205,7 @@ public:
return *this;
}
rational& operator-=(int64_t r) {
rational& operator-=(int r) {
(*this) -= rational(r);
return *this;
}
@ -224,15 +225,15 @@ public:
return *this;
}
rational & operator%=(int64_t v) {
rational & operator%=(int v) {
return *this %= rational(v);
}
rational & operator/=(int64_t v) {
rational & operator/=(int v) {
return *this /= rational(v);
}
rational & operator*=(int64_t v) {
rational & operator*=(int v) {
return *this *= rational(v);
}
@ -562,11 +563,11 @@ inline bool operator>(rational const & r1, rational const & r2) {
return operator<(r2, r1);
}
inline bool operator<(int64_t r1, rational const & r2) {
inline bool operator<(int r1, rational const & r2) {
return rational(r1) < r2;
}
inline bool operator<(rational const & r1, int64_t r2) {
inline bool operator<(rational const & r1, int r2) {
return r1 < rational(r2);
}
@ -578,35 +579,35 @@ inline bool operator>=(rational const & r1, rational const & r2) {
return !operator<(r1, r2);
}
inline bool operator>(rational const & a, int64_t b) {
inline bool operator>(rational const & a, int b) {
return a > rational(b);
}
inline bool operator>(int64_t a, rational const & b) {
inline bool operator>(int a, rational const & b) {
return rational(a) > b;
}
inline bool operator>=(rational const& a, int64_t b) {
inline bool operator>=(rational const& a, int b) {
return a >= rational(b);
}
inline bool operator>=(int64_t a, rational const& b) {
inline bool operator>=(int a, rational const& b) {
return rational(a) >= b;
}
inline bool operator<=(rational const& a, int64_t b) {
inline bool operator<=(rational const& a, int b) {
return a <= rational(b);
}
inline bool operator<=(int64_t a, rational const& b) {
inline bool operator<=(int a, rational const& b) {
return rational(a) <= b;
}
inline bool operator!=(rational const& a, int64_t b) {
inline bool operator!=(rational const& a, int b) {
return !(a == rational(b));
}
inline bool operator==(rational const & a, int64_t b) {
inline bool operator==(rational const & a, int b) {
return a == rational(b);
}
@ -614,11 +615,11 @@ inline rational operator+(rational const & r1, rational const & r2) {
return rational(r1) += r2;
}
inline rational operator+(int64_t r1, rational const & r2) {
inline rational operator+(int r1, rational const & r2) {
return rational(r1) + r2;
}
inline rational operator+(rational const & r1, int64_t r2) {
inline rational operator+(rational const & r1, int r2) {
return r1 + rational(r2);
}
@ -627,11 +628,11 @@ inline rational operator-(rational const & r1, rational const & r2) {
return rational(r1) -= r2;
}
inline rational operator-(rational const & r1, int64_t r2) {
inline rational operator-(rational const & r1, int r2) {
return r1 - rational(r2);
}
inline rational operator-(int64_t r1, rational const & r2) {
inline rational operator-(int r1, rational const & r2) {
return rational(r1) - r2;
}
@ -647,17 +648,17 @@ inline rational operator*(rational const & r1, rational const & r2) {
inline rational operator*(rational const & r1, bool r2) {
UNREACHABLE();
return r1 * rational((uint64_t)r2);
}
inline rational operator*(rational const & r1, int64_t r2) {
return r1 * rational(r2);
}
inline rational operator*(bool r1, rational const & r2) {
inline rational operator*(rational const & r1, int r2) {
return r1 * rational(r2);
}
inline rational operator*(bool r1, rational const & r2) {
UNREACHABLE();
return rational((uint64_t)r1) * r2;
return rational(r1) * r2;
}
inline rational operator*(int64_t r1, rational const & r2) {
inline rational operator*(int r1, rational const & r2) {
return rational(r1) * r2;
}
@ -665,16 +666,16 @@ inline rational operator/(rational const & r1, rational const & r2) {
return rational(r1) /= r2;
}
inline rational operator/(rational const & r1, int64_t r2) {
inline rational operator/(rational const & r1, int r2) {
return r1 / rational(r2);
}
inline rational operator/(rational const & r1, bool r2) {
UNREACHABLE();
return r1 / rational((uint64_t)r2);
return r1 / rational(r2);
}
inline rational operator/(int64_t r1, rational const & r2) {
inline rational operator/(int r1, rational const & r2) {
return rational(r1) / r2;
}