mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-30 21:19:29 +00:00
Code Activity

remove shortcut as it breaks current contract

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-14 04:49:27 -07:00
parent 573c2cb8f7
commit 8158a500d4
1 changed files with 6 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/util/mpz.cpp
View file

@ -2320,10 +2320,13 @@ bool mpz_manager<SYNCH>::is_perfect_square(mpz const & a, mpz & root) {
set(root, 1); set(root, 1);
return true; return true;
} }
#if 0
// current contract is that root is set to an approximation within +1/-1 of actional root.
// x^2 mod 16 in { 9, 1, 4, 0 } // x^2 mod 16 in { 9, 1, 4, 0 }
auto mod16 = get_least_significant(a) & 0xF; auto mod16 = get_least_significant(a) & 0xF;
if (mod16 != 0 && mod16 != 1 && mod16 != 4 && mod16 != 9) if (mod16 != 0 && mod16 != 1 && mod16 != 4 && mod16 != 9)
return false; return false;
#endif
mpz lo, hi, mid, sq_lo, sq_mid; mpz lo, hi, mid, sq_lo, sq_mid;
set(lo, 1); set(lo, 1);
@ -2484,6 +2487,7 @@ bool mpz_manager<SYNCH>::root(mpz & a, unsigned n) {
template<bool SYNCH> template<bool SYNCH>
digit_t mpz_manager<SYNCH>::get_least_significant(mpz const& a) { digit_t mpz_manager<SYNCH>::get_least_significant(mpz const& a) {
SASSERT(!is_neg(a));
if (is_small(a)) if (is_small(a))
return std::abs(a.m_val); return std::abs(a.m_val);
#ifndef _MP_GMP #ifndef _MP_GMP
@ -2493,16 +2497,7 @@ digit_t mpz_manager<SYNCH>::get_least_significant(mpz const& a) {
return 0; return 0;
return cell_a->m_digits[0]; return cell_a->m_digits[0];
#else #else
digit_t result = 0; return mpz_get_ui(*a.m_ptr);
MPZ_BEGIN_CRITICAL();
mpz_set(m_tmp, *a.m_ptr);
mpz_abs(m_tmp, m_tmp);
if (mpz_sgn(m_tmp) != 0) {
mpz_tdiv_r_2exp(m_tmp2, m_tmp, 32);
result = mpz_get_ui(m_tmp2);
}
MPZ_END_CRITICAL();
return result;
#endif #endif
} }