encapsulate anum functionality

Z3Prover · Jan 20, 2024 · 1754523 · 1754523
1 parent 548be4c
commit 1754523
Show file tree

Hide file tree

Showing 2 changed files with 27 additions and 20 deletions.
diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp
@@ -204,21 +204,21 @@ namespace algebraic_numbers {
         }
 
         void del(numeral & a) {
-            if (a.m_cell == nullptr)
+            if (a.is_null())
                 return;
             if (a.is_basic())
                 del(a.to_basic());
             else
                 del(a.to_algebraic());
-            a.m_cell = nullptr;
+            a.clear();
         }
 
         void reset(numeral & a) {
             del(a);
         }
 
         bool is_zero(numeral const & a) {
-            return a.m_cell == nullptr;
+            return a.is_null();
         }
 
         bool is_pos(numeral const & a) {
@@ -359,7 +359,7 @@ namespace algebraic_numbers {
         }
 
         void swap(numeral & a, numeral & b) noexcept {
-            std::swap(a.m_cell, b.m_cell);
+            a.swap(b);
         }
 
         basic_cell * mk_basic_cell(mpq & n) {
@@ -432,13 +432,13 @@ namespace algebraic_numbers {
             }
             if (a.is_basic()) {
                 if (is_zero(a))
-                    a.m_cell = mk_basic_cell(n);
+                    a = mk_basic_cell(n);
                 else
                     qm().set(a.to_basic()->m_value, n);
             }
             else {
                 del(a);
-                a.m_cell = mk_basic_cell(n);
+                a = mk_basic_cell(n);
             }
         }
 
@@ -492,7 +492,7 @@ namespace algebraic_numbers {
             else {
                 if (a.is_basic()) {
                     del(a);
-                    a.m_cell = TAG(void*, mk_algebraic_cell(sz, p, lower, upper, minimal), ROOT);
+                    a = mk_algebraic_cell(sz, p, lower, upper, minimal);
                 }
                 else {
                     SASSERT(sz > 2);
@@ -526,7 +526,7 @@ namespace algebraic_numbers {
                     del(a);
                     void * mem = m_allocator.allocate(sizeof(algebraic_cell));
                     algebraic_cell * c = new (mem) algebraic_cell();
-                    a.m_cell = TAG(void *, c, ROOT);
+                    a = c;
                     copy(c, b.to_algebraic());
                     SASSERT(acell_inv(*c));
                 }
@@ -796,7 +796,7 @@ namespace algebraic_numbers {
                 scoped_mpq r(qm());
                 to_mpq(qm(), lower(c), r);
                 del(c);
-                a.m_cell = mk_basic_cell(r);
+                a = mk_basic_cell(r);
                 return false;
             }
         }
@@ -817,7 +817,7 @@ namespace algebraic_numbers {
                 scoped_mpq r(qm());
                 to_mpq(qm(), lower(c), r);
                 del(c);
-                a.m_cell = mk_basic_cell(r);
+                a = mk_basic_cell(r);
                 return false;
             }
             SASSERT(acell_inv(*c));

diff --git a/src/math/polynomial/algebraic_numbers.h b/src/math/polynomial/algebraic_numbers.h
@@ -360,19 +360,25 @@ namespace algebraic_numbers {
     struct basic_cell;
     struct algebraic_cell;
 
-    enum anum_kind { BASIC = 0, ROOT };
-
-    class anum {
-        friend struct manager::imp;
-        friend class manager;
-        void * m_cell;
-        anum(basic_cell * cell):m_cell(TAG(void*, cell, BASIC)) {}
-        anum(algebraic_cell * cell):m_cell(TAG(void*, cell, ROOT)) {}
+
+
+    class anum {   
+        enum anum_kind { BASIC = 0, ROOT };
+        void* m_cell;
+    public:
+        anum() :m_cell(nullptr) {}
+        anum(basic_cell* cell) :m_cell(TAG(void*, cell, BASIC)) { }
+        anum(algebraic_cell * cell):m_cell(TAG(void*, cell, ROOT)) {  }
+
         bool is_basic() const { return GET_TAG(m_cell) == BASIC; }
         basic_cell * to_basic() const { SASSERT(is_basic()); return UNTAG(basic_cell*, m_cell); }
         algebraic_cell * to_algebraic() const { SASSERT(!is_basic()); return UNTAG(algebraic_cell*, m_cell); }
-    public:
-        anum():m_cell(nullptr) {}
+
+        bool is_null() const { return m_cell == nullptr; }
+        void clear() { m_cell = nullptr; }
+        void swap(anum & other) { std::swap(m_cell, other.m_cell); }
+        anum& operator=(basic_cell* cell) { SASSERT(is_null());  m_cell = TAG(void*, cell, BASIC); return *this; }
+        anum& operator=(algebraic_cell* cell) { SASSERT(is_null());  m_cell = TAG(void*, cell, ROOT); return *this; }
     };
 };
 
@@ -428,6 +434,7 @@ AN_MK_BINARY(operator/, div)
 #undef AN_MK_BINARY
 #undef AN_MK_BINARY_CORE
 
+
 inline scoped_anum root(scoped_anum const & a, unsigned k) {
     scoped_anum r(a.m());
     a.m().root(a, k, r);