mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix referencen to vvr()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-04-20 13:41:54 -07:00
parent 49c2d991ca
commit c97a6dd7cb
3 changed files with 12 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/util/lp/nla_basics_lemmas.cpp
View file

@ -76,7 +76,7 @@ bool basics::try_get_non_strict_sign_from_bounds(lpvar j, int& sign) const {
}
void basics::get_non_strict_sign(lpvar j, int& sign) const {
const rational & v = vvr(j);
const rational v = vvr(j);
if (v.is_zero()) {
try_get_non_strict_sign_from_bounds(j, sign);
} else {
@ -323,8 +323,8 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const smon&
lpvar mon_var = c().m_emons[rm.var()].var();
TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout); tout << "\nmon_var = " << mon_var << "\n";);
const auto & mv = vvr(mon_var);
const auto abs_mv = abs(mv);
const auto mv = vvr(mon_var);
const auto abs_mv = abs(mv);
if (abs_mv == rational::zero()) {
return false;
@ -570,8 +570,8 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const
TRACE("nla_solver_bl", c().print_monomial(m, tout););
lpvar mon_var = m.var();
const auto & mv = vvr(mon_var);
const auto abs_mv = abs(mv);
const auto mv = vvr(mon_var);
const auto abs_mv = abs(mv);
if (abs_mv == rational::zero()) {
return false;
}
@ -670,8 +670,8 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const sm
lpvar mon_var = c().m_emons[rm.var()].var();
TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout); tout << "\nmon_var = " << mon_var << "\n";);
const auto & mv = vvr(mon_var);
const auto abs_mv = abs(mv);
const auto mv = vvr(mon_var);
const auto abs_mv = abs(mv);
if (abs_mv == rational::zero()) {
return false;

4
src/util/lp/nla_order_lemmas.cpp
View file

@ -54,7 +54,7 @@ void order::order_lemma_on_rmonomial(const smon& rm) {
void order::order_lemma_on_binomial(const monomial& ac) {
TRACE("nla_solver", tout << pp_mon(c(), ac););
SASSERT(!check_monomial(ac) && ac.size() == 2);
const rational & mult_val = vvr(ac[0]) * vvr(ac[1]);
const rational mult_val = vvr(ac[0]) * vvr(ac[1]);
const rational acv = vvr(ac);
bool gt = acv > mult_val;
for (unsigned k = 0; k < 2; k++) {
@ -182,7 +182,7 @@ void order::order_lemma_on_factorization(const smon& rm, const factorization& ab
rational sign = _().m_emons.orig_sign(rm);
for (factor f: ab)
sign *= _().canonize_sign(f);
const rational & fv = vvr(ab[0]) * vvr(ab[1]);
const rational fv = vvr(ab[0]) * vvr(ab[1]);
const rational mv = sign * vvr(m);
TRACE("nla_solver",
tout << "ab.size()=" << ab.size() << "\n";

6
src/util/lp/nla_tangent_lemmas.cpp
View file

@ -40,7 +40,7 @@ void tangents::generate_simple_tangent_lemma(const smon* rm) {
m_core->add_empty_lemma();
const monomial & m = c().m_emons[rm->var()];
const rational v = c().product_value(m);
const rational& mv = vvr(m);
const rational mv = vvr(m);
SASSERT(mv != v);
SASSERT(!mv.is_zero() && !v.is_zero());
rational sign = rational(nla::rat_sign(mv));
@ -51,7 +51,7 @@ void tangents::generate_simple_tangent_lemma(const smon* rm) {
bool gt = abs(mv) > abs(v);
if (gt) {
for (lpvar j : m) {
const rational & jv = vvr(j);
const rational jv = vvr(j);
rational js = rational(nla::rat_sign(jv));
c().mk_ineq(js, j, llc::LT);
c().mk_ineq(js, j, llc::GT, jv);
@ -59,7 +59,7 @@ void tangents::generate_simple_tangent_lemma(const smon* rm) {
c().mk_ineq(sign, rm->var(), llc::LE, std::max(v, rational(-1)));
} else {
for (lpvar j : m) {
const rational & jv = vvr(j);
const rational jv = vvr(j);
rational js = rational(nla::rat_sign(jv));
c().mk_ineq(js, j, llc::LT, std::max(jv, rational(0)));
}