From e41acd7b50534778700aa7121b8af726940b79ff Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 23 Apr 2025 16:33:38 -0700 Subject: [PATCH] convert m_r_upper and m_r_lower bounds to plain vectors manage backtracking state together with backtracking of column data. --- src/math/lp/int_branch.cpp | 4 ++-- src/math/lp/lar_core_solver.h | 10 +++----- src/math/lp/lar_core_solver_def.h | 4 ++-- src/math/lp/lar_solver.cpp | 40 +++++++++++++++++++++---------- src/math/lp/lar_solver.h | 10 ++++++++ src/math/lp/lp_core_solver_base.h | 2 +- 6 files changed, 46 insertions(+), 24 deletions(-) diff --git a/src/math/lp/int_branch.cpp b/src/math/lp/int_branch.cpp index a5ce3c291..fd8fd305b 100644 --- a/src/math/lp/int_branch.cpp +++ b/src/math/lp/int_branch.cpp @@ -75,7 +75,7 @@ int int_branch::find_inf_int_base_column() { if (!lia.column_is_int_inf(j)) continue; usage = lra.usage_in_terms(j); - if (lia.is_boxed(j) && (range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage)) <= small_value) { + if (lia.is_boxed(j) && (range = lcs.m_r_upper_bounds[j].x - lcs.m_r_lower_bounds[j].x - rational(2*usage)) <= small_value) { result = j; k++; n = 1; @@ -98,7 +98,7 @@ int int_branch::find_inf_int_base_column() { continue; SASSERT(!lia.is_fixed(j)); usage = lra.usage_in_terms(j); - new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage); + new_range = lcs.m_r_upper_bounds[j].x - lcs.m_r_lower_bounds[j].x - rational(2*usage); if (new_range < range) { n = 1; result = j; diff --git a/src/math/lp/lar_core_solver.h b/src/math/lp/lar_core_solver.h index 6ea5f7d50..552874cec 100644 --- a/src/math/lp/lar_core_solver.h +++ b/src/math/lp/lar_core_solver.h @@ -29,8 +29,8 @@ public: stacked_vector m_column_types; // r - solver fields, for rational numbers - stacked_vector> m_r_lower_bounds; - stacked_vector> m_r_upper_bounds; + vector> m_r_lower_bounds; + vector> m_r_upper_bounds; static_matrix> m_r_A; stacked_vector m_r_pushed_basis; vector m_r_basis; @@ -121,15 +121,11 @@ public: m_stacked_simplex_strategy = settings().simplex_strategy(); m_stacked_simplex_strategy.push(); m_column_types.push(); - // rational - m_r_lower_bounds.push(); - m_r_upper_bounds.push(); + // rational } void pop(unsigned k) { // rationals - m_r_lower_bounds.pop(k); - m_r_upper_bounds.pop(k); m_column_types.pop(k); m_r_x.resize(m_r_A.column_count()); diff --git a/src/math/lp/lar_core_solver_def.h b/src/math/lp/lar_core_solver_def.h index 5dbd32cb5..29d93405b 100644 --- a/src/math/lp/lar_core_solver_def.h +++ b/src/math/lp/lar_core_solver_def.h @@ -27,8 +27,8 @@ lar_core_solver::lar_core_solver( m_r_heading, m_costs_dummy, m_column_types(), - m_r_lower_bounds(), - m_r_upper_bounds(), + m_r_lower_bounds, + m_r_upper_bounds, settings, column_names) { } diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 4d6846c32..bb4f5be06 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -421,14 +421,14 @@ namespace lp { auto& val = lcs.r_x(j); switch (lcs.m_column_types()[j]) { case column_type::boxed: { - const auto& l = lcs.m_r_lower_bounds()[j]; - if (val == l || val == lcs.m_r_upper_bounds()[j]) return false; + const auto& l = lcs.m_r_lower_bounds[j]; + if (val == l || val == lcs.m_r_upper_bounds[j]) return false; set_value_for_nbasic_column(j, l); return true; } case column_type::lower_bound: { - const auto& l = lcs.m_r_lower_bounds()[j]; + const auto& l = lcs.m_r_lower_bounds[j]; if (val != l) { set_value_for_nbasic_column(j, l); return true; @@ -437,7 +437,7 @@ namespace lp { } case column_type::fixed: case column_type::upper_bound: { - const auto & u = lcs.m_r_upper_bounds()[j]; + const auto & u = lcs.m_r_upper_bounds[j]; if (val != u) { set_value_for_nbasic_column(j, u); return true; @@ -574,15 +574,31 @@ namespace lp { A_r().pop(k); } + struct lar_solver::column_update_trail : public trail { + lar_solver& s; + column_update_trail(lar_solver& s) : s(s) {} + void undo() override { + auto& [is_upper, j, bound, column] = s.m_column_updates.back(); + if (is_upper) + s.m_mpq_lar_core_solver.m_r_upper_bounds[j] = bound; + else + s.m_mpq_lar_core_solver.m_r_lower_bounds[j] = bound; + s.m_columns[j] = column; + s.m_column_updates.pop_back(); + } + }; + void lar_solver::set_upper_bound_witness(lpvar j, u_dependency* dep, impq const& high) { - m_trail.push(vector_value_trail(m_columns, j)); + m_column_updates.push_back({true, j, get_upper_bound(j), m_columns[j]}); + m_trail.push(column_update_trail(*this)); m_columns[j].set_upper_bound_witness(dep); m_mpq_lar_core_solver.m_r_upper_bounds[j] = high; insert_to_columns_with_changed_bounds(j); } void lar_solver::set_lower_bound_witness(lpvar j, u_dependency* dep, impq const& low) { - m_trail.push(vector_value_trail(m_columns, j)); + m_column_updates.push_back({false, j, get_lower_bound(j), m_columns[j]}); + m_trail.push(column_update_trail(*this)); m_columns[j].set_lower_bound_witness(dep); m_mpq_lar_core_solver.m_r_lower_bounds[j] = low; insert_to_columns_with_changed_bounds(j); @@ -1084,7 +1100,7 @@ namespace lp { const column& ul = m_columns[var]; dep = ul.lower_bound_witness(); if (dep != nullptr) { - auto& p = m_mpq_lar_core_solver.m_r_lower_bounds()[var]; + auto& p = m_mpq_lar_core_solver.m_r_lower_bounds[var]; value = p.x; is_strict = p.y.is_pos(); return true; @@ -1103,7 +1119,7 @@ namespace lp { const column& ul = m_columns[var]; dep = ul.upper_bound_witness(); if (dep != nullptr) { - auto& p = m_mpq_lar_core_solver.m_r_upper_bounds()[var]; + auto& p = m_mpq_lar_core_solver.m_r_upper_bounds[var]; value = p.x; is_strict = p.y.is_neg(); return true; @@ -1625,8 +1641,8 @@ namespace lp { // SASSERT(m_mpq_lar_core_solver.m_r_lower_bounds.size() == j && m_mpq_lar_core_solver.m_r_upper_bounds.size() == j); // restore later m_mpq_lar_core_solver.resize_x(j + 1); auto& rslv = m_mpq_lar_core_solver.m_r_solver; - m_mpq_lar_core_solver.m_r_lower_bounds.increase_size_by_one(); - m_mpq_lar_core_solver.m_r_upper_bounds.increase_size_by_one(); + m_mpq_lar_core_solver.m_r_lower_bounds.reserve(j + 1); + m_mpq_lar_core_solver.m_r_upper_bounds.reserve(j + 1); rslv.inf_heap_increase_size_by_one(); rslv.m_costs.resize(j + 1); rslv.m_d.resize(j + 1); @@ -2264,9 +2280,9 @@ namespace lp { impq ivalue(value); auto& lcs = m_mpq_lar_core_solver; - if (column_has_upper_bound(j) && lcs.m_r_upper_bounds()[j] < ivalue) + if (column_has_upper_bound(j) && lcs.m_r_upper_bounds[j] < ivalue) return false; - if (column_has_lower_bound(j) && lcs.m_r_lower_bounds()[j] > ivalue) + if (column_has_lower_bound(j) && lcs.m_r_lower_bounds[j] > ivalue) return false; set_value_for_nbasic_column(j, ivalue); diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 372cc502b..15c4facc6 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -73,6 +73,14 @@ class lar_solver : public column_namer { } }; + struct column_update { + bool is_upper; + unsigned j; + impq bound; + column column; + }; + struct column_update_trail; + //////////////////// fields ////////////////////////// trail_stack m_trail; lp_settings m_settings; @@ -86,6 +94,8 @@ class lar_solver : public column_namer { bool m_need_register_terms = false; var_register m_var_register; svector m_columns; + vector m_column_updates; + constraint_set m_constraints; // the set of column indices j such that bounds have changed for j indexed_uint_set m_columns_with_changed_bounds; diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h index 1656545ea..239031d4e 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -437,7 +437,7 @@ public: } 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()) { + if (j >= m_column_types.size()) { out << "[" << j << "] is not present\n"; return out; }