ensure encapsulation boundaries

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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());

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<int> m_data;
-    vector<int> m_resize_buffer;
+    svector<int> m_data;
+    svector<int> m_resize_buffer;
+    unsigned_vector m_index;
+
 public:
-    vector<int> 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(); }
 };
 }

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<int> 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<mpq>();
 
     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<unsigned> became_feas;
     clean_popped_elements(A_r().column_count(), m_mpq_lar_core_solver.m_r_solver.m_inf_set);
     std::unordered_set<unsigned> 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);

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";
               }

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<unsigned>(j))
                 j = static_cast<int>(k);
         }