From c1ece496945314d2fe7d4a9c017d1a2d065e1de9 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sun, 29 Dec 2024 13:22:47 -1000 Subject: [PATCH] track changed columns in dio\ Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 51 ++++++++++++++++++++++++++++++++------ src/math/lp/lar_solver.cpp | 13 +++++----- src/math/lp/lar_solver.h | 6 ++--- 3 files changed, 53 insertions(+), 17 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 1141dc073..46286e35b 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -240,7 +240,7 @@ namespace lp { unsigned m_conflict_index = -1; // m_entries[m_conflict_index] gives the conflict unsigned m_max_number_of_iterations = 100; unsigned m_number_of_iterations; - std_vector> m_columns_to_entries; // m_columnn_to_terms[j] is the set of of all k such that m_entry[k].m_l depends on j + std::unordered_map> m_columns_to_term_columns; // m_columnn_to_term_columns[j] is the set of of all k such that lra.get_term(k) depends on j struct branch { unsigned m_j = UINT_MAX; mpq m_rs; @@ -290,16 +290,19 @@ namespace lp { }; - struct undo_add_column_bound : public trail { + struct undo_change_column_bound : public trail { imp& m_s; unsigned m_j; // the column that has been added - undo_add_column_bound(imp& s, unsigned j) : m_s(s), m_j(j) {} + undo_change_column_bound(imp& s, unsigned j) : m_s(s), m_j(j) {} void undo() override { - NOT_IMPLEMENTED_YET(); + m_s.add_changed_column(m_j); } }; + uint_set m_changed_columns; // the columns are given as lar_solver columns + friend undo_change_column_bound; + void add_changed_column(unsigned j) { m_changed_columns.insert(j);} std_vector m_added_terms; std_vector m_branch_stats; @@ -318,17 +321,17 @@ namespace lp { lra.trail().push(undo); } - void add_column_bound_delegate(unsigned j) { + void update_column_bound_delegate(unsigned j) { if (!lra.column_is_int(j)) return; - auto undo = undo_add_column_bound(*this, j); + auto undo = undo_change_column_bound(*this, j); lra.trail().push(undo) ; } public: imp(int_solver& lia, lar_solver& lra) : lia(lia), lra(lra) { lra.register_add_term_delegate([this](const lar_term*t){add_term_delegate(t);}); - lra.register_add_column_bound_delegate([this](unsigned j) {add_column_bound_delegate(j);}); + lra.register_update_column_bound_delegate([this](unsigned j) {update_column_bound_delegate(j);}); } term_o get_term_from_entry(unsigned i) const { term_o t; @@ -348,6 +351,22 @@ namespace lp { return m_var_register.local_to_external(j); } + void register_term_columns(const lar_term & t) { + for (const auto & p : t) { + register_term_column(p.j(), t); + } + } + void register_term_column(unsigned j, const lar_term& t) { + auto it = m_columns_to_term_columns.find(j); + if (it != m_columns_to_term_columns.end()) + it->second.insert(t.j()); + else { + auto s = std::unordered_set(); + s.insert(t.j()); + m_columns_to_term_columns[j] = s; + } + + } // the term has form sum(a_i*x_i) - t.j() = 0, void fill_entry(const lar_term& t) { TRACE("dioph_eq", print_lar_term_L(t, tout) << std::endl;); @@ -383,7 +402,7 @@ namespace lp { m_e_matrix.add_columns_up_to(lj); m_e_matrix.add_new_element(entry_index, lj, -mpq(1)); } - TRACE("dioph_eq", print_entry(entry_index, tout);); + register_term_columns(t); SASSERT(entry_invariant(entry_index)); } @@ -394,6 +413,21 @@ namespace lp { } return true; } + void process_changed_columns() { + std::unordered_set entries_to_recalculate; + for (unsigned j : m_changed_columns) { + for (unsigned k : m_columns_to_term_columns[j]) { + for (const auto& p : m_l_matrix.column(k)) { + entries_to_recalculate.insert(p.var()); + } + } + } + + if (entries_to_recalculate.size() > 0) + NOT_IMPLEMENTED_YET(); + + m_changed_columns.reset(); + } void init() { m_report_branch = false; @@ -403,6 +437,7 @@ namespace lp { m_number_of_iterations = 0; m_branch_stack.clear(); m_lra_level = 0; + process_changed_columns(); for (const lar_term* t: m_added_terms) { fill_entry(*t); } diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 3ddc00334..723bdebbb 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1600,10 +1600,10 @@ namespace lp { return m_var_register.external_is_used(v); } void lar_solver::register_add_term_delegate(const std::function& f) { - this->m_add_term_delegates.push_back(f); + this->m_add_term_callbacks.push_back(f); } - void lar_solver::register_add_column_bound_delegate(const std::function& f) { - this->m_add_column_bound_delegates.push_back(f); + void lar_solver::register_update_column_bound_delegate(const std::function& f) { + this->m_update_column_bound_callbacks.push_back(f); } void lar_solver::add_non_basic_var_to_core_fields(unsigned ext_j, bool is_int) { @@ -1702,7 +1702,7 @@ namespace lp { lp_assert(m_var_register.size() == A_r().column_count()); if (m_need_register_terms) register_normalized_term(*t, A_r().column_count() - 1); - for (const auto & f: m_add_term_delegates) + for (const auto & f: m_add_term_callbacks) f(t); return ret; } @@ -1751,8 +1751,6 @@ namespace lp { constraint_index lar_solver::add_var_bound(lpvar j, lconstraint_kind kind, const mpq& right_side) { constraint_index ci = mk_var_bound(j, kind, right_side); activate(ci); - for (const auto & f: m_add_column_bound_delegates) - f(j); return ci; } @@ -1992,6 +1990,9 @@ 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;); + for (const auto &f: m_update_column_bound_callbacks) { + f(j); + } } void lar_solver::insert_to_columns_with_changed_bounds(unsigned j) { diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index cd1dd9664..8bd83e004 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -406,11 +406,11 @@ public: } void register_add_term_delegate(const std::function&); - void register_add_column_bound_delegate(const std::function&); + void register_update_column_bound_delegate(const std::function&); private: - std_vector> m_add_term_delegates; - std_vector> m_add_column_bound_delegates; + std_vector> m_add_term_callbacks; + std_vector> m_update_column_bound_callbacks; public: bool external_is_used(unsigned) const; void pop(unsigned k);