encapsulate mpz a bit more

Z3Prover · Jan 20, 2024 · a2993f7 · a2993f7
1 parent d2706ba
commit a2993f7
Show file tree

Hide file tree

Showing 2 changed files with 33 additions and 28 deletions.
diff --git a/src/util/mpq.h b/src/util/mpq.h
@@ -47,7 +47,7 @@ class mpq_manager : public mpz_manager<SYNCH> {
 
     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
@@ -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<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_i64(mpz & c, int64_t v) {
         if (v >= INT_MIN && v <= INT_MAX) {
-            c.m_val = static_cast<int>(v); 
-            c.m_kind = mpz_small;
+            c.set(static_cast<int>(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,17 +537,15 @@ 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);
         }
     }
 
     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<int>(val);
-            a.m_kind = mpz_small;
+            a.set(static_cast<int>(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