From 7e579604e19be1a86bcb0e52f50dc38002d00049 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 7 Feb 2015 19:39:15 +0000 Subject: [PATCH] Eliminated the old MS-Bignum interface because it stood in the way of progress. Signed-off-by: Christoph M. Wintersteiger --- src/util/mpff.cpp | 50 ++++++++++++--------------- src/util/mpff.h | 4 ++- src/util/mpfx.cpp | 26 +++++++------- src/util/mpfx.h | 2 ++ src/util/mpn.cpp | 16 +++++++-- src/util/mpn.h | 88 +++-------------------------------------------- src/util/mpz.cpp | 88 +++++++++++++++++++---------------------------- src/util/mpz.h | 4 ++- 8 files changed, 95 insertions(+), 183 deletions(-) diff --git a/src/util/mpff.cpp b/src/util/mpff.cpp index 7678a051e..b979b32ff 100644 --- a/src/util/mpff.cpp +++ b/src/util/mpff.cpp @@ -700,7 +700,7 @@ void mpff_manager::add_sub(bool is_sub, mpff const & a, mpff const & b, mpff & c c.m_sign = sgn_a; unsigned * sig_r = m_buffers[1].c_ptr(); size_t r_sz; - add_full(sig_a, m_precision, n_sig_b, m_precision, sig_r, m_precision + 1, &r_sz, 0); + m_mpn_manager.add(sig_a, m_precision, n_sig_b, m_precision, sig_r, m_precision + 1, &r_sz); SASSERT(r_sz <= m_precision + 1); unsigned num_leading_zeros = nlz(m_precision + 1, sig_r); SASSERT(num_leading_zeros >= sizeof(unsigned) * 8 - 1); // num_leading_zeros >= 31 @@ -740,11 +740,11 @@ void mpff_manager::add_sub(bool is_sub, mpff const & a, mpff const & b, mpff & c unsigned * sig_c = sig(c); if (::lt(m_precision, sig_a, n_sig_b)) { c.m_sign = sgn_b; - sub_diff(n_sig_b, m_precision, sig_a, m_precision, sig_c, &borrow, 0); + m_mpn_manager.sub(n_sig_b, m_precision, sig_a, m_precision, sig_c, &borrow); } else { c.m_sign = sgn_a; - sub_diff(sig_a, m_precision, n_sig_b, m_precision, sig_c, &borrow, 0); + m_mpn_manager.sub(sig_a, m_precision, n_sig_b, m_precision, sig_c, &borrow); } SASSERT(borrow == 0); unsigned num_leading_zeros = nlz(m_precision, sig_c); @@ -793,7 +793,7 @@ void mpff_manager::mul(mpff const & a, mpff const & b, mpff & c) { int64 exp_c = exp_a + exp_b; // store result in m_buffers[0] unsigned * r = m_buffers[0].c_ptr(); - multiply(sig(a), m_precision, sig(b), m_precision, r, 0); + m_mpn_manager.mul(sig(a), m_precision, sig(b), m_precision, r); // r has 2*m_precision_bits bits unsigned num_leading_zeros = nlz(m_precision*2, r); SASSERT(num_leading_zeros <= m_precision_bits); @@ -864,12 +864,10 @@ void mpff_manager::div(mpff const & a, mpff const & b, mpff & c) { // a is at least 2^(2*m_precision_bits - 1) // Thus the quotient of a/b cannot be zero // Actually, quotient of a/b must be >= 2^(2*m_precision_bits - 1)/(2^m_precision_bits - 1) - divide(_a, 2*m_precision, - sig(b), m_precision, - reciprocal_1_NULL, - q, - r, - 0); + m_mpn_manager.div(_a, 2 * m_precision, + sig(b), m_precision, + q, + r); TRACE("mpff_div", unsigned j = q_sz; while (j > 0) { --j; tout << std::hex << std::setfill('0') << std::setw(2*sizeof(unsigned)) << q[j]; tout << " "; } @@ -1193,7 +1191,7 @@ void mpff_manager::display(std::ostream & out, mpff const & n) const { if (shift > 0) shr(m_precision, u_buffer.c_ptr(), shift, u_buffer.c_ptr()); sbuffer str_buffer(11*m_precision, 0); - out << mp_decimal(u_buffer.c_ptr(), m_precision, str_buffer.begin(), str_buffer.size(), 0); + out << m_mpn_manager.to_string(u_buffer.c_ptr(), m_precision, str_buffer.begin(), str_buffer.size()); if (exp > 0) { if (exp <= 63) { uint64 _exp = 1; @@ -1225,7 +1223,7 @@ void mpff_manager::display(std::ostream & out, mpff const & n) const { } } -void mpff_manager::display_decimal(std::ostream & out, mpff const & n, unsigned prec, unsigned min_exponent) const { +void mpff_manager::display_decimal(std::ostream & out, mpff const & n, unsigned prec, unsigned min_exponent) { // The result in scientific notation when n.m_exponent >= min_exponent or n.m_exponent <= - min_exponent - m_precision_bits int64 exp = n.m_exponent; if (exp >= min_exponent || exp <= -static_cast(min_exponent) - m_precision_bits || is_int(n)) { @@ -1246,7 +1244,7 @@ void mpff_manager::display_decimal(std::ostream & out, mpff const & n, unsigned buffer.push_back(s[i]); shr(buffer.size(), buffer.c_ptr(), shift, buffer.size(), buffer.c_ptr()); sbuffer str_buffer(11*buffer.size(), 0); - out << mp_decimal(buffer.c_ptr(), buffer.size(), str_buffer.begin(), str_buffer.size(), 0); + out << m_mpn_manager.to_string(buffer.c_ptr(), buffer.size(), str_buffer.begin(), str_buffer.size()); } else { sbuffer buffer1, buffer2; @@ -1274,14 +1272,12 @@ void mpff_manager::display_decimal(std::ostream & out, mpff const & n, unsigned out << "0"; } else { - divide(buffer1.c_ptr(), m_precision, - pw_buffer.c_ptr(), num_words, - reciprocal_1_NULL, - buffer3.c_ptr(), - buffer2.c_ptr(), - 0); + m_mpn_manager.div(buffer1.c_ptr(), m_precision, + pw_buffer.c_ptr(), num_words, + buffer3.c_ptr(), + buffer2.c_ptr()); sbuffer str_buffer(11*buffer3.size(), 0); - out << mp_decimal(buffer3.c_ptr(), buffer3.size(), str_buffer.begin(), str_buffer.size(), 0); + out << m_mpn_manager.to_string(buffer3.c_ptr(), buffer3.size(), str_buffer.begin(), str_buffer.size()); SASSERT(!::is_zero(buffer2.size(), buffer2.c_ptr())); // otherwise n is an integer ::copy(buffer2.size(), buffer2.c_ptr(), buffer1.size(), buffer1.c_ptr()); } @@ -1298,7 +1294,7 @@ void mpff_manager::display_decimal(std::ostream & out, mpff const & n, unsigned return; } i = i + 1; - multiply(buffer1.c_ptr(), sz1, &ten, 1, buffer2.c_ptr(), 0); + m_mpn_manager.mul(buffer1.c_ptr(), sz1, &ten, 1, buffer2.c_ptr()); unsigned sz2 = sz1 + 1; while (sz2 > 0 && buffer2[sz2-1] == 0) --sz2; @@ -1310,12 +1306,10 @@ void mpff_manager::display_decimal(std::ostream & out, mpff const & n, unsigned SASSERT(sz1 == 0 || !::is_zero(sz1, buffer1.c_ptr())); } else { - divide(buffer2.c_ptr(), sz2, - pw_buffer.c_ptr(), num_words, - reciprocal_1_NULL, - buffer3.c_ptr(), - buffer1.c_ptr(), - 0); + m_mpn_manager.div(buffer2.c_ptr(), sz2, + pw_buffer.c_ptr(), num_words, + buffer3.c_ptr(), + buffer1.c_ptr()); out << buffer3[0]; sz1 = num_words; while (sz1 > 0 && buffer1[sz1-1] == 0) @@ -1353,7 +1347,7 @@ void mpff_manager::display_smt2(std::ostream & out, mpff const & n, bool decimal out << "(/ "; sbuffer str_buffer(11*m_precision, 0); - out << mp_decimal(u_buffer.c_ptr(), m_precision, str_buffer.begin(), str_buffer.size(), 0); + out << m_mpn_manager.to_string(u_buffer.c_ptr(), m_precision, str_buffer.begin(), str_buffer.size()); if (decimal) out << ".0"; if (exp != 0) { diff --git a/src/util/mpff.h b/src/util/mpff.h index 8d4c853af..ef488c934 100644 --- a/src/util/mpff.h +++ b/src/util/mpff.h @@ -29,6 +29,7 @@ Revision History: #include"z3_exception.h" #include"scoped_numeral.h" #include"scoped_numeral_vector.h" +#include"mpn.h" class mpff_manager; @@ -115,6 +116,7 @@ class mpff_manager { svector m_buffers[MPFF_NUM_BUFFERS]; svector m_set_buffer; mpff m_one; + mpn_manager m_mpn_manager; unsigned * sig(mpff const & n) const { return m_significands.c_ptr() + (n.m_sig_idx * m_precision); } @@ -465,7 +467,7 @@ public: void display_raw(std::ostream & out, mpff const & n) const; void display(std::ostream & out, mpff const & n) const; void display_pp(std::ostream & out, mpff const & n) const { display(out, n); } - void display_decimal(std::ostream & out, mpff const & n, unsigned prec=32, unsigned max_power=128) const; + void display_decimal(std::ostream & out, mpff const & n, unsigned prec=32, unsigned max_power=128); void display_smt2(std::ostream & out, mpff const & n, bool decimal=true) const; std::string to_string(mpff const & a) const; diff --git a/src/util/mpfx.cpp b/src/util/mpfx.cpp index c0b3a1936..c75a43046 100644 --- a/src/util/mpfx.cpp +++ b/src/util/mpfx.cpp @@ -387,12 +387,12 @@ void mpfx_manager::add_sub(bool is_sub, mpfx const & a, mpfx const & b, mpfx & c SASSERT(sgn_a != sgn_b); if (::lt(m_total_sz, w_a, w_b)) { c.m_sign = sgn_b; - sub_diff(w_b, m_total_sz, w_a, m_total_sz, w_c, &borrow, 0); + m_mpn_manager.sub(w_b, m_total_sz, w_a, m_total_sz, w_c, &borrow); SASSERT(!::is_zero(m_total_sz, w_c)); } else { c.m_sign = sgn_a; - sub_diff(w_a, m_total_sz, w_b, m_total_sz, w_c, &borrow, 0); + m_mpn_manager.sub(w_a, m_total_sz, w_b, m_total_sz, w_c, &borrow); if (::is_zero(m_total_sz, w_c)) reset(c); } @@ -423,7 +423,7 @@ void mpfx_manager::mul(mpfx const & a, mpfx const & b, mpfx & c) { allocate_if_needed(c); c.m_sign = a.m_sign ^ b.m_sign; unsigned * r = m_buffer0.c_ptr(); - multiply(words(a), m_total_sz, words(b), m_total_sz, r, 0); + m_mpn_manager.mul(words(a), m_total_sz, words(b), m_total_sz, r); // round result unsigned * _r = r + m_frac_part_sz; if ((c.m_sign == 1) != m_to_plus_inf && !::is_zero(m_frac_part_sz, r)) { @@ -473,12 +473,10 @@ void mpfx_manager::div(mpfx const & a, mpfx const & b, mpfx & c) { unsigned q_sz = a_shft_sz - b_sz + 1; unsigned * w_r = m_buffer2.c_ptr(); unsigned r_sz = b_sz; - divide(w_a_shft, a_shft_sz, - w_b, b_sz, - reciprocal_1_NULL, - w_q, - w_r, - 0); + m_mpn_manager.div(w_a_shft, a_shft_sz, + w_b, b_sz, + w_q, + w_r); for (unsigned i = m_total_sz; i < q_sz; i++) if (w_q[i] != 0) throw overflow_exception(); @@ -769,7 +767,7 @@ void mpfx_manager::display(std::ostream & out, mpfx const & n) const { } sbuffer str_buffer(11*sz, 0); - out << mp_decimal(w, sz, str_buffer.begin(), str_buffer.size(), 0); + out << m_mpn_manager.to_string(w, sz, str_buffer.begin(), str_buffer.size()); if (!is_int(n)) { SASSERT(shift != UINT_MAX); // reverse effect of shr @@ -796,7 +794,7 @@ void mpfx_manager::display_smt2(std::ostream & out, mpfx const & n) const { out << "(/ "; } sbuffer str_buffer(11*sz, 0); - out << mp_decimal(w, sz, str_buffer.begin(), str_buffer.size(), 0); + out << m_mpn_manager.to_string(w, sz, str_buffer.begin(), str_buffer.size()); if (!is_int(n)) { out << " "; unsigned * w = m_buffer0.c_ptr(); @@ -804,7 +802,7 @@ void mpfx_manager::display_smt2(std::ostream & out, mpfx const & n) const { w[i] = 0; w[m_frac_part_sz] = 1; sbuffer str_buffer2(11*(m_frac_part_sz+1), 0); - out << mp_decimal(w, m_frac_part_sz+1, str_buffer2.begin(), str_buffer2.size(), 0); + out << m_mpn_manager.to_string(w, m_frac_part_sz + 1, str_buffer2.begin(), str_buffer2.size()); out << ")"; } if (is_neg(n)) @@ -816,7 +814,7 @@ void mpfx_manager::display_decimal(std::ostream & out, mpfx const & n, unsigned out << "-"; unsigned * w = words(n); sbuffer str_buffer(11*m_int_part_sz, 0); - out << mp_decimal(w + m_frac_part_sz, m_int_part_sz, str_buffer.begin(), str_buffer.size(), 0); + out << m_mpn_manager.to_string(w + m_frac_part_sz, m_int_part_sz, str_buffer.begin(), str_buffer.size()); if (!is_int(n)) { out << "."; unsigned * frac = m_buffer0.c_ptr(); @@ -830,7 +828,7 @@ void mpfx_manager::display_decimal(std::ostream & out, mpfx const & n, unsigned out << "?"; return; } - multiply(frac, m_frac_part_sz, &ten, 1, n_frac, 0); + m_mpn_manager.mul(frac, m_frac_part_sz, &ten, 1, n_frac); frac_is_zero = ::is_zero(m_frac_part_sz, n_frac); SASSERT(n_frac[m_frac_part_sz] <= 9); if (!frac_is_zero || n_frac[m_frac_part_sz] != 0) diff --git a/src/util/mpfx.h b/src/util/mpfx.h index b4eeaebe6..f152128d8 100644 --- a/src/util/mpfx.h +++ b/src/util/mpfx.h @@ -25,6 +25,7 @@ Revision History: #include"z3_exception.h" #include"scoped_numeral.h" #include"scoped_numeral_vector.h" +#include"mpn.h" class mpfx_manager; @@ -83,6 +84,7 @@ class mpfx_manager { unsigned_vector m_buffer0, m_buffer1, m_buffer2; unsigned_vector m_tmp_digits; mpfx m_one; + mpn_manager m_mpn_manager; unsigned * words(mpfx const & n) const { return m_words.c_ptr() + (n.m_sig_idx * m_total_sz); } unsigned sz(unsigned * ws) const; diff --git a/src/util/mpn.cpp b/src/util/mpn.cpp index 6a544f583..ba0a8563a 100644 --- a/src/util/mpn.cpp +++ b/src/util/mpn.cpp @@ -26,17 +26,17 @@ Revision History: typedef uint64 mpn_double_digit; COMPILE_TIME_ASSERT(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit)); -mpn_manager static_mpn_manager; - const mpn_digit mpn_manager::zero = 0; mpn_manager::mpn_manager() { #ifdef Z3DEBUG trace_enabled=true; #endif + omp_init_nest_lock(&m_lock); } mpn_manager::~mpn_manager() { + omp_destroy_nest_lock(&m_lock); } int mpn_manager::compare(mpn_digit const * a, size_t const lnga, @@ -164,6 +164,7 @@ bool mpn_manager::div(mpn_digit const * numer, size_t const lnum, mpn_digit const * denom, size_t const lden, mpn_digit * quot, mpn_digit * rem) { + MPN_BEGIN_CRITICAL(); trace(numer, lnum, denom, lden, "/"); bool res = false; @@ -225,6 +226,7 @@ bool mpn_manager::div(mpn_digit const * numer, size_t const lnum, SASSERT(ok); #endif + MPN_END_CRITICAL(); return res; } @@ -233,6 +235,7 @@ size_t mpn_manager::div_normalize(mpn_digit const * numer, size_t const lnum, mpn_sbuffer & n_numer, mpn_sbuffer & n_denom) const { + MPN_BEGIN_CRITICAL(); size_t d = 0; while (((denom[lden-1] << d) & MASK_FIRST) == 0) d++; SASSERT(d < DIGIT_BITS); @@ -261,11 +264,13 @@ size_t mpn_manager::div_normalize(mpn_digit const * numer, size_t const lnum, STRACE("mpn_norm", tout << "Normalized: n_numer="; display_raw(tout, n_numer.c_ptr(), n_numer.size()); tout << " n_denom="; display_raw(tout, n_denom.c_ptr(), n_denom.size()); tout << std::endl; ); + MPN_END_CRITICAL(); return d; } void mpn_manager::div_unnormalize(mpn_sbuffer & numer, mpn_sbuffer & denom, size_t const d, mpn_digit * rem) const { + MPN_BEGIN_CRITICAL(); if (d == 0) { for (size_t i = 0; i < denom.size(); i++) rem[i] = numer[i]; @@ -275,11 +280,13 @@ void mpn_manager::div_unnormalize(mpn_sbuffer & numer, mpn_sbuffer & denom, rem[i] = numer[i] >> d | (LAST_BITS(d, numer[i+1]) << (DIGIT_BITS-d)); rem[denom.size()-1] = numer[denom.size()-1] >> d; } + MPN_END_CRITICAL(); } bool mpn_manager::div_1(mpn_sbuffer & numer, mpn_digit const denom, mpn_digit * quot) const { + MPN_BEGIN_CRITICAL(); mpn_double_digit q_hat, temp, r_hat, ms; mpn_digit borrow; @@ -307,11 +314,13 @@ bool mpn_manager::div_1(mpn_sbuffer & numer, mpn_digit const denom, tout << std::endl; ); } + MPN_END_CRITICAL(); return true; // return rem != 0 or something like that? } bool mpn_manager::div_n(mpn_sbuffer & numer, mpn_sbuffer const & denom, mpn_digit * quot, mpn_digit * rem) { + MPN_BEGIN_CRITICAL(); SASSERT(denom.size() > 1); // This is essentially Knuth's Algorithm D. @@ -363,7 +372,8 @@ bool mpn_manager::div_n(mpn_sbuffer & numer, mpn_sbuffer const & denom, tout << " borrow=" << borrow; tout << std::endl; ); } - + + MPN_END_CRITICAL(); return true; // return rem != 0 or something like that? } diff --git a/src/util/mpn.h b/src/util/mpn.h index 219368de3..ab96446b2 100644 --- a/src/util/mpn.h +++ b/src/util/mpn.h @@ -22,13 +22,15 @@ Revision History: #include #include"util.h" #include"buffer.h" - -// we supply a definition of a basic max because mpz relies on it. -#define max(a,b) (((a) > (b)) ? (a) : (b)) +#include"z3_omp.h" typedef unsigned int mpn_digit; class mpn_manager { + omp_nest_lock_t m_lock; +#define MPN_BEGIN_CRITICAL() omp_set_nest_lock(&const_cast(m_lock)); +#define MPN_END_CRITICAL() omp_unset_nest_lock(&const_cast(m_lock)); + public: mpn_manager(); ~mpn_manager(); @@ -56,7 +58,6 @@ public: char * to_string(mpn_digit const * a, size_t const lng, char * buf, size_t const lbuf) const; - private: #ifdef _AMD64_ class mpn_sbuffer : public sbuffer { @@ -112,85 +113,6 @@ private: void trace(mpn_digit const * a, size_t const lnga) const; void trace_nl(mpn_digit const * a, size_t const lnga) const; - -public: - // This function is needed because of the static_mpn_manager global variable. - // It must be invoked by the memory_manager during finalization. - // After we remove MSBignum from the code base, the global variable will - // not be needed anymore, and we will be able to eliminate this function. - void finalize() { - u.finalize(); - v.finalize(); - t_ms.finalize(); - t_ab.finalize(); - } }; - -// MSBignum compatible interface -// Note: The `owner' parameter is ignored. We use separate mpn_manager objects for the -// same purpose. Multiple owners are not supported in these compatibility functions, -// instead a static mpn_manager is used. - -extern mpn_manager static_mpn_manager; - -typedef unsigned int digit_t; - -typedef struct { - mpn_digit multiplier; - size_t shiftamt; -} reciprocal_1_t; - -#define reciprocal_1_NULL ((reciprocal_1_t*)0) - -inline int compare_diff(digit_t const * a, size_t const lnga, - digit_t const * b, size_t const lngb) -{ - return static_mpn_manager.compare(a, lnga, b, lngb); -} - -inline char * mp_decimal(digit_t const * a, size_t const lng, // Number to be converted and its length - char * buf, size_t const lbuf, // output buffer and its length - int owner) -{ - return static_mpn_manager.to_string(a, lng, buf, lbuf); -} - -inline bool add_full(digit_t const * a, size_t const lnga, - digit_t const * b, size_t const lngb, - digit_t *c, size_t const lngc_alloc, - size_t * plngc, - int owner) -{ - return static_mpn_manager.add(a, lnga, b, lngb, c, lngc_alloc, plngc); -} - -inline bool sub_diff(digit_t const * a, size_t const lnga, - digit_t const * b, size_t const lngb, - digit_t * c, digit_t * pborrow, - int owner) -{ - return static_mpn_manager.sub(a, lnga, b, lngb, c, pborrow); -} - -inline bool multiply(digit_t const * a, size_t const lnga, - digit_t const * b, size_t const lngb, - digit_t * c, - int owner) -{ - return static_mpn_manager.mul(a, lnga, b, lngb, c); -} - -inline bool divide(digit_t const * numer, size_t const lnum, - digit_t const * denom, size_t const lden, - reciprocal_1_t const * supplied_reciprocal, /* reciprocal_t struct for this denominator, - or reciprocal_1_NULL - if not previously precomputed */ - digit_t * quot, /* Quotient -- length MAX(lnum - lden + 1, 0) */ - digit_t * rem, /* Remainder -- length lden */ - int owner) -{ - return static_mpn_manager.div(numer, lnum, denom, lden, quot, rem); -} - #endif diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 94df9f78d..163f7fb86 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -37,7 +37,7 @@ Revision History: // #define LS_BINARY_GCD // #define LEHMER_GCD -#if defined(_MP_GMP) || (defined(_MP_MSBIGNUM) && defined(_AMD64_)) +#if defined(_MP_GMP) // Use LEHMER only if not using GMP // LEHMER assumes 32-bit digits, so it cannot be used with MSBIGNUM library + 64-bit binary #define EUCLID_GCD @@ -365,25 +365,18 @@ void mpz_manager::big_add_sub(mpz const & a, mpz const & b, mpz & c) { sign_b = -sign_b; size_t real_sz; if (sign_a == sign_b) { - unsigned sz = max(cell_a->m_size, cell_b->m_size)+1; + unsigned sz = std::max(cell_a->m_size, cell_b->m_size)+1; ensure_tmp_capacity<0>(sz); - add_full(cell_a->m_digits, - cell_a->m_size, - cell_b->m_digits, - cell_b->m_size, - m_tmp[0]->m_digits, - sz, - &real_sz, - 0); + m_mpn_manager.add(cell_a->m_digits, cell_a->m_size, + cell_b->m_digits, cell_b->m_size, + m_tmp[0]->m_digits, sz, &real_sz); SASSERT(real_sz <= sz); set<0>(c, sign_a, static_cast(real_sz)); } else { digit_t borrow; - int r = compare_diff(cell_a->m_digits, - cell_a->m_size, - cell_b->m_digits, - cell_b->m_size); + int r = m_mpn_manager.compare(cell_a->m_digits, cell_a->m_size, + cell_b->m_digits, cell_b->m_size); if (r == 0) { reset(c); } @@ -391,13 +384,12 @@ void mpz_manager::big_add_sub(mpz const & a, mpz const & b, mpz & c) { // a < b unsigned sz = cell_b->m_size; ensure_tmp_capacity<0>(sz); - sub_diff(cell_b->m_digits, - cell_b->m_size, - cell_a->m_digits, - cell_a->m_size, - m_tmp[0]->m_digits, - &borrow, - 0); + m_mpn_manager.sub(cell_b->m_digits, + cell_b->m_size, + cell_a->m_digits, + cell_a->m_size, + m_tmp[0]->m_digits, + &borrow); SASSERT(borrow == 0); set<0>(c, sign_b, sz); } @@ -405,13 +397,12 @@ void mpz_manager::big_add_sub(mpz const & a, mpz const & b, mpz & c) { // a > b unsigned sz = cell_a->m_size; ensure_tmp_capacity<0>(sz); - sub_diff(cell_a->m_digits, - cell_a->m_size, - cell_b->m_digits, - cell_b->m_size, - m_tmp[0]->m_digits, - &borrow, - 0); + m_mpn_manager.sub(cell_a->m_digits, + cell_a->m_size, + cell_b->m_digits, + cell_b->m_size, + m_tmp[0]->m_digits, + &borrow); SASSERT(borrow == 0); set<0>(c, sign_a, sz); } @@ -460,12 +451,11 @@ void mpz_manager::big_mul(mpz const & a, mpz const & b, mpz & c) { get_sign_cell<1>(b, sign_b, cell_b); unsigned sz = cell_a->m_size + cell_b->m_size; ensure_tmp_capacity<0>(sz); - multiply(cell_a->m_digits, - cell_a->m_size, - cell_b->m_digits, - cell_b->m_size, - m_tmp[0]->m_digits, - 0); + m_mpn_manager.mul(cell_a->m_digits, + cell_a->m_size, + cell_b->m_digits, + cell_b->m_size, + m_tmp[0]->m_digits); set<0>(c, sign_a == sign_b ? 1 : -1, sz); #else // GMP version @@ -505,14 +495,10 @@ void mpz_manager::quot_rem_core(mpz const & a, mpz const & b, mpz & q, mp unsigned r_sz = cell_b->m_size; ensure_tmp_capacity<0>(q_sz); ensure_tmp_capacity<1>(r_sz); - divide(cell_a->m_digits, - cell_a->m_size, - cell_b->m_digits, - cell_b->m_size, - reciprocal_1_NULL, - m_tmp[0]->m_digits, - m_tmp[1]->m_digits, - 0); + m_mpn_manager.div(cell_a->m_digits, cell_a->m_size, + cell_b->m_digits, cell_b->m_size, + m_tmp[0]->m_digits, + m_tmp[1]->m_digits); if (MODE == QUOT_ONLY || MODE == QUOT_AND_REM) set<0>(q, sign_a == sign_b ? 1 : -1, q_sz); if (MODE == REM_ONLY || MODE == QUOT_AND_REM) @@ -606,7 +592,7 @@ void mpz_manager::gcd(mpz const & a, mpz const & b, mpz & c) { // Binary GCD for big numbers // - It doesn't use division // - The initial experiments, don't show any performance improvement - // - It only works with _MP_INTERNAL and _MP_MSBIGNUM + // - It only works with _MP_INTERNAL mpz u, v, diff; set(u, a); set(v, b); @@ -1243,10 +1229,8 @@ int mpz_manager::big_compare(mpz const & a, mpz const & b) { // a is positive if (sign_b > 0) { // a & b are positive - return compare_diff(cell_a->m_digits, - cell_a->m_size, - cell_b->m_digits, - cell_b->m_size); + return m_mpn_manager.compare(cell_a->m_digits, cell_a->m_size, + cell_b->m_digits, cell_b->m_size); } else { // b is negative @@ -1261,10 +1245,8 @@ int mpz_manager::big_compare(mpz const & a, mpz const & b) { } else { // a & b are negative - return compare_diff(cell_b->m_digits, - cell_b->m_size, - cell_a->m_digits, - cell_a->m_size); + return m_mpn_manager.compare(cell_b->m_digits, cell_b->m_size, + cell_a->m_digits, cell_a->m_size); } } #else @@ -1411,11 +1393,11 @@ void mpz_manager::display(std::ostream & out, mpz const & a) const { out << "-"; if (sizeof(digit_t) == 4) { sbuffer buffer(11*size(a), 0); - out << mp_decimal(digits(a), size(a), buffer.begin(), buffer.size(), 0); + out << m_mpn_manager.to_string(digits(a), size(a), buffer.begin(), buffer.size()); } else { sbuffer buffer(21*size(a), 0); - out << mp_decimal(digits(a), size(a), buffer.begin(), buffer.size(), 0); + out << m_mpn_manager.to_string(digits(a), size(a), buffer.begin(), buffer.size()); } #else // GMP version diff --git a/src/util/mpz.h b/src/util/mpz.h index 923d5b3a7..05e87886d 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -27,6 +27,7 @@ Revision History: #include"scoped_numeral.h" #include"scoped_numeral_vector.h" #include"z3_omp.h" +#include"mpn.h" unsigned u_gcd(unsigned u, unsigned v); uint64 u64_gcd(uint64 u, uint64 v); @@ -37,7 +38,7 @@ typedef unsigned digit_t; #ifdef _MSC_VER #pragma warning(disable : 4200) -#endif +#endif template class mpz_manager; template class mpq_manager; @@ -107,6 +108,7 @@ class mpz_manager { omp_nest_lock_t m_lock; #define MPZ_BEGIN_CRITICAL() if (SYNCH) omp_set_nest_lock(&m_lock); #define MPZ_END_CRITICAL() if (SYNCH) omp_unset_nest_lock(&m_lock); + mpn_manager m_mpn_manager; #ifndef _MP_GMP unsigned m_init_cell_capacity;