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

put mpz_cell under ifdef _NO_GMP

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-03 06:54:50 -07:00
parent 6981918c33
commit 810d63c246
2 changed files with 17 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/util/mpz.cpp
View file

@ -196,6 +196,7 @@ mpz_manager<SYNCH>::~mpz_manager() {
omp_destroy_nest_lock(&m_lock); omp_destroy_nest_lock(&m_lock);
} }
#ifndef _MP_GMP
template<bool SYNCH> template<bool SYNCH>
mpz_cell * mpz_manager<SYNCH>::allocate(unsigned capacity) { mpz_cell * mpz_manager<SYNCH>::allocate(unsigned capacity) {
SASSERT(capacity >= m_init_cell_capacity); SASSERT(capacity >= m_init_cell_capacity);
@ -215,6 +216,15 @@ void mpz_manager<SYNCH>::deallocate(bool is_heap, mpz_cell * ptr) {
} }
} }
template<bool SYNCH>
mpz_manager<SYNCH>::sign_cell::sign_cell(mpz_manager& m, mpz const& a):
m_local(reinterpret_cast<mpz_cell*>(m_bytes)), m_a(a) {
m_local.m_ptr->m_capacity = capacity;
m.get_sign_cell(a, m_sign, m_cell, m_local.m_ptr);
}
#endif
template<bool SYNCH> template<bool SYNCH>
@ -1119,12 +1129,6 @@ unsigned mpz_manager<SYNCH>::size_info(mpz const & a) {
#endif #endif
} }
template<bool SYNCH>
mpz_manager<SYNCH>::sign_cell::sign_cell(mpz_manager& m, mpz const& a):
m_local(reinterpret_cast<mpz_cell*>(m_bytes)), m_a(a) {
m_local.m_ptr->m_capacity = capacity;
m.get_sign_cell(a, m_sign, m_cell, m_local.m_ptr);
}
template<bool SYNCH> template<bool SYNCH>

12
src/util/mpz.h
View file

@ -183,6 +183,13 @@ class mpz_manager {
void clear(mpz& n) { } void clear(mpz& n) { }
/**
\brief Set \c a with the value stored at src, and the given sign.
\c sz is an overapproximation of the size of the number stored at \c src.
*/
void set(mpz_cell& src, mpz & a, int sign, unsigned sz);
#else #else
// GMP code // GMP code
mpz_t m_tmp, m_tmp2; mpz_t m_tmp, m_tmp2;
@ -215,11 +222,6 @@ class mpz_manager {
mpz m_two64; mpz m_two64;
/**
\brief Set \c a with the value stored at src, and the given sign.
\c sz is an overapproximation of the size of the number stored at \c src.
*/
void set(mpz_cell& src, mpz & a, int sign, unsigned sz);
static int64_t i64(mpz const & a) { return static_cast<int64_t>(a.m_val); } static int64_t i64(mpz const & a) { return static_cast<int64_t>(a.m_val); }