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

Nikolaj's changes in rationals

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-06-28 16:22:40 -07:00
parent c2f3428373
commit 40a363d249
2 changed files with 29 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

46
src/util/mpz.cpp
View file

@ -237,7 +237,7 @@ void mpz_manager<SYNCH>::set_big_i64(mpz & c, int64_t v) {
c.m_ptr = allocate(m_init_cell_capacity); c.m_ptr = allocate(m_init_cell_capacity);
c.m_owner = mpz_self; c.m_owner = mpz_self;
} }
c.m_kind = mpz_ptr_k; c.m_kind = mpz_ptr;
SASSERT(capacity(c) >= m_init_cell_capacity); SASSERT(capacity(c) >= m_init_cell_capacity);
uint64_t _v; uint64_t _v;
if (v < 0) { if (v < 0) {
@ -293,7 +293,7 @@ void mpz_manager<SYNCH>::set_big_ui64(mpz & c, uint64_t v) {
c.m_ptr = allocate(m_init_cell_capacity); c.m_ptr = allocate(m_init_cell_capacity);
c.m_owner = mpz_self; c.m_owner = mpz_self;
} }
c.m_kind = mpz_ptr_k; c.m_kind = mpz_ptr;
SASSERT(capacity(c) >= m_init_cell_capacity); SASSERT(capacity(c) >= m_init_cell_capacity);
c.m_val = 1; c.m_val = 1;
if (sizeof(digit_t) == sizeof(uint64_t)) { if (sizeof(digit_t) == sizeof(uint64_t)) {
@ -368,7 +368,7 @@ void mpz_manager<SYNCH>::set(mpz_cell& src, mpz & a, int sign, unsigned sz) {
set_digits(a, i, src.m_digits); set_digits(a, i, src.m_digits);
a.m_val = sign; a.m_val = sign;
SASSERT(a.m_kind == mpz_ptr_k); SASSERT(a.m_kind == mpz_ptr);
} }
#endif #endif
@ -413,7 +413,7 @@ void mpz_manager<SYNCH>::set_digits(mpz & target, unsigned sz, digit_t const * d
target.m_ptr = allocate(c); target.m_ptr = allocate(c);
target.m_ptr->m_size = sz; target.m_ptr->m_size = sz;
target.m_ptr->m_capacity = c; target.m_ptr->m_capacity = c;
target.m_kind = mpz_ptr_k; target.m_kind = mpz_ptr;
target.m_owner = mpz_self; target.m_owner = mpz_self;
memcpy(target.m_ptr->m_digits, digits, sizeof(digit_t) * sz); memcpy(target.m_ptr->m_digits, digits, sizeof(digit_t) * sz);
} }
@ -426,14 +426,14 @@ void mpz_manager<SYNCH>::set_digits(mpz & target, unsigned sz, digit_t const * d
deallocate(target); deallocate(target);
target.m_val = 1; target.m_val = 1;
target.m_ptr = ptr; target.m_ptr = ptr;
target.m_kind = mpz_ptr_k; target.m_kind = mpz_ptr;
target.m_owner = mpz_self; target.m_owner = mpz_self;
} }
else { else {
target.m_ptr->m_size = sz; target.m_ptr->m_size = sz;
if (target.m_ptr->m_digits != digits) if (target.m_ptr->m_digits != digits)
memcpy(target.m_ptr->m_digits, digits, sizeof(digit_t) * sz); memcpy(target.m_ptr->m_digits, digits, sizeof(digit_t) * sz);
target.m_kind = mpz_ptr_k; target.m_kind = mpz_ptr;
} }
#else #else
mk_big(target); mk_big(target);
@ -1453,7 +1453,7 @@ void mpz_manager<SYNCH>::big_set(mpz & target, mpz const & source) {
target.m_ptr = allocate(capacity(source)); target.m_ptr = allocate(capacity(source));
target.m_ptr->m_size = size(source); target.m_ptr->m_size = size(source);
target.m_ptr->m_capacity = capacity(source); target.m_ptr->m_capacity = capacity(source);
target.m_kind = mpz_ptr_k; target.m_kind = mpz_ptr;
target.m_owner = mpz_self; target.m_owner = mpz_self;
memcpy(target.m_ptr->m_digits, source.m_ptr->m_digits, sizeof(digit_t) * size(source)); memcpy(target.m_ptr->m_digits, source.m_ptr->m_digits, sizeof(digit_t) * size(source));
} }
@ -1462,14 +1462,14 @@ void mpz_manager<SYNCH>::big_set(mpz & target, mpz const & source) {
target.m_ptr = allocate(capacity(source)); target.m_ptr = allocate(capacity(source));
target.m_ptr->m_size = size(source); target.m_ptr->m_size = size(source);
target.m_ptr->m_capacity = capacity(source); target.m_ptr->m_capacity = capacity(source);
target.m_kind = mpz_ptr_k; target.m_kind = mpz_ptr;
target.m_owner = mpz_self; target.m_owner = mpz_self;
memcpy(target.m_ptr->m_digits, source.m_ptr->m_digits, sizeof(digit_t) * size(source)); memcpy(target.m_ptr->m_digits, source.m_ptr->m_digits, sizeof(digit_t) * size(source));
} }
else { else {
target.m_ptr->m_size = size(source); target.m_ptr->m_size = size(source);
memcpy(target.m_ptr->m_digits, source.m_ptr->m_digits, sizeof(digit_t) * size(source)); memcpy(target.m_ptr->m_digits, source.m_ptr->m_digits, sizeof(digit_t) * size(source));
target.m_kind = mpz_ptr_k; target.m_kind = mpz_ptr;
} }
#else #else
// GMP version // GMP version
@ -1736,7 +1736,7 @@ void mpz_manager<SYNCH>::power(mpz const & a, unsigned p, mpz & b) {
b.m_ptr->m_digits[i] = 0; b.m_ptr->m_digits[i] = 0;
b.m_ptr->m_digits[sz-1] = 1 << shift; b.m_ptr->m_digits[sz-1] = 1 << shift;
b.m_val = 1; b.m_val = 1;
b.m_kind = mpz_ptr_k; b.m_kind = mpz_ptr;
} }
return; return;
} }
@ -1819,25 +1819,26 @@ void mpz_manager<SYNCH>::ensure_capacity(mpz & a, unsigned capacity) {
return; return;
if (capacity < m_init_cell_capacity) if (capacity < m_init_cell_capacity)
capacity = m_init_cell_capacity; capacity = m_init_cell_capacity;
if (a.m_ptr == nullptr) {
a.m_ptr = allocate(capacity); if (is_small(a)) {
a.m_owner = mpz_self; int val = a.m_val;
a.m_kind = mpz_ptr_k; allocate_if_needed(a, capacity);
SASSERT(a.m_ptr->m_capacity == capacity); a.m_kind = mpz_ptr;
if (a.m_val == INT_MIN) { SASSERT(a.m_ptr->m_capacity >= capacity);
if (val == INT_MIN) {
unsigned intmin_sz = m_int_min.m_ptr->m_size; unsigned intmin_sz = m_int_min.m_ptr->m_size;
for (unsigned i = 0; i < intmin_sz; i++) for (unsigned i = 0; i < intmin_sz; i++)
a.m_ptr->m_digits[i] = m_int_min.m_ptr->m_digits[i]; a.m_ptr->m_digits[i] = m_int_min.m_ptr->m_digits[i];
a.m_val = -1; a.m_val = -1;
a.m_ptr->m_size = m_int_min.m_ptr->m_size; a.m_ptr->m_size = m_int_min.m_ptr->m_size;
} }
else if (a.m_val < 0) { else if (val < 0) {
a.m_ptr->m_digits[0] = -a.m_val; a.m_ptr->m_digits[0] = -val;
a.m_val = -1; a.m_val = -1;
a.m_ptr->m_size = 1; a.m_ptr->m_size = 1;
} }
else { else {
a.m_ptr->m_digits[0] = a.m_val; a.m_ptr->m_digits[0] = val;
a.m_val = 1; a.m_val = 1;
a.m_ptr->m_size = 1; a.m_ptr->m_size = 1;
} }
@ -1852,7 +1853,7 @@ void mpz_manager<SYNCH>::ensure_capacity(mpz & a, unsigned capacity) {
deallocate(a); deallocate(a);
a.m_ptr = new_cell; a.m_ptr = new_cell;
a.m_owner = mpz_self; a.m_owner = mpz_self;
a.m_kind = mpz_ptr_k; a.m_kind = mpz_ptr;
} }
} }
@ -1969,8 +1970,9 @@ void mpz_manager<SYNCH>::mul2k(mpz & a, unsigned k) {
unsigned new_sz = old_sz + word_shift + 1; unsigned new_sz = old_sz + word_shift + 1;
ensure_capacity(a, new_sz); ensure_capacity(a, new_sz);
TRACE("mpz_mul2k", tout << "word_shift: " << word_shift << "\nbit_shift: " << bit_shift << "\nold_sz: " << old_sz << "\nnew_sz: " << new_sz TRACE("mpz_mul2k", tout << "word_shift: " << word_shift << "\nbit_shift: " << bit_shift << "\nold_sz: " << old_sz << "\nnew_sz: " << new_sz
<< "\na after ensure capacity:\n" << to_string(a) << "\n";); << "\na after ensure capacity:\n" << to_string(a) << "\n";
SASSERT(a.m_ptr != nullptr); tout << a.m_kind << "\n";);
SASSERT(!is_small(a));
mpz_cell * cell_a = a.m_ptr; mpz_cell * cell_a = a.m_ptr;
old_sz = cell_a->m_size; old_sz = cell_a->m_size;
digit_t * ds = cell_a->m_digits; digit_t * ds = cell_a->m_digits;

7
src/util/mpz.h
View file

@ -79,7 +79,7 @@ class mpz_cell {
under winodws, m_ptr points to a mpz_cell that store the value. under winodws, m_ptr points to a mpz_cell that store the value.
*/ */
enum mpz_kind { mpz_small = 0, mpz_ptr_k = 1}; enum mpz_kind { mpz_small = 0, mpz_ptr = 1};
enum mpz_owner { mpz_self = 0, mpz_ext = 1}; enum mpz_owner { mpz_self = 0, mpz_ext = 1};
class mpz { class mpz {
@ -172,10 +172,13 @@ class mpz_manager {
if (n.m_ptr == nullptr || capacity(n) < c) { if (n.m_ptr == nullptr || capacity(n) < c) {
deallocate(n); deallocate(n);
n.m_val = 1; n.m_val = 1;
n.m_kind = mpz_ptr_k; n.m_kind = mpz_ptr;
n.m_owner = mpz_self; n.m_owner = mpz_self;
n.m_ptr = allocate(c); n.m_ptr = allocate(c);
} }
else {
n.m_kind = mpz_ptr;
}
} }
void deallocate(bool is_heap, mpz_cell * ptr) { void deallocate(bool is_heap, mpz_cell * ptr) {