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

update mpz for NO_GMP

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-03 18:31:05 -07:00
parent b61fa40063
commit dfdf7a0e4a
2 changed files with 10 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

2
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::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);

19
src/util/mpz.h
View file

@ -150,14 +150,6 @@ class mpz_manager {
} }
mpz_cell * allocate(unsigned capacity); mpz_cell * allocate(unsigned capacity);
void deallocate(mpz& n) {
if (n.m_ptr) {
deallocate(n.m_owner == mpz_self, n.m_ptr);
n.m_ptr = nullptr;
n.m_kind = mpz_small;
}
}
// make sure that n is a big number and has capacity equal to at least c. // make sure that n is a big number and has capacity equal to at least c.
void allocate_if_needed(mpz & n, unsigned c) { void allocate_if_needed(mpz & n, unsigned c) {
@ -181,7 +173,7 @@ class mpz_manager {
void normalize(mpz & a); void normalize(mpz & a);
void clear(mpz& n) { } void clear(mpz& n) { reset(n); }
/** /**
\brief Set \c a with the value stored at src, and the given sign. \brief Set \c a with the value stored at src, and the given sign.
@ -216,9 +208,16 @@ class mpz_manager {
} }
} }
void clear(mpz& n) { if (n.m_ptr) mpz_clear(*n.m_ptr); } void clear(mpz& n) { if (n.m_ptr) { mpz_clear(*n.m_ptr); }}
#endif #endif
void deallocate(mpz& n) {
if (n.m_ptr) {
deallocate(n.m_owner == mpz_self, n.m_ptr);
n.m_ptr = nullptr;
n.m_kind = mpz_small;
}
}
mpz m_two64; mpz m_two64;