mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-23 03:27:52 +00:00
Code Activity

import updates to rational from polysat

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-09 12:46:06 -08:00
parent 575538d325
commit e580c384b8
5 changed files with 60 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

27
src/util/rational.h
View file

@ -55,7 +55,7 @@ public:
explicit rational(double z) { UNREACHABLE(); }
explicit rational(char const * v) { m().set(m_val, v); }
explicit rational(unsigned const * v, unsigned sz) { m().set(m_val, sz, v); }
struct i64 {};
@ -489,6 +489,18 @@ public:
return get_num_digits(rational(10));
}
/**
* \brief Return the biggest k s.t. 2^k <= a.
* \remark Return 0 if a is not positive.
*/
unsigned prev_power_of_two() const { return m().prev_power_of_two(m_val); }
/**
* \brief Return the smallest k s.t. a <= 2^k.
* \remark Return 0 if a is not positive.
*/
unsigned next_power_of_two() const { return m().next_power_of_two(m_val); }
bool get_bit(unsigned index) const {
return m().get_bit(m_val, index);
}
@ -501,6 +513,15 @@ public:
return k;
}
/** Number of trailing zeros in an N-bit representation */
unsigned parity(unsigned num_bits) const {
SASSERT(!is_neg());
SASSERT(*this < rational::power_of_two(num_bits));
if (is_zero())
return num_bits;
return trailing_zeros();
}
static bool limit_denominator(rational &num, rational const& limit);
};
@ -649,3 +670,7 @@ inline rational gcd(rational const & r1, rational const & r2, rational & a, rati
rational::m().gcd(r1.m_val, r2.m_val, a.m_val, b.m_val, result.m_val);
return result;
}
inline void swap(rational& r1, rational& r2) {
r1.swap(r2);
}