mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

MPN synchronization fix

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-02-08 13:25:18 +00:00
parent 7e579604e1
commit a78dd680fb
2 changed files with 45 additions and 74 deletions
Download patch file Download diff file Expand all files Collapse all files

107
src/util/mpn.cpp
View file

@ -29,9 +29,6 @@ COMPILE_TIME_ASSERT(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit));
const mpn_digit mpn_manager::zero = 0; const mpn_digit mpn_manager::zero = 0;
mpn_manager::mpn_manager() { mpn_manager::mpn_manager() {
#ifdef Z3DEBUG
trace_enabled=true;
#endif
omp_init_nest_lock(&m_lock); omp_init_nest_lock(&m_lock);
} }
@ -43,11 +40,6 @@ int mpn_manager::compare(mpn_digit const * a, size_t const lnga,
mpn_digit const * b, size_t const lngb) const { mpn_digit const * b, size_t const lngb) const {
int res = 0; int res = 0;
#ifdef Z3DEBUG
if (trace_enabled)
STRACE("mpn", tout << "[mpn] "; );
#endif
trace(a, lnga); trace(a, lnga);
size_t j = max(lnga, lngb) - 1; size_t j = max(lnga, lngb) - 1;
@ -60,10 +52,7 @@ int mpn_manager::compare(mpn_digit const * a, size_t const lnga,
res = -1; res = -1;
} }
#ifdef Z3DEBUG TRACE("mpn", tout << ((res == 1) ? " > " : (res == -1) ? " < " : " == "); );
if (trace_enabled)
STRACE("mpn", tout << ((res == 1) ? " > " : (res == -1) ? " < " : " == "); );
#endif
trace_nl(b, lngb); trace_nl(b, lngb);
return res; return res;
@ -92,7 +81,7 @@ bool mpn_manager::add(mpn_digit const * a, size_t const lnga,
for (os = len+1; os > 1 && c[os-1] == 0; ) os--; for (os = len+1; os > 1 && c[os-1] == 0; ) os--;
SASSERT(os > 0 && os <= len+1); SASSERT(os > 0 && os <= len+1);
trace_nl(c, os); trace_nl(c, os);
return true; // return k != 0? What would MSBignum return? return true; // return k != 0?
} }
bool mpn_manager::sub(mpn_digit const * a, size_t const lnga, bool mpn_manager::sub(mpn_digit const * a, size_t const lnga,
@ -173,6 +162,7 @@ bool mpn_manager::div(mpn_digit const * numer, size_t const lnum,
quot[i] = 0; quot[i] = 0;
for (size_t i = 0; i < lden; i++) for (size_t i = 0; i < lden; i++)
rem[i] = (i < lnum) ? numer[i] : 0; rem[i] = (i < lnum) ? numer[i] : 0;
MPN_END_CRITICAL();
return false; return false;
} }
@ -181,8 +171,8 @@ bool mpn_manager::div(mpn_digit const * numer, size_t const lnum,
if (denom[i] != zero) all_zero = false; if (denom[i] != zero) all_zero = false;
if (all_zero) { if (all_zero) {
// Division by 0. What would the MSBignum divide function do?
UNREACHABLE(); UNREACHABLE();
MPN_END_CRITICAL();
return res; return res;
} }
@ -202,12 +192,12 @@ bool mpn_manager::div(mpn_digit const * numer, size_t const lnum,
if (lden == 1) if (lden == 1)
res = div_1(u, v[0], quot); res = div_1(u, v[0], quot);
else else
res = div_n(u, v, quot, rem); res = div_n(u, v, quot, rem, t_ms, t_ab);
div_unnormalize(u, v, d, rem); div_unnormalize(u, v, d, rem);
} }
// STRACE("mpn_dbg", display_raw(tout, quot, lnum - lden + 1); tout << ", "; // TRACE("mpn_dbg", display_raw(tout, quot, lnum - lden + 1); tout << ", ";
// display_raw(tout, rem, lden); tout << std::endl; ); // display_raw(tout, rem, lden); tout << std::endl; );
trace_nl(quot, lnum-lden+1); trace_nl(quot, lnum-lden+1);
trace(numer, lnum, denom, lden, "%"); trace(numer, lnum, denom, lden, "%");
@ -234,8 +224,7 @@ size_t mpn_manager::div_normalize(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_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,16 +250,13 @@ size_t mpn_manager::div_normalize(mpn_digit const * numer, size_t const lnum,
n_denom[0] = denom[0] << d; n_denom[0] = denom[0] << d;
} }
STRACE("mpn_norm", tout << "Normalized: n_numer="; display_raw(tout, n_numer.c_ptr(), n_numer.size()); TRACE("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];
@ -280,13 +266,10 @@ 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,20 +290,19 @@ bool mpn_manager::div_1(mpn_sbuffer & numer, mpn_digit const denom,
quot[j-1]--; quot[j-1]--;
numer[j] = numer[j-1] + denom; numer[j] = numer[j-1] + denom;
} }
STRACE("mpn_div1", tout << "j=" << j << " q_hat=" << q_hat << " r_hat=" << r_hat; TRACE("mpn_div1", tout << "j=" << j << " q_hat=" << q_hat << " r_hat=" << r_hat;
tout << " ms=" << ms; tout << " ms=" << ms;
tout << " new numer="; display_raw(tout, numer.c_ptr(), numer.size()); tout << " new numer="; display_raw(tout, numer.c_ptr(), numer.size());
tout << " borrow=" << borrow; tout << " borrow=" << borrow;
tout << std::endl; ); tout << std::endl; );
} }
MPN_END_CRITICAL(); return true; // return rem != 0?
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(); mpn_sbuffer & ms, mpn_sbuffer & ab) const {
SASSERT(denom.size() > 1); SASSERT(denom.size() > 1);
// This is essentially Knuth's Algorithm D. // This is essentially Knuth's Algorithm D.
@ -329,7 +311,7 @@ bool mpn_manager::div_n(mpn_sbuffer & numer, mpn_sbuffer const & denom,
SASSERT(numer.size() == m+n); SASSERT(numer.size() == m+n);
t_ms.resize(n+1); ms.resize(n+1);
mpn_double_digit q_hat, temp, r_hat; mpn_double_digit q_hat, temp, r_hat;
mpn_digit borrow; mpn_digit borrow;
@ -349,37 +331,30 @@ bool mpn_manager::div_n(mpn_sbuffer & numer, mpn_sbuffer const & denom,
// Replace numer[j+n]...numer[j] with // Replace numer[j+n]...numer[j] with
// numer[j+n]...numer[j] - q * (denom[n-1]...denom[0]) // numer[j+n]...numer[j] - q * (denom[n-1]...denom[0])
mpn_digit q_hat_small = (mpn_digit)q_hat; mpn_digit q_hat_small = (mpn_digit)q_hat;
#ifdef Z3DEBUG mul(&q_hat_small, 1, denom.c_ptr(), n, ms.c_ptr());
trace_enabled = false; sub(&numer[j], n+1, ms.c_ptr(), n+1, &numer[j], &borrow);
#endif
mul(&q_hat_small, 1, denom.c_ptr(), n, t_ms.c_ptr());
sub(&numer[j], n+1, t_ms.c_ptr(), n+1, &numer[j], &borrow);
quot[j] = q_hat_small; quot[j] = q_hat_small;
if (borrow) { if (borrow) {
quot[j]--; quot[j]--;
t_ab.resize(n+2); ab.resize(n+2);
size_t real_size; size_t real_size;
add(denom.c_ptr(), n, &numer[j], n+1, t_ab.c_ptr(), n+2, &real_size); add(denom.c_ptr(), n, &numer[j], n+1, ab.c_ptr(), n+2, &real_size);
for (size_t i = 0; i < n+1; i++) for (size_t i = 0; i < n+1; i++)
numer[j+i] = t_ab[i]; numer[j+i] = ab[i];
} }
#ifdef Z3DEBUG TRACE("mpn_div", tout << "q_hat=" << q_hat << " r_hat=" << r_hat;
trace_enabled = true; tout << " ms="; display_raw(tout, ms.c_ptr(), n);
#endif tout << " new numer="; display_raw(tout, numer.c_ptr(), m+n+1);
STRACE("mpn_div", tout << "q_hat=" << q_hat << " r_hat=" << r_hat; tout << " borrow=" << borrow;
tout << " t_ms="; display_raw(tout, t_ms.c_ptr(), n); tout << std::endl; );
tout << " new numer="; display_raw(tout, numer.c_ptr(), m+n+1);
tout << " borrow=" << borrow;
tout << std::endl; );
} }
MPN_END_CRITICAL(); return true; // return rem != 0?
return true; // return rem != 0 or something like that?
} }
char * mpn_manager::to_string(mpn_digit const * a, size_t const lng, char * buf, size_t const lbuf) const { char * mpn_manager::to_string(mpn_digit const * a, size_t const lng, char * buf, size_t const lbuf) const {
SASSERT(buf && lbuf > 0); SASSERT(buf && lbuf > 0);
STRACE("mpn_to_string", tout << "[mpn] to_string "; display_raw(tout, a, lng); tout << " == "; ); TRACE("mpn_to_string", tout << "[mpn] to_string "; display_raw(tout, a, lng); tout << " == "; );
if (lng == 1) { if (lng == 1) {
#ifdef _WINDOWS #ifdef _WINDOWS
@ -412,7 +387,7 @@ char * mpn_manager::to_string(mpn_digit const * a, size_t const lng, char * buf,
std::swap(buf[i], buf[j-i]); std::swap(buf[i], buf[j-i]);
} }
STRACE("mpn_to_string", tout << buf << std::endl; ); TRACE("mpn_to_string", tout << buf << std::endl; );
return buf; return buf;
} }
@ -427,23 +402,23 @@ void mpn_manager::trace(mpn_digit const * a, size_t const lnga,
mpn_digit const * b, size_t const lngb, mpn_digit const * b, size_t const lngb,
const char * op) const { const char * op) const {
#ifdef Z3DEBUG #ifdef Z3DEBUG
if (trace_enabled) char char_buf[4096];
STRACE("mpn", tout << "[mpn] " << to_string(a, lnga, char_buf, sizeof(char_buf)); TRACE("mpn", tout << "[mpn] " << to_string(a, lnga, char_buf, sizeof(char_buf));
tout << " " << op << " " << to_string(b, lngb, char_buf, sizeof(char_buf)); tout << " " << op << " " << to_string(b, lngb, char_buf, sizeof(char_buf));
tout << " == "; ); tout << " == "; );
#endif #endif
} }
void mpn_manager::trace(mpn_digit const * a, size_t const lnga) const { void mpn_manager::trace(mpn_digit const * a, size_t const lnga) const {
#ifdef Z3DEBUG #ifdef Z3DEBUG
if (trace_enabled) char char_buf[4096];
STRACE("mpn", tout << to_string(a, lnga, char_buf, sizeof(char_buf)); ); TRACE("mpn", tout << to_string(a, lnga, char_buf, sizeof(char_buf)); );
#endif #endif
} }
void mpn_manager::trace_nl(mpn_digit const * a, size_t const lnga) const { void mpn_manager::trace_nl(mpn_digit const * a, size_t const lnga) const {
#ifdef Z3DEBUG #ifdef Z3DEBUG
if (trace_enabled) char char_buf[4096];
STRACE("mpn", tout << to_string(a, lnga, char_buf, sizeof(char_buf)) << std::endl; ); TRACE("mpn", tout << to_string(a, lnga, char_buf, sizeof(char_buf)) << std::endl; );
#endif #endif
} }

12
src/util/mpn.h
View file

@ -28,8 +28,8 @@ typedef unsigned int mpn_digit;
class mpn_manager { class mpn_manager {
omp_nest_lock_t m_lock; omp_nest_lock_t m_lock;
#define MPN_BEGIN_CRITICAL() omp_set_nest_lock(&const_cast<omp_nest_lock_t>(m_lock)); #define MPN_BEGIN_CRITICAL() omp_set_nest_lock(&m_lock);
#define MPN_END_CRITICAL() omp_unset_nest_lock(&const_cast<omp_nest_lock_t>(m_lock)); #define MPN_END_CRITICAL() omp_unset_nest_lock(&m_lock);
public: public:
mpn_manager(); mpn_manager();
@ -100,12 +100,8 @@ private:
mpn_digit * quot) const; mpn_digit * quot) const;
bool div_n(mpn_sbuffer & numer, mpn_sbuffer const & denom, bool div_n(mpn_sbuffer & numer, mpn_sbuffer const & denom,
mpn_digit * quot, mpn_digit * rem); mpn_digit * quot, mpn_digit * rem,
mpn_sbuffer & ms, mpn_sbuffer & ab) const;
#ifdef Z3DEBUG
mutable char char_buf[4096];
bool trace_enabled;
#endif
void trace(mpn_digit const * a, size_t const lnga, void trace(mpn_digit const * a, size_t const lnga,
mpn_digit const * b, size_t const lngb, mpn_digit const * b, size_t const lngb,