From 4d7062d2a12e47b3506fc105e791a67867d70f1f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 8 Dec 2020 15:40:51 -0800 Subject: [PATCH] fix in nla_ordered_lemma Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.cpp | 2 +- src/math/lp/nla_order_lemmas.cpp | 15 ++++++++------- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 5a94b45d21e..ca491a169a6 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -783,7 +783,7 @@ namespace lp { update_x_and_inf_costs_for_columns_with_changed_bounds(); m_mpq_lar_core_solver.solve(); set_status(m_mpq_lar_core_solver.m_r_solver.get_status()); - lp_assert((((lp_settings::ddd++) % 100) != 0) || m_status != lp_status::OPTIMAL || all_constraints_hold()); + lp_assert(((m_settings.stats().m_make_feasible% 100) != 0) || m_status != lp_status::OPTIMAL || all_constraints_hold()); } diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index 800bc8bf137..8862891d415 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -199,20 +199,21 @@ bool order::order_lemma_on_ac_and_bc(const monic& rm_ac, } -// Here ab is a binary factorization of m. +// Here m = ab, that is ab is binary factorization of m. // We try to find a monic n = cd, such that |b| = |d| -// and get a lemma m R n & |b| = |d| => ab/|b| R cd /|d|, where R is a relation +// and get lemma m R n & |b| = |d| => ab/|b| R cd /|d|, where R is a relation void order::order_lemma_on_factorization(const monic& m, const factorization& ab) { - bool sign = m.rsign(); - for (factor f: ab) - sign ^= _().canonize_sign(f); + bool sign = false; + for (factor f: ab) + sign ^= f.sign(); const rational rsign = sign_to_rat(sign); const rational fv = val(var(ab[0])) * val(var(ab[1])); const rational mv = rsign * var_val(m); TRACE("nla_solver", tout << "ab.size()=" << ab.size() << "\n"; - tout << "we should have sign*var_val(m):" << mv << "=(" << rsign << ")*(" << var_val(m) <<") to be equal to " << " val(var(ab[0]))*val(var(ab[1])):" << fv << "\n";); - TRACE("nla_solver", tout << "m="; _().print_monic_with_vars(m, tout); tout << "\nfactorization="; _().print_factorization(ab, tout);); + tout << "we should have mv =" << mv << " = " << fv << " = fv\n"; + tout << "m = "; _().print_monic_with_vars(m, tout); tout << "\nab ="; _().print_factorization(ab, tout);); + if (mv != fv && !c().has_real(m)) { bool gt = mv > fv; for (unsigned j = 0, k = 1; j < 2; j++, k--) {