mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
Merge branch 'master' of https://github.com/z3prover/z3
This commit is contained in:
commit
5b71f7cf9e
|
@ -506,8 +506,7 @@ namespace realclosure {
|
|||
m_bqim(lim, m_bqm),
|
||||
m_plus_inf_approx(m_bqm),
|
||||
m_minus_inf_approx(m_bqm) {
|
||||
mpq one(1);
|
||||
m_one = mk_rational(one);
|
||||
m_one = mk_rational(mpq(1));
|
||||
inc_ref(m_one);
|
||||
m_pi = nullptr;
|
||||
m_e = nullptr;
|
||||
|
@ -2557,13 +2556,10 @@ namespace realclosure {
|
|||
return new (allocator()) rational_value();
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Make a rational and swap its value with v
|
||||
*/
|
||||
rational_value * mk_rational_and_swap(mpq & v) {
|
||||
rational_value * mk_rational(mpq && v) {
|
||||
SASSERT(!qm().is_zero(v));
|
||||
rational_value * r = mk_rational();
|
||||
::swap(r->m_value, v);
|
||||
r->m_value = std::move(v);
|
||||
return r;
|
||||
}
|
||||
|
||||
|
@ -2585,7 +2581,7 @@ namespace realclosure {
|
|||
SASSERT(!bqm().is_zero(v));
|
||||
scoped_mpq v_q(qm()); // v as a rational
|
||||
::to_mpq(qm(), v, v_q);
|
||||
return mk_rational(v_q);
|
||||
return mk_rational(std::move(v_q));
|
||||
}
|
||||
|
||||
void reset_interval(value * a) {
|
||||
|
@ -3270,7 +3266,7 @@ namespace realclosure {
|
|||
scoped_mpq num_z(qm());
|
||||
qm().div(lcm_z, to_mpq(dens[i]), num_z);
|
||||
SASSERT(qm().is_int(num_z));
|
||||
m = mk_rational_and_swap(num_z);
|
||||
m = mk_rational(std::move(num_z));
|
||||
is_z = true;
|
||||
}
|
||||
bool found_lt_eq = false;
|
||||
|
@ -3432,7 +3428,7 @@ namespace realclosure {
|
|||
scoped_mpq r(qm());
|
||||
SASSERT(qm().is_int(to_mpq(a)));
|
||||
qm().div(to_mpq(a), b, r);
|
||||
a = mk_rational_and_swap(r);
|
||||
a = mk_rational(std::move(r));
|
||||
}
|
||||
else {
|
||||
rational_function_value * rf = to_rational_function(a);
|
||||
|
@ -3592,9 +3588,8 @@ namespace realclosure {
|
|||
r.reset();
|
||||
if (sz > 1) {
|
||||
for (unsigned i = 1; i < sz; i++) {
|
||||
mpq i_mpq(i);
|
||||
value_ref a_i(*this);
|
||||
a_i = mk_rational_and_swap(i_mpq);
|
||||
a_i = mk_rational(mpq(i));
|
||||
mul(a_i, p[i], a_i);
|
||||
r.push_back(a_i);
|
||||
}
|
||||
|
@ -3821,7 +3816,7 @@ namespace realclosure {
|
|||
scoped_mpz mpz_twok(qm());
|
||||
qm().mul2k(mpz(1), b.k(), mpz_twok);
|
||||
value_ref twok(*this), twok_i(*this);
|
||||
twok = mk_rational(mpz_twok);
|
||||
twok = mk_rational(std::move(mpz_twok));
|
||||
twok_i = twok;
|
||||
value_ref c(*this);
|
||||
c = mk_rational(b.numerator());
|
||||
|
@ -5061,7 +5056,7 @@ namespace realclosure {
|
|||
if (qm().is_zero(v))
|
||||
r = nullptr;
|
||||
else
|
||||
r = mk_rational_and_swap(v);
|
||||
r = mk_rational(std::move(v));
|
||||
}
|
||||
else {
|
||||
INC_DEPTH();
|
||||
|
@ -5090,7 +5085,7 @@ namespace realclosure {
|
|||
if (qm().is_zero(v))
|
||||
r = nullptr;
|
||||
else
|
||||
r = mk_rational_and_swap(v);
|
||||
r = mk_rational(std::move(v));
|
||||
}
|
||||
else {
|
||||
value_ref neg_b(*this);
|
||||
|
@ -5124,7 +5119,7 @@ namespace realclosure {
|
|||
scoped_mpq v(qm());
|
||||
qm().set(v, to_mpq(a));
|
||||
qm().neg(v);
|
||||
r = mk_rational_and_swap(v);
|
||||
r = mk_rational(std::move(v));
|
||||
}
|
||||
else {
|
||||
neg_rf(to_rational_function(a), r);
|
||||
|
@ -5269,7 +5264,7 @@ namespace realclosure {
|
|||
else if (is_nz_rational(a) && is_nz_rational(b)) {
|
||||
scoped_mpq v(qm());
|
||||
qm().mul(to_mpq(a), to_mpq(b), v);
|
||||
r = mk_rational_and_swap(v);
|
||||
r = mk_rational(std::move(v));
|
||||
}
|
||||
else {
|
||||
INC_DEPTH();
|
||||
|
@ -5304,7 +5299,7 @@ namespace realclosure {
|
|||
else if (is_nz_rational(a) && is_nz_rational(b)) {
|
||||
scoped_mpq v(qm());
|
||||
qm().div(to_mpq(a), to_mpq(b), v);
|
||||
r = mk_rational_and_swap(v);
|
||||
r = mk_rational(std::move(v));
|
||||
}
|
||||
else {
|
||||
value_ref inv_b(*this);
|
||||
|
@ -5557,7 +5552,7 @@ namespace realclosure {
|
|||
if (is_nz_rational(a)) {
|
||||
scoped_mpq v(qm());
|
||||
qm().inv(to_mpq(a), v);
|
||||
r = mk_rational_and_swap(v);
|
||||
r = mk_rational(std::move(v));
|
||||
}
|
||||
else {
|
||||
inv_rf(to_rational_function(a), r);
|
||||
|
|
|
@ -32,13 +32,10 @@ public:
|
|||
mpq(mpq &&) noexcept = default;
|
||||
mpq & operator=(mpq&&) = default;
|
||||
mpq & operator=(mpq const&) = delete;
|
||||
void swap(mpq & other) { m_num.swap(other.m_num); m_den.swap(other.m_den); }
|
||||
mpz const & numerator() const { return m_num; }
|
||||
mpz const & denominator() const { return m_den; }
|
||||
};
|
||||
|
||||
inline void swap(mpq & m1, mpq & m2) { m1.swap(m2); }
|
||||
|
||||
template<bool SYNCH = true>
|
||||
class mpq_manager : public mpz_manager<SYNCH> {
|
||||
mpz m_tmp1;
|
||||
|
|
Loading…
Reference in a new issue