3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00

don't use mp[zq] synchronized mode if OpenMP mode is disabled

This commit is contained in:
Nuno Lopes 2018-07-14 20:44:35 +01:00
parent 7d20fbb280
commit b88596283f
10 changed files with 97 additions and 41 deletions

View file

@ -376,9 +376,11 @@ void mpff_manager::set(mpff & n, unsynch_mpz_manager & m, mpz const & v) {
set_core(n, m, v); set_core(n, m, v);
} }
#ifndef _NO_OMP_
void mpff_manager::set(mpff & n, synch_mpz_manager & m, mpz const & v) { void mpff_manager::set(mpff & n, synch_mpz_manager & m, mpz const & v) {
set_core(n, m, v); set_core(n, m, v);
} }
#endif
template<bool SYNCH> template<bool SYNCH>
void mpff_manager::set_core(mpff & n, mpq_manager<SYNCH> & m, mpq const & v) { void mpff_manager::set_core(mpff & n, mpq_manager<SYNCH> & m, mpq const & v) {
@ -397,9 +399,11 @@ void mpff_manager::set(mpff & n, unsynch_mpq_manager & m, mpq const & v) {
set_core(n, m, v); set_core(n, m, v);
} }
#ifndef _NO_OMP_
void mpff_manager::set(mpff & n, synch_mpq_manager & m, mpq const & v) { void mpff_manager::set(mpff & n, synch_mpq_manager & m, mpq const & v) {
set_core(n, m, v); set_core(n, m, v);
} }
#endif
bool mpff_manager::eq(mpff const & a, mpff const & b) const { bool mpff_manager::eq(mpff const & a, mpff const & b) const {
if (is_zero(a) && is_zero(b)) if (is_zero(a) && is_zero(b))
@ -1077,9 +1081,11 @@ void mpff_manager::significand(mpff const & n, unsynch_mpz_manager & m, mpz & t)
significand_core(n, m, t); significand_core(n, m, t);
} }
#ifndef _NO_OMP_
void mpff_manager::significand(mpff const & n, synch_mpz_manager & m, mpz & t) { void mpff_manager::significand(mpff const & n, synch_mpz_manager & m, mpz & t) {
significand_core(n, m, t); significand_core(n, m, t);
} }
#endif
template<bool SYNCH> template<bool SYNCH>
void mpff_manager::to_mpz_core(mpff const & n, mpz_manager<SYNCH> & m, mpz & t) { void mpff_manager::to_mpz_core(mpff const & n, mpz_manager<SYNCH> & m, mpz & t) {
@ -1109,9 +1115,11 @@ void mpff_manager::to_mpz(mpff const & n, unsynch_mpz_manager & m, mpz & t) {
to_mpz_core(n, m, t); to_mpz_core(n, m, t);
} }
#ifndef _NO_OMP_
void mpff_manager::to_mpz(mpff const & n, synch_mpz_manager & m, mpz & t) { void mpff_manager::to_mpz(mpff const & n, synch_mpz_manager & m, mpz & t) {
to_mpz_core(n, m, t); to_mpz_core(n, m, t);
} }
#endif
template<bool SYNCH> template<bool SYNCH>
void mpff_manager::to_mpq_core(mpff const & n, mpq_manager<SYNCH> & m, mpq & t) { void mpff_manager::to_mpq_core(mpff const & n, mpq_manager<SYNCH> & m, mpq & t) {
@ -1154,9 +1162,11 @@ void mpff_manager::to_mpq(mpff const & n, unsynch_mpq_manager & m, mpq & t) {
to_mpq_core(n, m, t); to_mpq_core(n, m, t);
} }
#ifndef _NO_OMP_
void mpff_manager::to_mpq(mpff const & n, synch_mpq_manager & m, mpq & t) { void mpff_manager::to_mpq(mpff const & n, synch_mpq_manager & m, mpq & t) {
to_mpq_core(n, m, t); to_mpq_core(n, m, t);
} }
#endif
void mpff_manager::display_raw(std::ostream & out, mpff const & n) const { void mpff_manager::display_raw(std::ostream & out, mpff const & n) const {
if (is_neg(n)) if (is_neg(n))

View file

@ -58,9 +58,14 @@ class mpz;
class mpq; class mpq;
template<bool SYNCH> class mpz_manager; template<bool SYNCH> class mpz_manager;
template<bool SYNCH> class mpq_manager; template<bool SYNCH> class mpq_manager;
#ifndef _NO_OMP_
typedef mpz_manager<true> synch_mpz_manager; typedef mpz_manager<true> synch_mpz_manager;
typedef mpz_manager<false> unsynch_mpz_manager;
typedef mpq_manager<true> synch_mpq_manager; typedef mpq_manager<true> synch_mpq_manager;
#else
typedef mpz_manager<false> synch_mpz_manager;
typedef mpq_manager<false> synch_mpq_manager;
#endif
typedef mpz_manager<false> unsynch_mpz_manager;
typedef mpq_manager<false> unsynch_mpq_manager; typedef mpq_manager<false> unsynch_mpq_manager;
class mpff_manager { class mpff_manager {
@ -213,7 +218,9 @@ public:
\brief Return the significand as a mpz numeral. \brief Return the significand as a mpz numeral.
*/ */
void significand(mpff const & n, unsynch_mpz_manager & m, mpz & r); void significand(mpff const & n, unsynch_mpz_manager & m, mpz & r);
#ifndef _NO_OMP_
void significand(mpff const & n, synch_mpz_manager & m, mpz & r); void significand(mpff const & n, synch_mpz_manager & m, mpz & r);
#endif
/** /**
\brief Return true if n is negative \brief Return true if n is negative
@ -378,9 +385,11 @@ public:
void set(mpff & n, int64_t num, uint64_t den); void set(mpff & n, int64_t num, uint64_t den);
void set(mpff & n, mpff const & v); void set(mpff & n, mpff const & v);
void set(mpff & n, unsynch_mpz_manager & m, mpz const & v); void set(mpff & n, unsynch_mpz_manager & m, mpz const & v);
void set(mpff & n, synch_mpz_manager & m, mpz const & v);
void set(mpff & n, unsynch_mpq_manager & m, mpq const & v); void set(mpff & n, unsynch_mpq_manager & m, mpq const & v);
#ifndef _NO_OMP_
void set(mpff & n, synch_mpq_manager & m, mpq const & v); void set(mpff & n, synch_mpq_manager & m, mpq const & v);
void set(mpff & n, synch_mpz_manager & m, mpz const & v);
#endif
void set_plus_epsilon(mpff & n); void set_plus_epsilon(mpff & n);
void set_minus_epsilon(mpff & n); void set_minus_epsilon(mpff & n);
void set_max(mpff & n); void set_max(mpff & n);
@ -420,6 +429,7 @@ public:
*/ */
void to_mpz(mpff const & n, unsynch_mpz_manager & m, mpz & t); void to_mpz(mpff const & n, unsynch_mpz_manager & m, mpz & t);
#ifndef _NO_OMP_
/** /**
\brief Convert n into a mpz numeral. \brief Convert n into a mpz numeral.
@ -428,6 +438,7 @@ public:
\remark if exponent(n) is too big, we may run out of memory. \remark if exponent(n) is too big, we may run out of memory.
*/ */
void to_mpz(mpff const & n, synch_mpz_manager & m, mpz & t); void to_mpz(mpff const & n, synch_mpz_manager & m, mpz & t);
#endif
/** /**
\brief Convert n into a mpq numeral. \brief Convert n into a mpq numeral.
@ -436,12 +447,14 @@ public:
*/ */
void to_mpq(mpff const & n, unsynch_mpq_manager & m, mpq & t); void to_mpq(mpff const & n, unsynch_mpq_manager & m, mpq & t);
#ifndef _NO_OMP_
/** /**
\brief Convert n into a mpq numeral. \brief Convert n into a mpq numeral.
\remark if exponent(n) is too big, we may run out of memory. \remark if exponent(n) is too big, we may run out of memory.
*/ */
void to_mpq(mpff const & n, synch_mpq_manager & m, mpq & t); void to_mpq(mpff const & n, synch_mpq_manager & m, mpq & t);
#endif
/** /**
\brief Return n as an int64. \brief Return n as an int64.

View file

@ -272,9 +272,11 @@ void mpfx_manager::set(mpfx & n, unsynch_mpz_manager & m, mpz const & v) {
set_core(n, m, v); set_core(n, m, v);
} }
#ifndef _NO_OMP_
void mpfx_manager::set(mpfx & n, synch_mpz_manager & m, mpz const & v) { void mpfx_manager::set(mpfx & n, synch_mpz_manager & m, mpz const & v) {
set_core(n, m, v); set_core(n, m, v);
} }
#endif
template<bool SYNCH> template<bool SYNCH>
void mpfx_manager::set_core(mpfx & n, mpq_manager<SYNCH> & m, mpq const & v) { void mpfx_manager::set_core(mpfx & n, mpq_manager<SYNCH> & m, mpq const & v) {
@ -309,9 +311,11 @@ void mpfx_manager::set(mpfx & n, unsynch_mpq_manager & m, mpq const & v) {
set_core(n, m, v); set_core(n, m, v);
} }
#ifndef _NO_OMP_
void mpfx_manager::set(mpfx & n, synch_mpq_manager & m, mpq const & v) { void mpfx_manager::set(mpfx & n, synch_mpq_manager & m, mpq const & v) {
set_core(n, m, v); set_core(n, m, v);
} }
#endif
bool mpfx_manager::eq(mpfx const & a, mpfx const & b) const { bool mpfx_manager::eq(mpfx const & a, mpfx const & b) const {
if (is_zero(a) && is_zero(b)) if (is_zero(a) && is_zero(b))
@ -714,9 +718,11 @@ void mpfx_manager::to_mpz(mpfx const & n, unsynch_mpz_manager & m, mpz & t) {
to_mpz_core(n, m, t); to_mpz_core(n, m, t);
} }
#ifndef _NO_OMP_
void mpfx_manager::to_mpz(mpfx const & n, synch_mpz_manager & m, mpz & t) { void mpfx_manager::to_mpz(mpfx const & n, synch_mpz_manager & m, mpz & t) {
to_mpz_core(n, m, t); to_mpz_core(n, m, t);
} }
#endif
template<bool SYNCH> template<bool SYNCH>
void mpfx_manager::to_mpq_core(mpfx const & n, mpq_manager<SYNCH> & m, mpq & t) { void mpfx_manager::to_mpq_core(mpfx const & n, mpq_manager<SYNCH> & m, mpq & t) {
@ -738,9 +744,11 @@ void mpfx_manager::to_mpq(mpfx const & n, unsynch_mpq_manager & m, mpq & t) {
to_mpq_core(n, m, t); to_mpq_core(n, m, t);
} }
#ifndef _NO_OMP_
void mpfx_manager::to_mpq(mpfx const & n, synch_mpq_manager & m, mpq & t) { void mpfx_manager::to_mpq(mpfx const & n, synch_mpq_manager & m, mpq & t) {
to_mpq_core(n, m, t); to_mpq_core(n, m, t);
} }
#endif
void mpfx_manager::display_raw(std::ostream & out, mpfx const & n) const { void mpfx_manager::display_raw(std::ostream & out, mpfx const & n) const {
if (is_neg(n)) if (is_neg(n))

View file

@ -51,9 +51,14 @@ class mpz;
class mpq; class mpq;
template<bool SYNCH> class mpz_manager; template<bool SYNCH> class mpz_manager;
template<bool SYNCH> class mpq_manager; template<bool SYNCH> class mpq_manager;
#ifndef _NO_OMP_
typedef mpz_manager<true> synch_mpz_manager; typedef mpz_manager<true> synch_mpz_manager;
typedef mpz_manager<false> unsynch_mpz_manager;
typedef mpq_manager<true> synch_mpq_manager; typedef mpq_manager<true> synch_mpq_manager;
#else
typedef mpz_manager<false> synch_mpz_manager;
typedef mpq_manager<false> synch_mpq_manager;
#endif
typedef mpz_manager<false> unsynch_mpz_manager;
typedef mpq_manager<false> unsynch_mpq_manager; typedef mpq_manager<false> unsynch_mpq_manager;
class mpfx_manager { class mpfx_manager {
@ -312,9 +317,11 @@ public:
void set(mpfx & n, int64_t num, uint64_t den); void set(mpfx & n, int64_t num, uint64_t den);
void set(mpfx & n, mpfx const & v); void set(mpfx & n, mpfx const & v);
void set(mpfx & n, unsynch_mpz_manager & m, mpz const & v); void set(mpfx & n, unsynch_mpz_manager & m, mpz const & v);
void set(mpfx & n, synch_mpz_manager & m, mpz const & v);
void set(mpfx & n, unsynch_mpq_manager & m, mpq const & v); void set(mpfx & n, unsynch_mpq_manager & m, mpq const & v);
#ifndef _NO_OMP_
void set(mpfx & n, synch_mpz_manager & m, mpz const & v);
void set(mpfx & n, synch_mpq_manager & m, mpq const & v); void set(mpfx & n, synch_mpq_manager & m, mpq const & v);
#endif
/** /**
\brief Set n to the smallest representable numeral greater than zero. \brief Set n to the smallest representable numeral greater than zero.
@ -359,22 +366,26 @@ public:
*/ */
void to_mpz(mpfx const & n, unsynch_mpz_manager & m, mpz & t); void to_mpz(mpfx const & n, unsynch_mpz_manager & m, mpz & t);
#ifndef _NO_OMP_
/** /**
\brief Convert n into a mpz numeral. \brief Convert n into a mpz numeral.
\pre is_int(n) \pre is_int(n)
*/ */
void to_mpz(mpfx const & n, synch_mpz_manager & m, mpz & t); void to_mpz(mpfx const & n, synch_mpz_manager & m, mpz & t);
#endif
/** /**
\brief Convert n into a mpq numeral. \brief Convert n into a mpq numeral.
*/ */
void to_mpq(mpfx const & n, unsynch_mpq_manager & m, mpq & t); void to_mpq(mpfx const & n, unsynch_mpq_manager & m, mpq & t);
#ifndef _NO_OMP_
/** /**
\brief Convert n into a mpq numeral. \brief Convert n into a mpq numeral.
*/ */
void to_mpq(mpfx const & n, synch_mpq_manager & m, mpq & t); void to_mpq(mpfx const & n, synch_mpq_manager & m, mpq & t);
#endif
/** /**
\brief Return the biggest k s.t. 2^k <= a. \brief Return the biggest k s.t. 2^k <= a.

View file

@ -26,12 +26,12 @@ mpq_manager<SYNCH>::mpq_manager() {
template<bool SYNCH> template<bool SYNCH>
mpq_manager<SYNCH>::~mpq_manager() { mpq_manager<SYNCH>::~mpq_manager() {
del(m_n_tmp); del(m_tmp1);
del(m_add_tmp1); del(m_tmp2);
del(m_add_tmp2); del(m_tmp3);
del(m_lt_tmp1); del(m_tmp4);
del(m_lt_tmp2); del(m_q_tmp1);
del(m_addmul_tmp); del(m_q_tmp2);
} }
@ -68,9 +68,9 @@ bool mpq_manager<SYNCH>::rat_lt(mpq const & a, mpq const & b) {
return r; return r;
} }
else { else {
mul(na, db, m_lt_tmp1); mul(na, db, m_q_tmp1);
mul(nb, da, m_lt_tmp2); mul(nb, da, m_q_tmp2);
return lt(m_lt_tmp1, m_lt_tmp2); return lt(m_q_tmp1, m_q_tmp2);
} }
} }
@ -384,8 +384,7 @@ void mpq_manager<SYNCH>::rat_mul(mpq const & a, mpq const & b, mpq & c) {
del(tmp2); del(tmp2);
} }
else { else {
mpz& g1 = m_n_tmp, &g2 = m_addmul_tmp.m_num, &tmp1 = m_add_tmp1, &tmp2 = m_add_tmp2; rat_mul(a, b, c, m_tmp1, m_tmp2, m_tmp3, m_tmp4);
rat_mul(a, b, c, g1, g2, tmp1, tmp2);
} }
STRACE("rat_mpq", tout << to_string(c) << "\n";); STRACE("rat_mpq", tout << to_string(c) << "\n";);
} }
@ -402,8 +401,7 @@ void mpq_manager<SYNCH>::rat_add(mpq const & a, mpq const & b, mpq & c) {
del(g); del(g);
} }
else { else {
mpz& g = m_n_tmp, &tmp1 = m_add_tmp1, &tmp2 = m_add_tmp2, &tmp3 = m_addmul_tmp.m_num; lin_arith_op<false>(a, b, c, m_tmp1, m_tmp2, m_tmp3, m_tmp4);
lin_arith_op<false>(a, b, c, g, tmp1, tmp2, tmp3);
} }
STRACE("rat_mpq", tout << to_string(c) << "\n";); STRACE("rat_mpq", tout << to_string(c) << "\n";);
} }
@ -420,13 +418,13 @@ void mpq_manager<SYNCH>::rat_sub(mpq const & a, mpq const & b, mpq & c) {
del(g); del(g);
} }
else { else {
mpz& g = m_n_tmp, &tmp1 = m_add_tmp1, &tmp2 = m_add_tmp2, &tmp3 = m_addmul_tmp.m_num; lin_arith_op<true>(a, b, c, m_tmp1, m_tmp2, m_tmp3, m_tmp4);
lin_arith_op<true>(a, b, c, g, tmp1, tmp2, tmp3);
} }
STRACE("rat_mpq", tout << to_string(c) << "\n";); STRACE("rat_mpq", tout << to_string(c) << "\n";);
} }
#ifndef _NO_OMP_
template class mpq_manager<true>; template class mpq_manager<true>;
#endif
template class mpq_manager<false>; template class mpq_manager<false>;

View file

@ -41,12 +41,12 @@ inline void swap(mpq & m1, mpq & m2) { m1.swap(m2); }
template<bool SYNCH = true> template<bool SYNCH = true>
class mpq_manager : public mpz_manager<SYNCH> { class mpq_manager : public mpz_manager<SYNCH> {
mpz m_n_tmp; mpz m_tmp1;
mpz m_add_tmp1; mpz m_tmp2;
mpz m_add_tmp2; mpz m_tmp3;
mpq m_addmul_tmp; mpz m_tmp4;
mpq m_lt_tmp1; mpq m_q_tmp1;
mpq m_lt_tmp2; mpq m_q_tmp2;
void reset_denominator(mpq & a) { void reset_denominator(mpq & a) {
del(a.m_den); del(a.m_den);
@ -66,11 +66,11 @@ class mpq_manager : public mpz_manager<SYNCH> {
del(tmp); del(tmp);
} }
else { else {
gcd(a.m_num, a.m_den, m_n_tmp); gcd(a.m_num, a.m_den, m_tmp1);
if (is_one(m_n_tmp)) if (is_one(m_tmp1))
return; return;
div(a.m_num, m_n_tmp, a.m_num); div(a.m_num, m_tmp1, a.m_num);
div(a.m_den, m_n_tmp, a.m_den); div(a.m_den, m_tmp1, a.m_den);
} }
} }
@ -87,9 +87,9 @@ class mpq_manager : public mpz_manager<SYNCH> {
del(tmp1); del(tmp1);
} }
else { else {
mul(b, a.m_den, m_add_tmp1); mul(b, a.m_den, m_tmp1);
set(c.m_den, a.m_den); set(c.m_den, a.m_den);
add(a.m_num, m_add_tmp1, c.m_num); add(a.m_num, m_tmp1, c.m_num);
normalize(c); normalize(c);
} }
STRACE("rat_mpq", tout << to_string(c) << "\n";); STRACE("rat_mpq", tout << to_string(c) << "\n";);
@ -320,8 +320,8 @@ public:
del(tmp); del(tmp);
} }
else { else {
mul(b,c,m_addmul_tmp); mul(b, c, m_q_tmp1);
add(a, m_addmul_tmp, d); add(a, m_q_tmp1, d);
} }
} }
} }
@ -342,8 +342,8 @@ public:
del(tmp); del(tmp);
} }
else { else {
mul(b,c,m_addmul_tmp); mul(b,c, m_q_tmp1);
add(a, m_addmul_tmp, d); add(a, m_q_tmp1, d);
} }
} }
} }
@ -365,8 +365,8 @@ public:
del(tmp); del(tmp);
} }
else { else {
mul(b,c,m_addmul_tmp); mul(b,c, m_q_tmp1);
sub(a, m_addmul_tmp, d); sub(a, m_q_tmp1, d);
} }
} }
} }
@ -387,8 +387,8 @@ public:
del(tmp); del(tmp);
} }
else { else {
mul(b,c,m_addmul_tmp); mul(b,c, m_q_tmp1);
sub(a, m_addmul_tmp, d); sub(a, m_q_tmp1, d);
} }
} }
} }
@ -816,7 +816,11 @@ public:
bool is_even(mpq const & a) { return is_int(a) && is_even(a.m_num); } bool is_even(mpq const & a) { return is_int(a) && is_even(a.m_num); }
}; };
#ifndef _NO_OMP_
typedef mpq_manager<true> synch_mpq_manager; typedef mpq_manager<true> synch_mpq_manager;
#else
typedef mpq_manager<false> synch_mpq_manager;
#endif
typedef mpq_manager<false> unsynch_mpq_manager; typedef mpq_manager<false> unsynch_mpq_manager;
typedef _scoped_numeral<unsynch_mpq_manager> scoped_mpq; typedef _scoped_numeral<unsynch_mpq_manager> scoped_mpq;

View file

@ -39,5 +39,7 @@ std::string mpq_inf_manager<SYNCH>::to_string(mpq_inf const & a) {
} }
#ifndef _NO_OMP_
template class mpq_inf_manager<true>; template class mpq_inf_manager<true>;
#endif
template class mpq_inf_manager<false>; template class mpq_inf_manager<false>;

View file

@ -279,7 +279,11 @@ public:
mpq_manager<SYNCH>& get_mpq_manager() { return m; } mpq_manager<SYNCH>& get_mpq_manager() { return m; }
}; };
#ifndef _NO_OMP_
typedef mpq_inf_manager<true> synch_mpq_inf_manager; typedef mpq_inf_manager<true> synch_mpq_inf_manager;
#else
typedef mpq_inf_manager<false> synch_mpq_inf_manager;
#endif
typedef mpq_inf_manager<false> unsynch_mpq_inf_manager; typedef mpq_inf_manager<false> unsynch_mpq_inf_manager;
#endif #endif

View file

@ -2369,5 +2369,7 @@ bool mpz_manager<SYNCH>::divides(mpz const & a, mpz const & b) {
return r; return r;
} }
#ifndef _NO_OMP_
template class mpz_manager<true>; template class mpz_manager<true>;
#endif
template class mpz_manager<false>; template class mpz_manager<false>;

View file

@ -692,7 +692,11 @@ public:
bool decompose(mpz const & n, svector<digit_t> & digits); bool decompose(mpz const & n, svector<digit_t> & digits);
}; };
#ifndef _NO_OMP_
typedef mpz_manager<true> synch_mpz_manager; typedef mpz_manager<true> synch_mpz_manager;
#else
typedef mpz_manager<false> synch_mpz_manager;
#endif
typedef mpz_manager<false> unsynch_mpz_manager; typedef mpz_manager<false> unsynch_mpz_manager;
typedef _scoped_numeral<unsynch_mpz_manager> scoped_mpz; typedef _scoped_numeral<unsynch_mpz_manager> scoped_mpz;