From 2975873b914b075cf734a912036f06bdfd6256d0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Mar 2020 19:29:59 -0700 Subject: [PATCH] ensure encapsulation boundaries Signed-off-by: Nikolaj Bjorner --- src/math/lp/emonics.cpp | 4 ++-- src/math/lp/int_set.h | 21 +++++++++++++++------ src/math/lp/lar_solver.cpp | 20 ++++++++++---------- src/math/lp/lp_core_solver_base.h | 4 ++-- src/math/lp/lp_primal_core_solver.h | 2 +- 5 files changed, 30 insertions(+), 21 deletions(-) diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp index efeb56c57..e691480e3 100644 --- a/src/math/lp/emonics.cpp +++ b/src/math/lp/emonics.cpp @@ -431,7 +431,7 @@ void emonics::merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v } void emonics::after_merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) { - if (m_ve.find(~r1) == m_ve.find(~r2) && r1.var() != r2.var()) { // the other sign has also been merged + if (m_ve.find(~r1) == m_ve.find(~r2)) { // the other sign has also been merged TRACE("nla_solver_mons", tout << r2 << " <- " << r1 << "\n";); m_use_lists.reserve(std::max(r2.var(), r1.var()) + 1); TRACE("nla_solver_mons", tout << "rehashing " << r1.var() << "\n";); @@ -441,7 +441,7 @@ void emonics::after_merge_eh(signed_var r2, signed_var r1, signed_var v2, signed } void emonics::unmerge_eh(signed_var r2, signed_var r1) { - if (m_ve.find(~r1) != m_ve.find(~r2) && r1.var() != r2.var()) { // the other sign has also been unmerged + if (m_ve.find(~r1) != m_ve.find(~r2)) { // the other sign has also been unmerged TRACE("nla_solver_mons", tout << r2 << " -> " << r1 << "\n";); unmerge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]); rehash_cg(r1.var()); diff --git a/src/math/lp/int_set.h b/src/math/lp/int_set.h index ca698be3e..be45714bf 100644 --- a/src/math/lp/int_set.h +++ b/src/math/lp/int_set.h @@ -15,6 +15,7 @@ Author: Revision History: + TBD use indexed_uint_set from src/util/uint_set.h, --*/ #pragma once @@ -23,12 +24,18 @@ Revision History: namespace lp { // serves at a set of non-negative integers smaller than the set size class int_set { - vector m_data; - vector m_resize_buffer; + svector m_data; + svector m_resize_buffer; + unsigned_vector m_index; + public: - vector m_index; int_set(unsigned size): m_data(size, -1) {} int_set() {} + int_set(int_set const& other): + m_data(other.m_data), + m_resize_buffer(other.m_resize_buffer), + m_index(other.m_index) {} + bool contains(unsigned j) const { if (j >= m_data.size()) return false; @@ -81,13 +88,15 @@ public: m_data[j] = -1; m_index.resize(0); } - void print(std::ostream & out ) const { + + std::ostream& operator<<(std::ostream& out) const { for (unsigned j : m_index) { out << j << " "; } out << std::endl; + return out; } - const int * begin() const { return m_index.begin(); } - const int * end() const { return m_index.end(); } + const unsigned * begin() const { return m_index.begin(); } + const unsigned * end() const { return m_index.end(); } }; } diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index f7f6a6f1d..c27fd6bc9 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -250,7 +250,7 @@ void lar_solver::propagate_bounds_for_touched_rows(lp_bound_propagator & bp) { if (!use_tableau()) return; // todo: consider to remove the restriction - for (unsigned i : m_rows_with_changed_bounds.m_index) { + for (unsigned i : m_rows_with_changed_bounds) { calculate_implied_bounds_for_row(i, bp); if (settings().get_cancel_flag()) return; @@ -326,7 +326,7 @@ void lar_solver::push() { void lar_solver::clean_popped_elements(unsigned n, int_set& set) { vector to_remove; - for (unsigned j: set.m_index) + for (unsigned j: set) if (j >= n) to_remove.push_back(j); for (unsigned j : to_remove) @@ -418,7 +418,7 @@ bool lar_solver::reduced_costs_are_zeroes_for_r_solver() const { void lar_solver::set_costs_to_zero(const lar_term& term) { auto & rslv = m_mpq_lar_core_solver.m_r_solver; auto & jset = m_mpq_lar_core_solver.m_r_solver.m_inf_set; // hijack this set that should be empty right now - lp_assert(jset.m_index.size()==0); + lp_assert(jset.is_empty()); for (const auto & p : term) { unsigned j = p.var(); @@ -432,7 +432,7 @@ void lar_solver::set_costs_to_zero(const lar_term& term) { } } - for (unsigned j : jset.m_index) + for (unsigned j : jset) rslv.m_d[j] = zero_of_type(); jset.clear(); @@ -808,22 +808,22 @@ void lar_solver::detect_rows_with_changed_bounds_for_column(unsigned j) { } void lar_solver::detect_rows_with_changed_bounds() { - for (auto j : m_columns_with_changed_bound.m_index) + for (auto j : m_columns_with_changed_bound) detect_rows_with_changed_bounds_for_column(j); } void lar_solver::update_x_and_inf_costs_for_columns_with_changed_bounds() { - for (auto j : m_columns_with_changed_bound.m_index) + for (auto j : m_columns_with_changed_bound) update_x_and_inf_costs_for_column_with_changed_bounds(j); } void lar_solver::update_x_and_inf_costs_for_columns_with_changed_bounds_tableau() { - for (auto j : m_columns_with_changed_bound.m_index) + for (auto j : m_columns_with_changed_bound) update_x_and_inf_costs_for_column_with_changed_bounds(j); if (tableau_with_costs()) { if (m_mpq_lar_core_solver.m_r_solver.m_using_infeas_costs) { - for (unsigned j : m_basic_columns_with_changed_cost.m_index) + for (unsigned j : m_basic_columns_with_changed_cost) m_mpq_lar_core_solver.m_r_solver.update_inf_cost_for_column_tableau(j); lp_assert(m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); } @@ -1477,7 +1477,7 @@ void lar_solver::clean_inf_set_of_r_solver_after_pop() { vector became_feas; clean_popped_elements(A_r().column_count(), m_mpq_lar_core_solver.m_r_solver.m_inf_set); std::unordered_set basic_columns_with_changed_cost; - auto inf_index_copy = m_mpq_lar_core_solver.m_r_solver.m_inf_set.m_index; + auto inf_index_copy = m_mpq_lar_core_solver.m_r_solver.m_inf_set; for (auto j: inf_index_copy) { if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) { continue; @@ -1498,7 +1498,7 @@ void lar_solver::clean_inf_set_of_r_solver_after_pop() { m_mpq_lar_core_solver.m_r_solver.m_inf_set.erase(j); } became_feas.clear(); - for (unsigned j : m_mpq_lar_core_solver.m_r_solver.m_inf_set.m_index) { + for (unsigned j : m_mpq_lar_core_solver.m_r_solver.m_inf_set) { lp_assert(m_mpq_lar_core_solver.m_r_heading[j] >= 0); if (m_mpq_lar_core_solver.m_r_solver.column_is_feasible(j)) became_feas.push_back(j); diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h index 22cdae336..a932bc615 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -42,8 +42,8 @@ public: bool current_x_is_feasible() const { TRACE("feas", if (m_inf_set.size()) { - tout << "column " << m_inf_set.m_index[0] << " is infeasible" << std::endl; - print_column_info(m_inf_set.m_index[0], tout); + tout << "column " << *m_inf_set.begin() << " is infeasible" << std::endl; + print_column_info(*m_inf_set.begin(), tout); } else { tout << "x is feasible\n"; } diff --git a/src/math/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h index 98c8be009..e891e6a3e 100644 --- a/src/math/lp/lp_primal_core_solver.h +++ b/src/math/lp/lp_primal_core_solver.h @@ -450,7 +450,7 @@ public: int find_leaving_tableau_rows(X & new_val_for_leaving) { int j = -1; - for (unsigned k : this->m_inf_set.m_index) { + for (unsigned k : this->m_inf_set) { if (k < static_cast(j)) j = static_cast(k); }