From 687c4877461f14cbe0f828b1e761bd9492a54886 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sun, 15 Mar 2020 19:47:31 -0700 Subject: [PATCH] accept terms indices in core::explain_coeff_upper_bound() Signed-off-by: Lev Nachmanson --- src/math/lp/nla_core.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 41d8d1dba..2212d042f 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -342,21 +342,22 @@ bool core:: explain_coeff_lower_bound(const lp::lar_term::ival& p, rational& bou bool core:: explain_coeff_upper_bound(const lp::lar_term::ival& p, rational& bound, lp::explanation& e) const { const rational& a = p.coeff(); + lpvar j = lp::is_term(p.var())? m_lar_solver.map_term_index_to_column_index(p.var()) : p.var(); SASSERT(!a.is_zero()); unsigned c; // the index for the lower or the upper bound if (a.is_neg()) { - unsigned c = m_lar_solver.get_column_lower_bound_witness(p.var()); + unsigned c = m_lar_solver.get_column_lower_bound_witness(j); if (c + 1 == 0) return false; - bound = a * m_lar_solver.get_lower_bound(p.var()).x; + bound = a * m_lar_solver.get_lower_bound(j).x; e.add(c); return true; } // a.is_pos() - c = m_lar_solver.get_column_upper_bound_witness(p.var()); + c = m_lar_solver.get_column_upper_bound_witness(j); if (c + 1 == 0) return false; - bound = a * m_lar_solver.get_upper_bound(p.var()).x; + bound = a * m_lar_solver.get_upper_bound(j).x; e.add(c); return true; }