From 46b9273a79b8a3e2ea34d4139d5b539a9aa794b0 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 10 Jun 2019 15:10:54 -0700 Subject: [PATCH] fixes in interval explanations Signed-off-by: Lev Nachmanson --- src/math/lp/bound_analyzer_on_row.h | 1 + src/math/lp/lp_bound_propagator.cpp | 2 ++ src/math/lp/nla_intervals.cpp | 12 ++++++------ 3 files changed, 9 insertions(+), 6 deletions(-) diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h index 528980f74..73fcd1212 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -56,6 +56,7 @@ public : {} void analyze() { + TRACE("lp_bound_prop", print_linear_combination_of_column_indices_only(m_row, tout); tout << " = " << m_rs << "\n";); for (const auto & c : m_row) { if ((m_column_of_l == -2) && (m_column_of_u == -2)) break; diff --git a/src/math/lp/lp_bound_propagator.cpp b/src/math/lp/lp_bound_propagator.cpp index bf7171cd8..729d060e1 100644 --- a/src/math/lp/lp_bound_propagator.cpp +++ b/src/math/lp/lp_bound_propagator.cpp @@ -42,6 +42,7 @@ bool lp_bound_propagator::lower_bound_is_available_for_column(unsigned j) const return false; } } + bool lp_bound_propagator::upper_bound_is_available(unsigned j) const { if (upper_bound_is_available_for_column(j)) return true; @@ -123,6 +124,7 @@ bool lp_bound_propagator::nl_monomial_upper_bound_should_be_taken(unsigned j) co } bool lp_bound_propagator::nl_monomial_lower_bound_should_be_taken(unsigned j) const { + lp_assert(lower_bound_is_available(j)); return (!lower_bound_is_available_for_column(j)) || (nl_monomial_lower_bound_is_available(j) && m_nla_solver->get_lower_bound(j) > m_lar_solver.m_mpq_lar_core_solver.m_r_lower_bounds()[j]); } diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 6f1ae1b41..f9b55be27 100755 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -23,12 +23,12 @@ intervals::interval intervals::mul_signs_with_deps(const svector& vars) c m_imanager.set(a, mpq(1)); for (lpvar v : vars) { set_var_interval_signs_with_deps(v, b); - if (m_imanager.is_zero(b)) - return b; interval_deps deps; m_imanager.mul(a, b, c, deps); m_imanager.set(a, c); m_config.add_deps(a, b, deps, a); + if (m_imanager.is_zero(a)) + return a; } return a; @@ -174,7 +174,7 @@ lp::impq intervals::get_upper_bound_of_monomial(lpvar j) const { auto r = lp::impq(a.m_upper); if (a.m_upper_open) r.y = -1; - TRACE("nla_intervals", m_core->print_monomial_with_vars(m, tout) << "upper = " << r << "\n";); + TRACE("nla_intervals_detail", m_core->print_monomial_with_vars(m, tout) << "upper = " << r << "\n";); return r; } lp::impq intervals::get_lower_bound_of_monomial(lpvar j) const { @@ -184,7 +184,7 @@ lp::impq intervals::get_lower_bound_of_monomial(lpvar j) const { auto r = lp::impq(a.m_lower); if (a.m_lower_open) r.y = 1; - TRACE("nla_intervals", m_core->print_monomial_with_vars(m, tout) << "lower = " << r << "\n";); + TRACE("nla_intervals_detail", m_core->print_monomial_with_vars(m, tout) << "lower = " << r << "\n";); return r; } @@ -240,9 +240,9 @@ lp::lar_solver& intervals::ls() { return m_core->m_lar_solver; } const lp::lar_solver& intervals::ls() const { return m_core->m_lar_solver; } std::ostream& intervals::print_explanations(const svector &expl , std::ostream& out) const { - out << "interv expl: "; + out << "interv expl:\n "; for (auto ci : expl) - m_core->m_lar_solver.print_constraint(ci, out) << "\n"; + m_core->m_lar_solver.print_constraint_indices_only(ci, out); return out; }