mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-24 01:01:19 +00:00
Code Activity

optimize has_sign_bit and mod2k to not compute powers of two

Browse source 
this is very useful for bitvectors of large bitwidths
This commit is contained in:
Nuno Lopes 2026-01-31 10:36:43 +00:00 • committed by Nikolaj Bjorner
parent 9771839005
commit 6c3f9a3540
6 changed files with 97 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/util/rational.h
View file

@ -51,10 +51,10 @@ public:
explicit rational(unsigned n) { m().set(m_val, n); }
rational(int n, int d) { m().set(m_val, n, d); }
rational(mpq const & q) { m().set(m_val, q); }
rational(mpq && q) noexcept : m_val(std::move(q)) {}
rational(mpz const & z) { m().set(m_val, z); }
rational(mpz && z) noexcept : m_val(std::move(z)) {}
explicit rational(double z) { UNREACHABLE(); }
@ -274,8 +274,8 @@ public:
}
friend inline rational mod2k(rational const & a, unsigned k) {
if (a.is_nonneg() && a.is_int() && a.bitsize() <= k)
return a;
if (a.is_int())
return rational::m().mod2k(a.m_val.numerator(), k);
return mod(a, power_of_two(k));
}