From a2993f7457923ecfa1a7bdcaa5057b81f900a01b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 20 Jan 2024 12:57:43 -0800 Subject: [PATCH] encapsulate mpz a bit more --- src/util/mpq.h | 2 +- src/util/mpz.h | 59 +++++++++++++++++++++++++++----------------------- 2 files changed, 33 insertions(+), 28 deletions(-) diff --git a/src/util/mpq.h b/src/util/mpq.h index fa6e8ec756f..286c2758d86 100644 --- a/src/util/mpq.h +++ b/src/util/mpq.h @@ -47,7 +47,7 @@ class mpq_manager : public mpz_manager { void reset_denominator(mpq & a) { del(a.m_den); - a.m_den.m_val = 1; + a.m_den.set(1); } void normalize(mpq & a) { diff --git a/src/util/mpz.h b/src/util/mpz.h index 44e3e9c0bb8..6d1b3449df1 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -84,6 +84,7 @@ class mpz { #else typedef mpz_t mpz_type; #endif +protected: int m_val; unsigned m_kind:1; unsigned m_owner:1; @@ -116,6 +117,17 @@ class mpz { 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_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 @@ -242,14 +254,13 @@ class mpz_manager { mpz m_two64; - static int64_t i64(mpz const & a) { return static_cast(a.m_val); } + static int64_t i64(mpz const & a) { return static_cast(a.value()); } void set_big_i64(mpz & c, int64_t v); void set_i64(mpz & c, int64_t v) { if (v >= INT_MIN && v <= INT_MAX) { - c.m_val = static_cast(v); - c.m_kind = mpz_small; + c.set(static_cast(v)); } else { 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) { if (is_small(a)) { - if (a.m_val == INT_MIN) { + if (a.value() == INT_MIN) { sign = -1; cell = m_int_min.m_ptr; } else { cell = reserve; cell->m_size = 1; - if (a.m_val < 0) { + if (a.value() < 0) { sign = -1; - cell->m_digits[0] = -a.m_val; + cell->m_digits[0] = -a.value(); } else { sign = 1; - cell->m_digits[0] = a.m_val; + cell->m_digits[0] = a.value(); } } } else { - sign = a.m_val; + sign = a.sign(); cell = a.m_ptr; } } @@ -398,7 +409,7 @@ class 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); } @@ -461,7 +472,7 @@ class mpz_manager { bool eq(mpz const & a, mpz const & b) { if (is_small(a) && is_small(b)) { - return a.m_val == b.m_val; + return a.value() == b.value(); } else { return big_compare(a, b) == 0; @@ -470,7 +481,7 @@ class mpz_manager { bool lt(mpz const& a, int b) { if (is_small(a)) { - return a.m_val < b; + return a.value() < b; } else { return lt(a, mpz(b)); @@ -479,7 +490,7 @@ class mpz_manager { bool lt(mpz const & a, mpz const & b) { if (is_small(a) && is_small(b)) { - return a.m_val < b.m_val; + return a.value() < b.value(); } else { return big_compare(a, b) < 0; @@ -526,8 +537,7 @@ class mpz_manager { void set(mpz & target, mpz const & source) { if (is_small(source)) { - target.m_val = source.m_val; - target.m_kind = mpz_small; + target.set(source.value()); } else { big_set(target, source); @@ -535,8 +545,7 @@ class mpz_manager { } void set(mpz & a, int val) { - a.m_val = val; - a.m_kind = mpz_small; + a.set(val); } void set(mpz & a, unsigned val) { @@ -554,8 +563,7 @@ class mpz_manager { void set(mpz & a, uint64_t val) { if (val < INT_MAX) { - a.m_val = static_cast(val); - a.m_kind = mpz_small; + a.set(static_cast(val)); } else { set_big_ui64(a, val); @@ -574,10 +582,7 @@ class mpz_manager { void reset(mpz & a); void swap(mpz & a, mpz & b) noexcept { - std::swap(a.m_val, b.m_val); - 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; + a.swap(b); } bool is_uint64(mpz const & a) const; @@ -624,20 +629,20 @@ class mpz_manager { static bool is_one(mpz const & a) { #ifndef _MP_GMP - return is_small(a) && a.m_val == 1; + return is_small(a) && a.value() == 1; #else if (is_small(a)) - return a.m_val == 1; + return a.value() == 1; return mpz_cmp_si(*a.m_ptr, 1) == 0; #endif } static bool is_minus_one(mpz const & a) { #ifndef _MP_GMP - return is_small(a) && a.m_val == -1; + return is_small(a) && a.value() == -1; #else if (is_small(a)) - return a.m_val == -1; + return a.value() == -1; return mpz_cmp_si(*a.m_ptr, -1) == 0; #endif } @@ -712,7 +717,7 @@ class mpz_manager { bool is_even(mpz const & a) { if (is_small(a)) - return !(a.m_val & 0x1); + return !(a.value() & 0x1); #ifndef _MP_GMP return !(0x1 & digits(a)[0]); #else