mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 20:31:21 +00:00
Code Activity

encapsulate mpz a bit more

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-01-20 12:57:43 -08:00
parent d2706bab64
commit a2993f7457
2 changed files with 33 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/util/mpq.h
View file

@ -47,7 +47,7 @@ class mpq_manager : public mpz_manager<SYNCH> {
void reset_denominator(mpq & a) { void reset_denominator(mpq & a) {
del(a.m_den); del(a.m_den);
a.m_den.m_val = 1; a.m_den.set(1);
} }
void normalize(mpq & a) { void normalize(mpq & a) {

59
src/util/mpz.h
View file

@ -84,6 +84,7 @@ class mpz {
#else #else
typedef mpz_t mpz_type; typedef mpz_t mpz_type;
#endif #endif
protected:
int m_val; int m_val;
unsigned m_kind:1; unsigned m_kind:1;
unsigned m_owner:1; unsigned m_owner:1;
@ -116,6 +117,17 @@ public:
unsigned o = m_owner; m_owner = other.m_owner; other.m_owner = o; 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; unsigned k = m_kind; m_kind = other.m_kind; other.m_kind = k;
} }
void set(int v) {
m_val = v;
m_kind = mpz_small;
}
inline bool is_small() const { return m_kind == mpz_small; }
inline int value() const { SASSERT(is_small()); return m_val; }
inline int sign() const { SASSERT(!is_small()); return m_val; }
}; };
#ifndef _MP_GMP #ifndef _MP_GMP
@ -242,14 +254,13 @@ class mpz_manager {
mpz m_two64; mpz m_two64;
static int64_t i64(mpz const & a) { return static_cast<int64_t>(a.m_val); } static int64_t i64(mpz const & a) { return static_cast<int64_t>(a.value()); }
void set_big_i64(mpz & c, int64_t v); void set_big_i64(mpz & c, int64_t v);
void set_i64(mpz & c, int64_t v) { void set_i64(mpz & c, int64_t v) {
if (v >= INT_MIN && v <= INT_MAX) { if (v >= INT_MIN && v <= INT_MAX) {
c.m_val = static_cast<int>(v); c.set(static_cast<int>(v));
c.m_kind = mpz_small;
} }
else { else {
set_big_i64(c, v); set_big_i64(c, v);
@ -306,25 +317,25 @@ 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)) {
if (a.m_val == INT_MIN) { if (a.value() == INT_MIN) {
sign = -1; sign = -1;
cell = m_int_min.m_ptr; cell = m_int_min.m_ptr;
} }
else { else {
cell = reserve; cell = reserve;
cell->m_size = 1; cell->m_size = 1;
if (a.m_val < 0) { if (a.value() < 0) {
sign = -1; sign = -1;
cell->m_digits[0] = -a.m_val; cell->m_digits[0] = -a.value();
} }
else { else {
sign = 1; sign = 1;
cell->m_digits[0] = a.m_val; cell->m_digits[0] = a.value();
} }
} }
} }
else { else {
sign = a.m_val; sign = a.sign();
cell = a.m_ptr; cell = a.m_ptr;
} }
} }
@ -398,7 +409,7 @@ public:
~mpz_manager(); ~mpz_manager();
static bool is_small(mpz const & a) { return a.m_kind == mpz_small; } static bool is_small(mpz const & a) { return a.is_small(); }
static mpz mk_z(int val) { return mpz(val); } static mpz mk_z(int val) { return mpz(val); }
@ -461,7 +472,7 @@ public:
bool eq(mpz const & a, mpz const & b) { bool eq(mpz const & a, mpz const & b) {
if (is_small(a) && is_small(b)) { if (is_small(a) && is_small(b)) {
return a.m_val == b.m_val; return a.value() == b.value();
} }
else { else {
return big_compare(a, b) == 0; return big_compare(a, b) == 0;
@ -470,7 +481,7 @@ public:
bool lt(mpz const& a, int b) { bool lt(mpz const& a, int b) {
if (is_small(a)) { if (is_small(a)) {
return a.m_val < b; return a.value() < b;
} }
else { else {
return lt(a, mpz(b)); return lt(a, mpz(b));
@ -479,7 +490,7 @@ public:
bool lt(mpz const & a, mpz const & b) { bool lt(mpz const & a, mpz const & b) {
if (is_small(a) && is_small(b)) { if (is_small(a) && is_small(b)) {
return a.m_val < b.m_val; return a.value() < b.value();
} }
else { else {
return big_compare(a, b) < 0; return big_compare(a, b) < 0;
@ -526,8 +537,7 @@ public:
void set(mpz & target, mpz const & source) { void set(mpz & target, mpz const & source) {
if (is_small(source)) { if (is_small(source)) {
target.m_val = source.m_val; target.set(source.value());
target.m_kind = mpz_small;
} }
else { else {
big_set(target, source); big_set(target, source);
@ -535,8 +545,7 @@ public:
} }
void set(mpz & a, int val) { void set(mpz & a, int val) {
a.m_val = val; a.set(val);
a.m_kind = mpz_small;
} }
void set(mpz & a, unsigned val) { void set(mpz & a, unsigned val) {
@ -554,8 +563,7 @@ public:
void set(mpz & a, uint64_t val) { void set(mpz & a, uint64_t val) {
if (val < INT_MAX) { if (val < INT_MAX) {
a.m_val = static_cast<int>(val); a.set(static_cast<int>(val));
a.m_kind = mpz_small;
} }
else { else {
set_big_ui64(a, val); set_big_ui64(a, val);
@ -574,10 +582,7 @@ public:
void reset(mpz & a); void reset(mpz & a);
void swap(mpz & a, mpz & b) noexcept { void swap(mpz & a, mpz & b) noexcept {
std::swap(a.m_val, b.m_val); a.swap(b);
std::swap(a.m_ptr, b.m_ptr);
auto o = a.m_owner; a.m_owner = b.m_owner; b.m_owner = o;
auto k = a.m_kind; a.m_kind = b.m_kind; b.m_kind = k;
} }
bool is_uint64(mpz const & a) const; bool is_uint64(mpz const & a) const;
@ -624,20 +629,20 @@ public:
static bool is_one(mpz const & a) { static bool is_one(mpz const & a) {
#ifndef _MP_GMP #ifndef _MP_GMP
return is_small(a) && a.m_val == 1; return is_small(a) && a.value() == 1;
#else #else
if (is_small(a)) if (is_small(a))
return a.m_val == 1; return a.value() == 1;
return mpz_cmp_si(*a.m_ptr, 1) == 0; return mpz_cmp_si(*a.m_ptr, 1) == 0;
#endif #endif
} }
static bool is_minus_one(mpz const & a) { static bool is_minus_one(mpz const & a) {
#ifndef _MP_GMP #ifndef _MP_GMP
return is_small(a) && a.m_val == -1; return is_small(a) && a.value() == -1;
#else #else
if (is_small(a)) if (is_small(a))
return a.m_val == -1; return a.value() == -1;
return mpz_cmp_si(*a.m_ptr, -1) == 0; return mpz_cmp_si(*a.m_ptr, -1) == 0;
#endif #endif
} }
@ -712,7 +717,7 @@ public:
bool is_even(mpz const & a) { bool is_even(mpz const & a) {
if (is_small(a)) if (is_small(a))
return !(a.m_val & 0x1); return !(a.value() & 0x1);
#ifndef _MP_GMP #ifndef _MP_GMP
return !(0x1 & digits(a)[0]); return !(0x1 & digits(a)[0]);
#else #else