mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
numeral helper functions
This commit is contained in:
parent
e31926d132
commit
6eae27ffad
|
@ -88,6 +88,8 @@ public:
|
||||||
|
|
||||||
void neg(mpf & o);
|
void neg(mpf & o);
|
||||||
void neg(mpf const & x, mpf & o);
|
void neg(mpf const & x, mpf & o);
|
||||||
|
|
||||||
|
void swap(mpf& a, mpf& b) { a.swap(b); }
|
||||||
|
|
||||||
bool is_zero(mpf const & x);
|
bool is_zero(mpf const & x);
|
||||||
bool is_neg(mpf const & x);
|
bool is_neg(mpf const & x);
|
||||||
|
|
|
@ -76,6 +76,13 @@ static uint64_t _trailing_zeros64(uint64_t x) {
|
||||||
}
|
}
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
|
unsigned trailing_zeros(uint32_t x) {
|
||||||
|
return static_cast<unsigned>(_trailing_zeros32(x));
|
||||||
|
}
|
||||||
|
|
||||||
|
unsigned trailing_zeros(uint64_t x) {
|
||||||
|
return static_cast<unsigned>(_trailing_zeros64(x));
|
||||||
|
}
|
||||||
|
|
||||||
#define _bit_min(x, y) (y + ((x - y) & ((int)(x - y) >> 31)))
|
#define _bit_min(x, y) (y + ((x - y) & ((int)(x - y) >> 31)))
|
||||||
#define _bit_max(x, y) (x - ((x - y) & ((int)(x - y) >> 31)))
|
#define _bit_max(x, y) (x - ((x - y) & ((int)(x - y) >> 31)))
|
||||||
|
|
|
@ -29,6 +29,9 @@ Revision History:
|
||||||
|
|
||||||
unsigned u_gcd(unsigned u, unsigned v);
|
unsigned u_gcd(unsigned u, unsigned v);
|
||||||
uint64_t u64_gcd(uint64_t u, uint64_t v);
|
uint64_t u64_gcd(uint64_t u, uint64_t v);
|
||||||
|
unsigned trailing_zeros(uint64_t);
|
||||||
|
unsigned trailing_zeros(uint32_t);
|
||||||
|
|
||||||
|
|
||||||
#ifdef _MP_GMP
|
#ifdef _MP_GMP
|
||||||
typedef unsigned digit_t;
|
typedef unsigned digit_t;
|
||||||
|
|
|
@ -130,7 +130,7 @@ bool rational::limit_denominator(rational &num, rational const& limit) {
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
|
||||||
bool rational::mult_inverse(unsigned num_bits, rational & result) {
|
bool rational::mult_inverse(unsigned num_bits, rational & result) const {
|
||||||
rational const& n = *this;
|
rational const& n = *this;
|
||||||
if (n.is_one()) {
|
if (n.is_one()) {
|
||||||
result = n;
|
result = n;
|
||||||
|
|
|
@ -157,6 +157,12 @@ public:
|
||||||
friend inline rational numerator(rational const & r) { rational result; m().get_numerator(r.m_val, result.m_val); return result; }
|
friend inline rational numerator(rational const & r) { rational result; m().get_numerator(r.m_val, result.m_val); return result; }
|
||||||
|
|
||||||
friend inline rational denominator(rational const & r) { rational result; m().get_denominator(r.m_val, result.m_val); return result; }
|
friend inline rational denominator(rational const & r) { rational result; m().get_denominator(r.m_val, result.m_val); return result; }
|
||||||
|
|
||||||
|
friend inline rational inv(rational const & r) {
|
||||||
|
rational result;
|
||||||
|
m().inv(r.m_val, result.m_val);
|
||||||
|
return result;
|
||||||
|
}
|
||||||
|
|
||||||
rational & operator+=(rational const & r) {
|
rational & operator+=(rational const & r) {
|
||||||
m().add(m_val, r.m_val, m_val);
|
m().add(m_val, r.m_val, m_val);
|
||||||
|
@ -346,8 +352,13 @@ public:
|
||||||
bool is_power_of_two(unsigned & shift) const {
|
bool is_power_of_two(unsigned & shift) const {
|
||||||
return m().is_power_of_two(m_val, shift);
|
return m().is_power_of_two(m_val, shift);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
bool is_power_of_two() const {
|
||||||
|
unsigned shift = 0;
|
||||||
|
return m().is_power_of_two(m_val, shift);
|
||||||
|
}
|
||||||
|
|
||||||
bool mult_inverse(unsigned num_bits, rational & result);
|
bool mult_inverse(unsigned num_bits, rational & result) const;
|
||||||
|
|
||||||
static rational const & zero() {
|
static rational const & zero() {
|
||||||
return m_zero;
|
return m_zero;
|
||||||
|
|
|
@ -61,11 +61,11 @@ public:
|
||||||
}
|
}
|
||||||
|
|
||||||
void swap(_scoped_numeral & n) {
|
void swap(_scoped_numeral & n) {
|
||||||
m_num.swap(n.m_num);
|
m().swap(m_num, n.m_num);
|
||||||
}
|
}
|
||||||
|
|
||||||
void swap(numeral & n) {
|
void swap(numeral & n) {
|
||||||
m_num.swap(n);
|
m().swap(m_num, n);
|
||||||
}
|
}
|
||||||
|
|
||||||
_scoped_numeral & operator+=(numeral const & a) {
|
_scoped_numeral & operator+=(numeral const & a) {
|
||||||
|
|
Loading…
Reference in a new issue