mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

use std::move

Browse source
This commit is contained in:
Nuno Lopes 2022-10-02 21:34:17 +01:00
parent cffe5fe1a5
commit 1eed058b98
1 changed files with 14 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/math/realclosure/realclosure.cpp
View file

@ -506,8 +506,7 @@ namespace realclosure {
m_bqim(lim, m_bqm), m_bqim(lim, m_bqm),
m_plus_inf_approx(m_bqm), m_plus_inf_approx(m_bqm),
m_minus_inf_approx(m_bqm) { m_minus_inf_approx(m_bqm) {
mpq one(1); m_one = mk_rational(mpq(1));
m_one = mk_rational(one);
inc_ref(m_one); inc_ref(m_one);
m_pi = nullptr; m_pi = nullptr;
m_e = nullptr; m_e = nullptr;
@ -2557,13 +2556,10 @@ namespace realclosure {
return new (allocator()) rational_value(); return new (allocator()) rational_value();
} }
/** rational_value * mk_rational(mpq && v) {
\brief Make a rational and swap its value with v
*/
rational_value * mk_rational_and_swap(mpq & v) {
SASSERT(!qm().is_zero(v)); SASSERT(!qm().is_zero(v));
rational_value * r = mk_rational(); rational_value * r = mk_rational();
::swap(r->m_value, v); r->m_value = std::move(v);
return r; return r;
} }
@ -2585,7 +2581,7 @@ namespace realclosure {
SASSERT(!bqm().is_zero(v)); SASSERT(!bqm().is_zero(v));
scoped_mpq v_q(qm()); // v as a rational scoped_mpq v_q(qm()); // v as a rational
::to_mpq(qm(), v, v_q); ::to_mpq(qm(), v, v_q);
return mk_rational(v_q); return mk_rational(std::move(v_q));
} }
void reset_interval(value * a) { void reset_interval(value * a) {
@ -3270,7 +3266,7 @@ namespace realclosure {
scoped_mpq num_z(qm()); scoped_mpq num_z(qm());
qm().div(lcm_z, to_mpq(dens[i]), num_z); qm().div(lcm_z, to_mpq(dens[i]), num_z);
SASSERT(qm().is_int(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; is_z = true;
} }
bool found_lt_eq = false; bool found_lt_eq = false;
@ -3432,7 +3428,7 @@ namespace realclosure {
scoped_mpq r(qm()); scoped_mpq r(qm());
SASSERT(qm().is_int(to_mpq(a))); SASSERT(qm().is_int(to_mpq(a)));
qm().div(to_mpq(a), b, r); qm().div(to_mpq(a), b, r);
a = mk_rational_and_swap(r); a = mk_rational(std::move(r));
} }
else { else {
rational_function_value * rf = to_rational_function(a); rational_function_value * rf = to_rational_function(a);
@ -3592,9 +3588,8 @@ namespace realclosure {
r.reset(); r.reset();
if (sz > 1) { if (sz > 1) {
for (unsigned i = 1; i < sz; i++) { for (unsigned i = 1; i < sz; i++) {
mpq i_mpq(i);
value_ref a_i(*this); 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); mul(a_i, p[i], a_i);
r.push_back(a_i); r.push_back(a_i);
} }
@ -3821,7 +3816,7 @@ namespace realclosure {
scoped_mpz mpz_twok(qm()); scoped_mpz mpz_twok(qm());
qm().mul2k(mpz(1), b.k(), mpz_twok); qm().mul2k(mpz(1), b.k(), mpz_twok);
value_ref twok(*this), twok_i(*this); value_ref twok(*this), twok_i(*this);
twok = mk_rational(mpz_twok); twok = mk_rational(std::move(mpz_twok));
twok_i = twok; twok_i = twok;
value_ref c(*this); value_ref c(*this);
c = mk_rational(b.numerator()); c = mk_rational(b.numerator());
@ -5061,7 +5056,7 @@ namespace realclosure {
if (qm().is_zero(v)) if (qm().is_zero(v))
r = nullptr; r = nullptr;
else else
r = mk_rational_and_swap(v); r = mk_rational(std::move(v));
} }
else { else {
INC_DEPTH(); INC_DEPTH();
@ -5090,7 +5085,7 @@ namespace realclosure {
if (qm().is_zero(v)) if (qm().is_zero(v))
r = nullptr; r = nullptr;
else else
r = mk_rational_and_swap(v); r = mk_rational(std::move(v));
} }
else { else {
value_ref neg_b(*this); value_ref neg_b(*this);
@ -5124,7 +5119,7 @@ namespace realclosure {
scoped_mpq v(qm()); scoped_mpq v(qm());
qm().set(v, to_mpq(a)); qm().set(v, to_mpq(a));
qm().neg(v); qm().neg(v);
r = mk_rational_and_swap(v); r = mk_rational(std::move(v));
} }
else { else {
neg_rf(to_rational_function(a), r); neg_rf(to_rational_function(a), r);
@ -5269,7 +5264,7 @@ namespace realclosure {
else if (is_nz_rational(a) && is_nz_rational(b)) { else if (is_nz_rational(a) && is_nz_rational(b)) {
scoped_mpq v(qm()); scoped_mpq v(qm());
qm().mul(to_mpq(a), to_mpq(b), v); qm().mul(to_mpq(a), to_mpq(b), v);
r = mk_rational_and_swap(v); r = mk_rational(std::move(v));
} }
else { else {
INC_DEPTH(); INC_DEPTH();
@ -5304,7 +5299,7 @@ namespace realclosure {
else if (is_nz_rational(a) && is_nz_rational(b)) { else if (is_nz_rational(a) && is_nz_rational(b)) {
scoped_mpq v(qm()); scoped_mpq v(qm());
qm().div(to_mpq(a), to_mpq(b), v); qm().div(to_mpq(a), to_mpq(b), v);
r = mk_rational_and_swap(v); r = mk_rational(std::move(v));
} }
else { else {
value_ref inv_b(*this); value_ref inv_b(*this);
@ -5557,7 +5552,7 @@ namespace realclosure {
if (is_nz_rational(a)) { if (is_nz_rational(a)) {
scoped_mpq v(qm()); scoped_mpq v(qm());
qm().inv(to_mpq(a), v); qm().inv(to_mpq(a), v);
r = mk_rational_and_swap(v); r = mk_rational(std::move(v));
} }
else { else {
inv_rf(to_rational_function(a), r); inv_rf(to_rational_function(a), r);