add ability to touch variables for bound propagation

src/math/lp/lar_solver.cpp

@@ -345,7 +345,7 @@ void lar_solver::set_costs_to_zero(const lar_term& term) {
             jset.insert(j);
         else {
             for (const auto & rc : A_r().m_rows[i])
-                    jset.insert(rc.var());
+                jset.insert(rc.var());
         }
     }
 
@@ -1269,6 +1269,14 @@ void lar_solver::random_update(unsigned sz, var_index const * vars) {
     ru.update();
 }
 
+void lar_solver::mark_rows_for_bound_prop(lpvar j) {
+    auto & column = A_r().m_columns[j];
+    for (auto const& r : column) {
+        m_rows_with_changed_bounds.insert(r.var());
+    }
+}
+
+
 
 void lar_solver::pivot_fixed_vars_from_basis() {
     m_mpq_lar_core_solver.m_r_solver.pivot_fixed_vars_from_basis();

src/math/lp/lar_solver.h

@@ -349,6 +349,7 @@ public:
     void activate_check_on_equal(constraint_index, var_index&);
     void activate(constraint_index);
     void random_update(unsigned sz, var_index const * vars);
+    void mark_rows_for_bound_prop(lpvar j);
     template <typename T>
     void propagate_bounds_for_touched_rows(lp_bound_propagator<T> & bp) {
         SASSERT(use_tableau());

src/math/lp/lp_settings.h

@@ -39,6 +39,16 @@ enum class column_type  {
     fixed = 4
 };
 
+inline std::ostream& operator<<(std::ostream& out, column_type const& t) {
+    switch (t) {
+    case column_type::free_column: return out << "free";
+    case column_type::lower_bound: return out << "lower";
+    case column_type::upper_bound: return out << "upper";
+    case column_type::boxed: return out << "boxed";
+    case column_type::fixed: return out << "fixed";
+    }
+}
+
 enum class simplex_strategy_enum {
     undecided = 3,
     tableau_rows = 0,

src/math/lp/static_matrix.h

@@ -46,6 +46,12 @@ typedef vector<column_cell> column_strip;
 
 template <typename T>
 using row_strip = vector<row_cell<T>>; 
+template <typename T>
+std::ostream& operator<<(std::ostream& out, const row_strip<T>& r) {
+    for (auto const& c : r)
+        out << c << " ";
+    return out << "\n";
+}
 
 // each assignment for this matrix should be issued only once!!!
 template <typename T, typename X>