From 1af2474f7bf504ff1af697f977c9c606a3dc9a82 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 16 Mar 2025 18:44:40 -0700 Subject: [PATCH] code review updates, tidy pretty printer for column info Signed-off-by: Nikolaj Bjorner --- src/math/lp/dioph_eq.cpp | 33 +++++++++++++------------------ src/math/lp/lar_solver.h | 7 ++++--- src/math/lp/lp_core_solver_base.h | 21 +++++++++++++------- 3 files changed, 32 insertions(+), 29 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index c6570eada..a26e07250 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -541,10 +541,10 @@ namespace lp { TRACE("d_undo", tout << "t:" << t << ", t->j():" << t->j() << std::endl;); TRACE("dioph_eq", lra.print_term(*t, tout); tout << ", t->j() =" << t->j() << std::endl;); if (!contains(m_active_terms, t)) { - for (int i = static_cast(m_added_terms.size() - 1); i >= 0; --i) { - if (m_added_terms[i] != t) continue; - if ((unsigned)i != m_added_terms.size() - 1) - m_added_terms[i] = m_added_terms.back(); + for (auto i = m_added_terms.size(); i-- > 0; ) { + if (m_added_terms[i] != t) + continue; + m_added_terms[i] = m_added_terms.back(); m_added_terms.pop_back(); break; // all is done since the term has not made it to m_active_terms } @@ -679,15 +679,13 @@ namespace lp { void make_sure_j_is_in_the_last_row_of_l_matrix() { unsigned j = m_l_matrix.column_count() - 1; const auto& last_e_row = m_l_matrix.m_rows.back(); - mpq alpha; - for (const auto& p : last_e_row) { - if (p.var() == j) { - return; - } - } - SASSERT(m_l_matrix.m_columns.back().size()); + if (any_of(last_e_row, [j](auto const& p) { return p.var() == j; })) + return; + SASSERT(m_l_matrix.m_columns.back().size() > 0); unsigned i = m_l_matrix.m_columns[j][0].var(); m_l_matrix.add_rows(mpq(1), i, m_l_matrix.row_count() - 1); + // what is the post-condition? Is 'j' used in the post-condition or is it 'i'? + // SASSERT(any_of(m_l_matrix.m_rows.back(), [i](auto const& p) { return p.var() == i; })); } void shrink_matrices() { @@ -705,9 +703,8 @@ namespace lp { remove_irrelevant_fresh_defs_for_row(i); - if (m_k2s.has_val(i)) { + if (m_k2s.has_val(i)) remove_from_S(i); - } m_sum_of_fixed.pop_back(); } @@ -760,7 +757,7 @@ namespace lp { TRACE("dio", tout << "marked term change j:" << j << std::endl;); m_changed_terms.insert(j); } - + void update_column_bound_callback(unsigned j) { if (!lra.column_is_int(j) || !lra.column_is_fixed(j)) return; @@ -1158,12 +1155,9 @@ namespace lp { template bool has_fresh_var(const T& t) const { - for (const auto& p : t) { - if (var_is_fresh(p.var())) - return true; - } - return false; + return any_of(t, [&](auto const& p) { return var_is_fresh(p.var()); }); } + bool has_fresh_var(unsigned row_index) const { return has_fresh_var(m_e_matrix[row_index]); } @@ -1417,6 +1411,7 @@ namespace lp { TRACE("dio", tout << "changed terms:"; for (auto j : sorted_changed_terms) tout << j << " "; tout << std::endl; print_S(tout); + // lra.display(tout); // print_bounds(tout); ); for (unsigned j : sorted_changed_terms) { diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 8cf9f8a11..575184b4f 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -618,11 +618,12 @@ public: inline bool column_has_term(lpvar j) const { return m_columns[j].term() != nullptr; } std::ostream& print_column_info(unsigned j, std::ostream& out, bool print_expl = false) const { - m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out); + m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out, false); if (column_has_term(j)) - print_term_as_indices(get_term(j), out) << "\n"; + print_term_as_indices(get_term(j), out << " := ") << " "; + out << "\n"; if (print_expl) - display_column_explanation(out, j); + display_column_explanation(out, j); return out; } diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h index bd33e39ff..67f7ffb6c 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -436,7 +436,7 @@ public: return out; } - std::ostream& print_column_info(unsigned j, std::ostream & out, const std::string& var_prefix = "x") const { + std::ostream& print_column_info(unsigned j, std::ostream & out, bool print_nl = false, const std::string& var_prefix = "j") const { if (j >= m_lower_bounds.size()) { out << "[" << j << "] is not present\n"; return out; @@ -446,12 +446,15 @@ public: strm << m_x[j]; std::string j_val = strm.str(); out << var_prefix << j << " = " << std::setw(6) << j_val; - if (m_basis_heading[j] >= 0) - out << " base "; - else - out << " "; - for (auto k = j_val.size(); k < 15; ++k) + if (j < 10) + out << " "; + else if (j < 100) out << " "; + + if (m_basis_heading[j] >= 0) + out << " base "; + else + out << " "; switch (m_column_types[j]) { case column_type::fixed: case column_type::boxed: @@ -469,7 +472,11 @@ public: default: UNREACHABLE(); } - return out << "\n"; + if (print_nl) + out << "\n"; + else + out << "\t"; + return out; } bool column_is_fixed(unsigned j) const { return this->m_column_types[j] == column_type::fixed; }