From f501aea3ebb28179bc272bc773d9ac08166b306d Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 12 Mar 2025 10:10:03 -1000 Subject: [PATCH] add comments and renaming Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 18 ++++++++++-------- src/math/lp/lar_solver.cpp | 30 +++++++++--------------------- src/math/lp/lar_solver.h | 2 -- 3 files changed, 19 insertions(+), 31 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index c78053e8b..88d7cd997 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -484,7 +484,9 @@ namespace lp { std::unordered_map> m_row2fresh_defs; indexed_uint_set m_changed_rows; - indexed_uint_set m_new_fixed_columns; + // m_changed_columns are the columns that just became fixed, or those that just stopped being fixed. + // If such a column appears in an entry it has to be recalculated. + indexed_uint_set m_changed_columns; indexed_uint_set m_changed_terms; // a term is defined by its column j, as in lar_solver.get_term(j) indexed_uint_set m_tightened_columns; // the column that got tightened by the tigthening phase, // m_column_to_terms[j] is the set of all k such lra.get_term(k) depends on j @@ -721,7 +723,7 @@ namespace lp { void add_changed_column(unsigned j) { TRACE("dio", lra.print_column_info(j, tout);); - m_new_fixed_columns.insert(j); + m_changed_columns.insert(j); } std_vector m_added_terms; std::unordered_set m_active_terms; @@ -751,7 +753,7 @@ namespace lp { void update_column_bound_callback(unsigned j) { if (!lra.column_is_int(j) || !lra.column_is_fixed(j)) return; - m_new_fixed_columns.insert(j); + m_changed_columns.insert(j); auto undo = undo_fixed_column(*this, j); lra.trail().push(undo); } @@ -932,7 +934,7 @@ namespace lp { } void find_changed_terms_and_more_changed_rows() { - for (unsigned j : m_new_fixed_columns) { + for (unsigned j : m_changed_columns) { const auto it = m_columns_to_terms.find(j); if (it != m_columns_to_terms.end()) for (unsigned k : it->second) { @@ -1025,8 +1027,8 @@ namespace lp { remove_irrelevant_fresh_defs(); eliminate_substituted_in_changed_rows(); - m_new_fixed_columns.reset(); - SASSERT(m_new_fixed_columns.size() == 0); + m_changed_columns.reset(); + SASSERT(m_changed_columns.size() == 0); m_changed_rows.reset(); SASSERT(entries_are_ok()); } @@ -1500,7 +1502,7 @@ namespace lp { if (tighten_bounds_for_non_trivial_gcd(g, j, false) != lia_move::undef) { return lia_move::conflict; } - if (m_new_fixed_columns.contains(j)) { + if (m_changed_columns.contains(j)) { return lia_move::continue_with_check; } return lia_move::undef; @@ -1743,7 +1745,7 @@ namespace lp { if (r == lia_move::conflict || r == lia_move::undef) { break; } - SASSERT(m_new_fixed_columns.size() == 0); + SASSERT(m_changed_columns.size() == 0); } while (f_vector.size()); if (r == lia_move::conflict) { diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index c0eac9dc3..e04f9c006 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1997,6 +1997,15 @@ namespace lp { TRACE("lar_solver_feas", tout << "j = " << j << " became " << (this->column_is_feasible(j) ? "feas" : "non-feas") << ", and " << (this->column_is_bounded(j) ? "bounded" : "non-bounded") << std::endl;); if (m_update_column_bound_callback) m_update_column_bound_callback(j); + + if (settings().dump_bound_lemmas()) { + if (kind == LE) + write_bound_lemma(j, false, __func__, std::cout); + else if (kind == GE) + write_bound_lemma(j, true, __func__, std::cout); + else + NOT_IMPLEMENTED_YET(); + } } void lar_solver::insert_to_columns_with_changed_bounds(unsigned j) { @@ -2509,24 +2518,6 @@ namespace lp { // Otherwise the new asserted lower bound is is greater than the existing upper bound. // dep is the reason for the new bound - void lar_solver::write_bound_lemma_to_file(unsigned j, bool is_low, const std::string & file_name, const std::string& location) const { - std::ofstream file(file_name); - if (!file.is_open()) { - // Handle file open error - std::cerr << "Failed to open file: " << file_name << std::endl; - return; - } - - write_bound_lemma(j, is_low, location, file); - file.close(); - - if (file.fail()) { - std::cerr << "Error occurred while writing to file: " << file_name << std::endl; - } else { - std::cout << "Bound lemma written to " << file_name << std::endl; - } - } - void lar_solver::set_crossed_bounds_column_and_deps(unsigned j, bool lower_bound, u_dependency* dep) { if (m_crossed_bounds_column != null_lpvar) return; // already set SASSERT(m_crossed_bounds_deps == nullptr); @@ -2557,9 +2548,6 @@ namespace lp { return out; } - - - // Helper function to format constants in SMT2 format std::string format_smt2_constant(const mpq& val) { if (val.is_neg()) { diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 9c6212c3c..bd02cfc13 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -726,8 +726,6 @@ public: return m_usage_in_terms[j]; } - void write_bound_lemma_to_file(unsigned j, bool is_low, const std::string & file_name, const std::string & location) const; - void write_bound_lemma(unsigned j, bool is_low, const std::string & location, std::ostream & out) const; std::function m_find_monics_with_changed_bounds_func = nullptr;