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

Eliminated the old MS-Bignum interface because it stood in the way of progress.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-02-07 19:39:15 +00:00
parent da01f237fd
commit 7e579604e1
8 changed files with 95 additions and 183 deletions
Download patch file Download diff file Expand all files Collapse all files

38
src/util/mpff.cpp
View file

@ -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; c.m_sign = sgn_a;
unsigned * sig_r = m_buffers[1].c_ptr(); unsigned * sig_r = m_buffers[1].c_ptr();
size_t r_sz; 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); SASSERT(r_sz <= m_precision + 1);
unsigned num_leading_zeros = nlz(m_precision + 1, sig_r); unsigned num_leading_zeros = nlz(m_precision + 1, sig_r);
SASSERT(num_leading_zeros >= sizeof(unsigned) * 8 - 1); // num_leading_zeros >= 31 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); unsigned * sig_c = sig(c);
if (::lt(m_precision, sig_a, n_sig_b)) { if (::lt(m_precision, sig_a, n_sig_b)) {
c.m_sign = sgn_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 { else {
c.m_sign = sgn_a; 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); SASSERT(borrow == 0);
unsigned num_leading_zeros = nlz(m_precision, sig_c); 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; int64 exp_c = exp_a + exp_b;
// store result in m_buffers[0] // store result in m_buffers[0]
unsigned * r = m_buffers[0].c_ptr(); 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 // r has 2*m_precision_bits bits
unsigned num_leading_zeros = nlz(m_precision*2, r); unsigned num_leading_zeros = nlz(m_precision*2, r);
SASSERT(num_leading_zeros <= m_precision_bits); 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) // a is at least 2^(2*m_precision_bits - 1)
// Thus the quotient of a/b cannot be zero // 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) // Actually, quotient of a/b must be >= 2^(2*m_precision_bits - 1)/(2^m_precision_bits - 1)
divide(_a, 2*m_precision, m_mpn_manager.div(_a, 2 * m_precision,
sig(b), m_precision, sig(b), m_precision,
reciprocal_1_NULL,
q, q,
r, r);
0);
TRACE("mpff_div", TRACE("mpff_div",
unsigned j = q_sz; unsigned j = q_sz;
while (j > 0) { --j; tout << std::hex << std::setfill('0') << std::setw(2*sizeof(unsigned)) << q[j]; tout << " "; } 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) if (shift > 0)
shr(m_precision, u_buffer.c_ptr(), shift, u_buffer.c_ptr()); shr(m_precision, u_buffer.c_ptr(), shift, u_buffer.c_ptr());
sbuffer<char, 1024> str_buffer(11*m_precision, 0); sbuffer<char, 1024> 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 > 0) {
if (exp <= 63) { if (exp <= 63) {
uint64 _exp = 1; 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 // 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; int64 exp = n.m_exponent;
if (exp >= min_exponent || exp <= -static_cast<int64>(min_exponent) - m_precision_bits || is_int(n)) { if (exp >= min_exponent || exp <= -static_cast<int64>(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]); buffer.push_back(s[i]);
shr(buffer.size(), buffer.c_ptr(), shift, buffer.size(), buffer.c_ptr()); shr(buffer.size(), buffer.c_ptr(), shift, buffer.size(), buffer.c_ptr());
sbuffer<char, 1024> str_buffer(11*buffer.size(), 0); sbuffer<char, 1024> 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 { else {
sbuffer<unsigned, 1024> buffer1, buffer2; sbuffer<unsigned, 1024> buffer1, buffer2;
@ -1274,14 +1272,12 @@ void mpff_manager::display_decimal(std::ostream & out, mpff const & n, unsigned
out << "0"; out << "0";
} }
else { else {
divide(buffer1.c_ptr(), m_precision, m_mpn_manager.div(buffer1.c_ptr(), m_precision,
pw_buffer.c_ptr(), num_words, pw_buffer.c_ptr(), num_words,
reciprocal_1_NULL,
buffer3.c_ptr(), buffer3.c_ptr(),
buffer2.c_ptr(), buffer2.c_ptr());
0);
sbuffer<char, 1024> str_buffer(11*buffer3.size(), 0); sbuffer<char, 1024> 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 SASSERT(!::is_zero(buffer2.size(), buffer2.c_ptr())); // otherwise n is an integer
::copy(buffer2.size(), buffer2.c_ptr(), buffer1.size(), buffer1.c_ptr()); ::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; return;
} }
i = i + 1; 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; unsigned sz2 = sz1 + 1;
while (sz2 > 0 && buffer2[sz2-1] == 0) while (sz2 > 0 && buffer2[sz2-1] == 0)
--sz2; --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())); SASSERT(sz1 == 0 || !::is_zero(sz1, buffer1.c_ptr()));
} }
else { else {
divide(buffer2.c_ptr(), sz2, m_mpn_manager.div(buffer2.c_ptr(), sz2,
pw_buffer.c_ptr(), num_words, pw_buffer.c_ptr(), num_words,
reciprocal_1_NULL,
buffer3.c_ptr(), buffer3.c_ptr(),
buffer1.c_ptr(), buffer1.c_ptr());
0);
out << buffer3[0]; out << buffer3[0];
sz1 = num_words; sz1 = num_words;
while (sz1 > 0 && buffer1[sz1-1] == 0) 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 << "(/ "; out << "(/ ";
sbuffer<char, 1024> str_buffer(11*m_precision, 0); sbuffer<char, 1024> 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 (decimal) out << ".0";
if (exp != 0) { if (exp != 0) {

4
src/util/mpff.h
View file

@ -29,6 +29,7 @@ Revision History:
#include"z3_exception.h" #include"z3_exception.h"
#include"scoped_numeral.h" #include"scoped_numeral.h"
#include"scoped_numeral_vector.h" #include"scoped_numeral_vector.h"
#include"mpn.h"
class mpff_manager; class mpff_manager;
@ -115,6 +116,7 @@ class mpff_manager {
svector<unsigned> m_buffers[MPFF_NUM_BUFFERS]; svector<unsigned> m_buffers[MPFF_NUM_BUFFERS];
svector<unsigned> m_set_buffer; svector<unsigned> m_set_buffer;
mpff m_one; 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); } 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_raw(std::ostream & out, mpff const & n) const;
void display(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_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; void display_smt2(std::ostream & out, mpff const & n, bool decimal=true) const;
std::string to_string(mpff const & a) const; std::string to_string(mpff const & a) const;

22
src/util/mpfx.cpp
View file

@ -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); SASSERT(sgn_a != sgn_b);
if (::lt(m_total_sz, w_a, w_b)) { if (::lt(m_total_sz, w_a, w_b)) {
c.m_sign = sgn_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)); SASSERT(!::is_zero(m_total_sz, w_c));
} }
else { else {
c.m_sign = sgn_a; 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)) if (::is_zero(m_total_sz, w_c))
reset(c); reset(c);
} }
@ -423,7 +423,7 @@ void mpfx_manager::mul(mpfx const & a, mpfx const & b, mpfx & c) {
allocate_if_needed(c); allocate_if_needed(c);
c.m_sign = a.m_sign ^ b.m_sign; c.m_sign = a.m_sign ^ b.m_sign;
unsigned * r = m_buffer0.c_ptr(); 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 // round result
unsigned * _r = r + m_frac_part_sz; unsigned * _r = r + m_frac_part_sz;
if ((c.m_sign == 1) != m_to_plus_inf && !::is_zero(m_frac_part_sz, r)) { 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 q_sz = a_shft_sz - b_sz + 1;
unsigned * w_r = m_buffer2.c_ptr(); unsigned * w_r = m_buffer2.c_ptr();
unsigned r_sz = b_sz; unsigned r_sz = b_sz;
divide(w_a_shft, a_shft_sz, m_mpn_manager.div(w_a_shft, a_shft_sz,
w_b, b_sz, w_b, b_sz,
reciprocal_1_NULL,
w_q, w_q,
w_r, w_r);
0);
for (unsigned i = m_total_sz; i < q_sz; i++) for (unsigned i = m_total_sz; i < q_sz; i++)
if (w_q[i] != 0) if (w_q[i] != 0)
throw overflow_exception(); throw overflow_exception();
@ -769,7 +767,7 @@ void mpfx_manager::display(std::ostream & out, mpfx const & n) const {
} }
sbuffer<char, 1024> str_buffer(11*sz, 0); sbuffer<char, 1024> 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)) { if (!is_int(n)) {
SASSERT(shift != UINT_MAX); SASSERT(shift != UINT_MAX);
// reverse effect of shr // reverse effect of shr
@ -796,7 +794,7 @@ void mpfx_manager::display_smt2(std::ostream & out, mpfx const & n) const {
out << "(/ "; out << "(/ ";
} }
sbuffer<char, 1024> str_buffer(11*sz, 0); sbuffer<char, 1024> 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)) { if (!is_int(n)) {
out << " "; out << " ";
unsigned * w = m_buffer0.c_ptr(); 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[i] = 0;
w[m_frac_part_sz] = 1; w[m_frac_part_sz] = 1;
sbuffer<char, 1024> str_buffer2(11*(m_frac_part_sz+1), 0); sbuffer<char, 1024> 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 << ")"; out << ")";
} }
if (is_neg(n)) if (is_neg(n))
@ -816,7 +814,7 @@ void mpfx_manager::display_decimal(std::ostream & out, mpfx const & n, unsigned
out << "-"; out << "-";
unsigned * w = words(n); unsigned * w = words(n);
sbuffer<char, 1024> str_buffer(11*m_int_part_sz, 0); sbuffer<char, 1024> 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)) { if (!is_int(n)) {
out << "."; out << ".";
unsigned * frac = m_buffer0.c_ptr(); unsigned * frac = m_buffer0.c_ptr();
@ -830,7 +828,7 @@ void mpfx_manager::display_decimal(std::ostream & out, mpfx const & n, unsigned
out << "?"; out << "?";
return; 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); frac_is_zero = ::is_zero(m_frac_part_sz, n_frac);
SASSERT(n_frac[m_frac_part_sz] <= 9); SASSERT(n_frac[m_frac_part_sz] <= 9);
if (!frac_is_zero || n_frac[m_frac_part_sz] != 0) if (!frac_is_zero || n_frac[m_frac_part_sz] != 0)

2
src/util/mpfx.h
View file

@ -25,6 +25,7 @@ Revision History:
#include"z3_exception.h" #include"z3_exception.h"
#include"scoped_numeral.h" #include"scoped_numeral.h"
#include"scoped_numeral_vector.h" #include"scoped_numeral_vector.h"
#include"mpn.h"
class mpfx_manager; class mpfx_manager;
@ -83,6 +84,7 @@ class mpfx_manager {
unsigned_vector m_buffer0, m_buffer1, m_buffer2; unsigned_vector m_buffer0, m_buffer1, m_buffer2;
unsigned_vector m_tmp_digits; unsigned_vector m_tmp_digits;
mpfx m_one; 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 * words(mpfx const & n) const { return m_words.c_ptr() + (n.m_sig_idx * m_total_sz); }
unsigned sz(unsigned * ws) const; unsigned sz(unsigned * ws) const;

14
src/util/mpn.cpp
View file

@ -26,17 +26,17 @@ Revision History:
typedef uint64 mpn_double_digit; typedef uint64 mpn_double_digit;
COMPILE_TIME_ASSERT(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit)); COMPILE_TIME_ASSERT(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit));
mpn_manager static_mpn_manager;
const mpn_digit mpn_manager::zero = 0; const mpn_digit mpn_manager::zero = 0;
mpn_manager::mpn_manager() { mpn_manager::mpn_manager() {
#ifdef Z3DEBUG #ifdef Z3DEBUG
trace_enabled=true; trace_enabled=true;
#endif #endif
omp_init_nest_lock(&m_lock);
} }
mpn_manager::~mpn_manager() { mpn_manager::~mpn_manager() {
omp_destroy_nest_lock(&m_lock);
} }
int mpn_manager::compare(mpn_digit const * a, size_t const lnga, 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 const * denom, size_t const lden,
mpn_digit * quot, mpn_digit * quot,
mpn_digit * rem) { mpn_digit * rem) {
MPN_BEGIN_CRITICAL();
trace(numer, lnum, denom, lden, "/"); trace(numer, lnum, denom, lden, "/");
bool res = false; bool res = false;
@ -225,6 +226,7 @@ bool mpn_manager::div(mpn_digit const * numer, size_t const lnum,
SASSERT(ok); SASSERT(ok);
#endif #endif
MPN_END_CRITICAL();
return res; 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_numer,
mpn_sbuffer & n_denom) const mpn_sbuffer & n_denom) const
{ {
MPN_BEGIN_CRITICAL();
size_t d = 0; size_t d = 0;
while (((denom[lden-1] << d) & MASK_FIRST) == 0) d++; while (((denom[lden-1] << d) & MASK_FIRST) == 0) d++;
SASSERT(d < DIGIT_BITS); 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()); 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; ); tout << " n_denom="; display_raw(tout, n_denom.c_ptr(), n_denom.size()); tout << std::endl; );
MPN_END_CRITICAL();
return d; return d;
} }
void mpn_manager::div_unnormalize(mpn_sbuffer & numer, mpn_sbuffer & denom, void mpn_manager::div_unnormalize(mpn_sbuffer & numer, mpn_sbuffer & denom,
size_t const d, mpn_digit * rem) const { size_t const d, mpn_digit * rem) const {
MPN_BEGIN_CRITICAL();
if (d == 0) { if (d == 0) {
for (size_t i = 0; i < denom.size(); i++) for (size_t i = 0; i < denom.size(); i++)
rem[i] = numer[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[i] = numer[i] >> d | (LAST_BITS(d, numer[i+1]) << (DIGIT_BITS-d));
rem[denom.size()-1] = numer[denom.size()-1] >> 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, bool mpn_manager::div_1(mpn_sbuffer & numer, mpn_digit const denom,
mpn_digit * quot) const mpn_digit * quot) const
{ {
MPN_BEGIN_CRITICAL();
mpn_double_digit q_hat, temp, r_hat, ms; mpn_double_digit q_hat, temp, r_hat, ms;
mpn_digit borrow; mpn_digit borrow;
@ -307,11 +314,13 @@ bool mpn_manager::div_1(mpn_sbuffer & numer, mpn_digit const denom,
tout << std::endl; ); tout << std::endl; );
} }
MPN_END_CRITICAL();
return true; // return rem != 0 or something like that? return true; // return rem != 0 or something like that?
} }
bool mpn_manager::div_n(mpn_sbuffer & numer, mpn_sbuffer const & denom, bool mpn_manager::div_n(mpn_sbuffer & numer, mpn_sbuffer const & denom,
mpn_digit * quot, mpn_digit * rem) { mpn_digit * quot, mpn_digit * rem) {
MPN_BEGIN_CRITICAL();
SASSERT(denom.size() > 1); SASSERT(denom.size() > 1);
// This is essentially Knuth's Algorithm D. // This is essentially Knuth's Algorithm D.
@ -364,6 +373,7 @@ bool mpn_manager::div_n(mpn_sbuffer & numer, mpn_sbuffer const & denom,
tout << std::endl; ); tout << std::endl; );
} }
MPN_END_CRITICAL();
return true; // return rem != 0 or something like that? return true; // return rem != 0 or something like that?
} }

88
src/util/mpn.h
View file

@ -22,13 +22,15 @@ Revision History:
#include<ostream> #include<ostream>
#include"util.h" #include"util.h"
#include"buffer.h" #include"buffer.h"
#include"z3_omp.h"
// we supply a definition of a basic max because mpz relies on it.
#define max(a,b) (((a) > (b)) ? (a) : (b))
typedef unsigned int mpn_digit; typedef unsigned int mpn_digit;
class mpn_manager { class mpn_manager {
omp_nest_lock_t m_lock;
#define MPN_BEGIN_CRITICAL() omp_set_nest_lock(&const_cast<omp_nest_lock_t>(m_lock));
#define MPN_END_CRITICAL() omp_unset_nest_lock(&const_cast<omp_nest_lock_t>(m_lock));
public: public:
mpn_manager(); mpn_manager();
~mpn_manager(); ~mpn_manager();
@ -56,7 +58,6 @@ public:
char * to_string(mpn_digit const * a, size_t const lng, char * to_string(mpn_digit const * a, size_t const lng,
char * buf, size_t const lbuf) const; char * buf, size_t const lbuf) const;
private: private:
#ifdef _AMD64_ #ifdef _AMD64_
class mpn_sbuffer : public sbuffer<mpn_digit> { class mpn_sbuffer : public sbuffer<mpn_digit> {
@ -112,85 +113,6 @@ private:
void trace(mpn_digit const * a, size_t const lnga) const; void trace(mpn_digit const * a, size_t const lnga) const;
void trace_nl(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 #endif

64
src/util/mpz.cpp
View file

@ -37,7 +37,7 @@ Revision History:
// #define LS_BINARY_GCD // #define LS_BINARY_GCD
// #define LEHMER_GCD // #define LEHMER_GCD
#if defined(_MP_GMP) || (defined(_MP_MSBIGNUM) && defined(_AMD64_)) #if defined(_MP_GMP)
// Use LEHMER only if not using GMP // Use LEHMER only if not using GMP
// LEHMER assumes 32-bit digits, so it cannot be used with MSBIGNUM library + 64-bit binary // LEHMER assumes 32-bit digits, so it cannot be used with MSBIGNUM library + 64-bit binary
#define EUCLID_GCD #define EUCLID_GCD
@ -365,25 +365,18 @@ void mpz_manager<SYNCH>::big_add_sub(mpz const & a, mpz const & b, mpz & c) {
sign_b = -sign_b; sign_b = -sign_b;
size_t real_sz; size_t real_sz;
if (sign_a == sign_b) { 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); ensure_tmp_capacity<0>(sz);
add_full(cell_a->m_digits, m_mpn_manager.add(cell_a->m_digits, cell_a->m_size,
cell_a->m_size, cell_b->m_digits, cell_b->m_size,
cell_b->m_digits, m_tmp[0]->m_digits, sz, &real_sz);
cell_b->m_size,
m_tmp[0]->m_digits,
sz,
&real_sz,
0);
SASSERT(real_sz <= sz); SASSERT(real_sz <= sz);
set<0>(c, sign_a, static_cast<unsigned>(real_sz)); set<0>(c, sign_a, static_cast<unsigned>(real_sz));
} }
else { else {
digit_t borrow; digit_t borrow;
int r = compare_diff(cell_a->m_digits, int r = m_mpn_manager.compare(cell_a->m_digits, cell_a->m_size,
cell_a->m_size, cell_b->m_digits, cell_b->m_size);
cell_b->m_digits,
cell_b->m_size);
if (r == 0) { if (r == 0) {
reset(c); reset(c);
} }
@ -391,13 +384,12 @@ void mpz_manager<SYNCH>::big_add_sub(mpz const & a, mpz const & b, mpz & c) {
// a < b // a < b
unsigned sz = cell_b->m_size; unsigned sz = cell_b->m_size;
ensure_tmp_capacity<0>(sz); ensure_tmp_capacity<0>(sz);
sub_diff(cell_b->m_digits, m_mpn_manager.sub(cell_b->m_digits,
cell_b->m_size, cell_b->m_size,
cell_a->m_digits, cell_a->m_digits,
cell_a->m_size, cell_a->m_size,
m_tmp[0]->m_digits, m_tmp[0]->m_digits,
&borrow, &borrow);
0);
SASSERT(borrow == 0); SASSERT(borrow == 0);
set<0>(c, sign_b, sz); set<0>(c, sign_b, sz);
} }
@ -405,13 +397,12 @@ void mpz_manager<SYNCH>::big_add_sub(mpz const & a, mpz const & b, mpz & c) {
// a > b // a > b
unsigned sz = cell_a->m_size; unsigned sz = cell_a->m_size;
ensure_tmp_capacity<0>(sz); ensure_tmp_capacity<0>(sz);
sub_diff(cell_a->m_digits, m_mpn_manager.sub(cell_a->m_digits,
cell_a->m_size, cell_a->m_size,
cell_b->m_digits, cell_b->m_digits,
cell_b->m_size, cell_b->m_size,
m_tmp[0]->m_digits, m_tmp[0]->m_digits,
&borrow, &borrow);
0);
SASSERT(borrow == 0); SASSERT(borrow == 0);
set<0>(c, sign_a, sz); set<0>(c, sign_a, sz);
} }
@ -460,12 +451,11 @@ void mpz_manager<SYNCH>::big_mul(mpz const & a, mpz const & b, mpz & c) {
get_sign_cell<1>(b, sign_b, cell_b); get_sign_cell<1>(b, sign_b, cell_b);
unsigned sz = cell_a->m_size + cell_b->m_size; unsigned sz = cell_a->m_size + cell_b->m_size;
ensure_tmp_capacity<0>(sz); ensure_tmp_capacity<0>(sz);
multiply(cell_a->m_digits, m_mpn_manager.mul(cell_a->m_digits,
cell_a->m_size, cell_a->m_size,
cell_b->m_digits, cell_b->m_digits,
cell_b->m_size, cell_b->m_size,
m_tmp[0]->m_digits, m_tmp[0]->m_digits);
0);
set<0>(c, sign_a == sign_b ? 1 : -1, sz); set<0>(c, sign_a == sign_b ? 1 : -1, sz);
#else #else
// GMP version // GMP version
@ -505,14 +495,10 @@ void mpz_manager<SYNCH>::quot_rem_core(mpz const & a, mpz const & b, mpz & q, mp
unsigned r_sz = cell_b->m_size; unsigned r_sz = cell_b->m_size;
ensure_tmp_capacity<0>(q_sz); ensure_tmp_capacity<0>(q_sz);
ensure_tmp_capacity<1>(r_sz); ensure_tmp_capacity<1>(r_sz);
divide(cell_a->m_digits, m_mpn_manager.div(cell_a->m_digits, cell_a->m_size,
cell_a->m_size, cell_b->m_digits, cell_b->m_size,
cell_b->m_digits,
cell_b->m_size,
reciprocal_1_NULL,
m_tmp[0]->m_digits, m_tmp[0]->m_digits,
m_tmp[1]->m_digits, m_tmp[1]->m_digits);
0);
if (MODE == QUOT_ONLY || MODE == QUOT_AND_REM) if (MODE == QUOT_ONLY || MODE == QUOT_AND_REM)
set<0>(q, sign_a == sign_b ? 1 : -1, q_sz); set<0>(q, sign_a == sign_b ? 1 : -1, q_sz);
if (MODE == REM_ONLY || MODE == QUOT_AND_REM) if (MODE == REM_ONLY || MODE == QUOT_AND_REM)
@ -606,7 +592,7 @@ void mpz_manager<SYNCH>::gcd(mpz const & a, mpz const & b, mpz & c) {
// Binary GCD for big numbers // Binary GCD for big numbers
// - It doesn't use division // - It doesn't use division
// - The initial experiments, don't show any performance improvement // - 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; mpz u, v, diff;
set(u, a); set(u, a);
set(v, b); set(v, b);
@ -1243,10 +1229,8 @@ int mpz_manager<SYNCH>::big_compare(mpz const & a, mpz const & b) {
// a is positive // a is positive
if (sign_b > 0) { if (sign_b > 0) {
// a & b are positive // a & b are positive
return compare_diff(cell_a->m_digits, return m_mpn_manager.compare(cell_a->m_digits, cell_a->m_size,
cell_a->m_size, cell_b->m_digits, cell_b->m_size);
cell_b->m_digits,
cell_b->m_size);
} }
else { else {
// b is negative // b is negative
@ -1261,10 +1245,8 @@ int mpz_manager<SYNCH>::big_compare(mpz const & a, mpz const & b) {
} }
else { else {
// a & b are negative // a & b are negative
return compare_diff(cell_b->m_digits, return m_mpn_manager.compare(cell_b->m_digits, cell_b->m_size,
cell_b->m_size, cell_a->m_digits, cell_a->m_size);
cell_a->m_digits,
cell_a->m_size);
} }
} }
#else #else
@ -1411,11 +1393,11 @@ void mpz_manager<SYNCH>::display(std::ostream & out, mpz const & a) const {
out << "-"; out << "-";
if (sizeof(digit_t) == 4) { if (sizeof(digit_t) == 4) {
sbuffer<char, 1024> buffer(11*size(a), 0); sbuffer<char, 1024> 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 { else {
sbuffer<char, 1024> buffer(21*size(a), 0); sbuffer<char, 1024> 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 #else
// GMP version // GMP version

2
src/util/mpz.h
View file

@ -27,6 +27,7 @@ Revision History:
#include"scoped_numeral.h" #include"scoped_numeral.h"
#include"scoped_numeral_vector.h" #include"scoped_numeral_vector.h"
#include"z3_omp.h" #include"z3_omp.h"
#include"mpn.h"
unsigned u_gcd(unsigned u, unsigned v); unsigned u_gcd(unsigned u, unsigned v);
uint64 u64_gcd(uint64 u, uint64 v); uint64 u64_gcd(uint64 u, uint64 v);
@ -107,6 +108,7 @@ class mpz_manager {
omp_nest_lock_t m_lock; omp_nest_lock_t m_lock;
#define MPZ_BEGIN_CRITICAL() if (SYNCH) omp_set_nest_lock(&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); #define MPZ_END_CRITICAL() if (SYNCH) omp_unset_nest_lock(&m_lock);
mpn_manager m_mpn_manager;
#ifndef _MP_GMP #ifndef _MP_GMP
unsigned m_init_cell_capacity; unsigned m_init_cell_capacity;