From c1ab7987f62f2ed969d8ba3a211690430988e5b7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 7 Jun 2021 11:41:35 -0700 Subject: [PATCH] #5324 --- src/math/simplex/model_based_opt.cpp | 35 +++++++++++++++------------- 1 file changed, 19 insertions(+), 16 deletions(-) diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp index e383a39fd..e785c33ed 100644 --- a/src/math/simplex/model_based_opt.cpp +++ b/src/math/simplex/model_based_opt.cpp @@ -378,7 +378,8 @@ namespace opt { } else if ((value == lub_val && r.m_type == opt::t_lt) || (is_pos && value < lub_val) || - (!is_pos && value > lub_val)) { + + (!is_pos && value > lub_val)) { m_above.push_back(bound_row_index); lub_val = value; bound_row_index = row_id; @@ -794,7 +795,7 @@ namespace opt { } std::ostream& model_based_opt::display(std::ostream& out, row const& r) { - out << (r.m_alive?"+":"-") << " "; + out << (r.m_alive?"a":"d") << " "; display(out, r.m_vars, r.m_coeff); if (r.m_type == opt::t_mod) { out << r.m_type << " " << r.m_mod << " = 0; value: " << r.m_value << "\n"; @@ -1192,7 +1193,9 @@ namespace opt { SASSERT(a.is_pos()); if (ty == t_lt) { SASSERT(compute_def); - m_rows[row_id1].m_coeff += a; + m_rows[row_id1].m_coeff += a; + m_rows[row_id1].m_type = t_le; + m_rows[row_id1].m_value += a; } if (m_var2is_int[x] && !a.is_one()) { row& r1 = m_rows[row_id1]; @@ -1208,19 +1211,19 @@ namespace opt { if (!visited.contains(row_id2)) { visited.insert(row_id2); b = get_coefficient(row_id2, x); - if (!b.is_zero()) { - row& dst = m_rows[row_id2]; - switch (dst.m_type) { - case t_eq: - case t_lt: - case t_le: - solve(row_id1, a, row_id2, x); - break; - case t_mod: - // mod reduction already done. - UNREACHABLE(); - break; - } + if (b.is_zero()) + continue; + row& dst = m_rows[row_id2]; + switch (dst.m_type) { + case t_eq: + case t_lt: + case t_le: + solve(row_id1, a, row_id2, x); + break; + case t_mod: + // mod reduction already done. + UNREACHABLE(); + break; } } }