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

fix NO_GMP compilation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-03 16:22:29 -07:00
parent c7e1d59b19
commit cb7fb524b2
2 changed files with 22 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/util/mpz.cpp
View file

@ -356,7 +356,7 @@ void mpz_manager<SYNCH>::set_big_ui64(mpz & c, uint64_t v) {
#ifdef _MP_GMP #ifdef _MP_GMP
template<bool SYNCH> template<bool SYNCH>
mpz_manager<SYNCH>::ensure_mpz_t(mpz_const& a) { mpz_manager<SYNCH>::ensure_mpz_t(mpz const& a) {
if (is_small(a)) { if (is_small(a)) {
m_result = &m_local; m_result = &m_local;
mpz_init(m_local); mpz_init(m_local);
@ -735,7 +735,7 @@ void mpz_manager<SYNCH>::big_add(mpz const & a, mpz const & b, mpz & c) {
big_add_sub<false>(a, b, c); big_add_sub<false>(a, b, c);
#else #else
// GMP version // GMP version
ensure_mpz a1(a), b1(b); ensure_mpz_t a1(a), b1(b);
mk_big(c); mk_big(c);
mpz_add(*c.m_ptr, a1(), b1()); mpz_add(*c.m_ptr, a1(), b1());
#endif #endif
@ -747,7 +747,7 @@ void mpz_manager<SYNCH>::big_sub(mpz const & a, mpz const & b, mpz & c) {
big_add_sub<true>(a, b, c); big_add_sub<true>(a, b, c);
#else #else
// GMP version // GMP version
ensure_mpz a1(a), b1(b); ensure_mpz_t a1(a), b1(b);
mk_big(c); mk_big(c);
mpz_sub(*c.m_ptr, a1(), b1()); mpz_sub(*c.m_ptr, a1(), b1());
#endif #endif
@ -770,7 +770,7 @@ void mpz_manager<SYNCH>::big_mul(mpz const & a, mpz const & b, mpz & c) {
del(tmp); del(tmp);
#else #else
// GMP version // GMP version
ensure_mpz a1(a), b1(b); ensure_mpz_t a1(a), b1(b);
mk_big(c); mk_big(c);
mpz_mul(*c.m_ptr, a1(), b1()); mpz_mul(*c.m_ptr, a1(), b1());
#endif #endif
@ -783,7 +783,7 @@ void mpz_manager<SYNCH>::big_div_rem(mpz const & a, mpz const & b, mpz & q, mpz
quot_rem_core<QUOT_AND_REM>(a, b, q, r); quot_rem_core<QUOT_AND_REM>(a, b, q, r);
#else #else
// GMP version // GMP version
ensure_mpz a1(a), b1(b); ensure_mpz_t a1(a), b1(b);
mk_big(q); mk_big(q);
mk_big(r); mk_big(r);
mpz_tdiv_qr(*q.m_ptr, *r.m_ptr, a1(), b1()); mpz_tdiv_qr(*q.m_ptr, *r.m_ptr, a1(), b1());
@ -837,7 +837,7 @@ void mpz_manager<SYNCH>::big_div(mpz const & a, mpz const & b, mpz & c) {
del(dummy); del(dummy);
#else #else
// GMP version // GMP version
ensure_mpz a1(a), b1(b); ensure_mpz_t a1(a), b1(b);
mk_big(c); mk_big(c);
mpz_tdiv_q(*c.m_ptr, a1(), b1()); mpz_tdiv_q(*c.m_ptr, a1(), b1());
#endif #endif
@ -852,7 +852,7 @@ void mpz_manager<SYNCH>::big_rem(mpz const & a, mpz const & b, mpz & c) {
del(dummy); del(dummy);
#else #else
// GMP version // GMP version
ensure_mpz a1(a), b1(b); ensure_mpz_t a1(a), b1(b);
mk_big(c); mk_big(c);
mpz_tdiv_r(*c.m_ptr, a1(), b1()); mpz_tdiv_r(*c.m_ptr, a1(), b1());
#endif #endif
@ -872,7 +872,7 @@ void mpz_manager<SYNCH>::gcd(mpz const & a, mpz const & b, mpz & c) {
} }
else { else {
#ifdef _MP_GMP #ifdef _MP_GMP
ensure_mpz a1(a), b1(b); ensure_mpz_t a1(a), b1(b);
mk_big(c); mk_big(c);
mpz_gcd(*c.m_ptr, a1(), b1()); mpz_gcd(*c.m_ptr, a1(), b1());
return; return;
@ -1357,7 +1357,7 @@ void mpz_manager<SYNCH>::bitwise_or(mpz const & a, mpz const & b, mpz & c) {
} }
del(a1); del(b1); del(a2); del(b2); del(m); del(tmp); del(a1); del(b1); del(a2); del(b2); del(m); del(tmp);
#else #else
ensure_mpz a1(a), b1(b); ensure_mpz_t a1(a), b1(b);
mk_big(c); mk_big(c);
mpz_ior(*c.m_ptr, a1(), b1()); mpz_ior(*c.m_ptr, a1(), b1());
#endif #endif
@ -1392,7 +1392,7 @@ void mpz_manager<SYNCH>::bitwise_and(mpz const & a, mpz const & b, mpz & c) {
} }
del(a1); del(b1); del(a2); del(b2); del(m); del(tmp); del(a1); del(b1); del(a2); del(b2); del(m); del(tmp);
#else #else
ensure_mpz a1(a), b1(b); ensure_mpz_t a1(a), b1(b);
mk_big(c); mk_big(c);
mpz_and(*c.m_ptr, a1(), b1()); mpz_and(*c.m_ptr, a1(), b1());
#endif #endif
@ -1434,7 +1434,7 @@ void mpz_manager<SYNCH>::bitwise_xor(mpz const & a, mpz const & b, mpz & c) {
} }
del(a1); del(b1); del(a2); del(b2); del(m); del(tmp); del(a1); del(b1); del(a2); del(b2); del(m); del(tmp);
#else #else
ensure_mpz a1(a), b1(b); ensure_mpz_t a1(a), b1(b);
mk_big(c); mk_big(c);
mpz_xor(*c.m_ptr, a1(), b1()); mpz_xor(*c.m_ptr, a1(), b1());
#endif #endif
@ -1542,7 +1542,7 @@ int mpz_manager<SYNCH>::big_compare(mpz const & a, mpz const & b) {
} }
#else #else
// GMP version // GMP version
ensure_mpz a1(a), b1(b); ensure_mpz_t a1(a), b1(b);
return mpz_cmp(a1(), b1()); return mpz_cmp(a1(), b1());
#endif #endif
} }
@ -1978,7 +1978,7 @@ void mpz_manager<SYNCH>::machine_div2k(mpz & a, unsigned k) {
c->m_size = new_sz; c->m_size = new_sz;
normalize(a); normalize(a);
#else #else
ensure_mpz a1(a); ensure_mpz_t a1(a);
MPZ_BEGIN_CRITICAL(); MPZ_BEGIN_CRITICAL();
mpz_tdiv_q_2exp(m_tmp, a1(), k); mpz_tdiv_q_2exp(m_tmp, a1(), k);
mk_big(a); mk_big(a);
@ -2043,7 +2043,7 @@ void mpz_manager<SYNCH>::mul2k(mpz & a, unsigned k) {
normalize(a); normalize(a);
TRACE("mpz_mul2k", tout << "mul2k result:\n" << to_string(a) << "\n";); TRACE("mpz_mul2k", tout << "mul2k result:\n" << to_string(a) << "\n";);
#else #else
ensure_mpz a1(a); ensure_mpz_t a1(a);
mk_big(a); mk_big(a);
mpz_mul_2exp(*a.m_ptr, a1(), k); mpz_mul_2exp(*a.m_ptr, a1(), k);
#endif #endif

16
src/util/mpz.h
View file

@ -135,11 +135,11 @@ inline void swap(mpz & m1, mpz & m2) { m1.swap(m2); }
template<bool SYNCH = true> template<bool SYNCH = true>
class mpz_manager { class mpz_manager {
small_object_allocator m_allocator; mutable small_object_allocator m_allocator;
omp_nest_lock_t m_lock; mutable 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; mutable mpn_manager m_mpn_manager;
#ifndef _MP_GMP #ifndef _MP_GMP
unsigned m_init_cell_capacity; unsigned m_init_cell_capacity;
@ -192,12 +192,12 @@ class mpz_manager {
#else #else
// GMP code // GMP code
mpz_t m_tmp, m_tmp2; mutable mpz_t m_tmp, m_tmp2;
mpz_t m_two32; mutable mpz_t m_two32;
mpz_t * m_arg[2]; mpz_t * m_arg[2];
mpz_t m_uint64_max; mutable mpz_t m_uint64_max;
mpz_t m_int64_max; mutable mpz_t m_int64_max;
mpz_t m_int64_min; mutable mpz_t m_int64_min;
mpz_t * allocate() { mpz_t * allocate() {
MPZ_BEGIN_CRITICAL(); MPZ_BEGIN_CRITICAL();