restore move_non_basic_to_bounds

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Z3Prover · Oct 6, 2023 · bf3817e · bf3817e
1 parent b61f4ac
commit bf3817e
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 8 deletions.
diff --git a/src/math/lp/core_solver_pretty_printer_def.h b/src/math/lp/core_solver_pretty_printer_def.h
@@ -279,10 +279,12 @@ template <typename T, typename X> void core_solver_pretty_printer<T, X>::print()
         print_row(i);
     }
     m_out << std::endl;
-    if (m_core_solver.inf_heap().size()) {
-        m_out << "inf columns: ";
+    if (!m_core_solver.inf_heap().empty()) {
+        m_out << "inf columns: size() = " << m_core_solver.inf_heap().size() << std::endl;
         print_vector(m_core_solver.inf_heap(), m_out);
         m_out << std::endl;
+    } else {
+        m_out << "inf columns: none\n";
     }
 }
 

diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
@@ -181,7 +181,10 @@ namespace lp {
 
     lp_status lar_solver::get_status() const { return m_status; }
 
-    void lar_solver::set_status(lp_status s) { m_status = s; }
+    void lar_solver::set_status(lp_status s) { 
+        TRACE("lar_solver", tout << "setting status to " << s << "\n";);
+        m_status = s; 
+    }
 
     lp_status lar_solver::find_feasible_solution() {
         stats().m_make_feasible++;
@@ -419,9 +422,7 @@ namespace lp {
     void lar_solver::move_non_basic_columns_to_bounds(bool shift_randomly) {
         auto& lcs = m_mpq_lar_core_solver;
         bool change = false;
-        for (unsigned j : m_columns_with_changed_bounds) {
-            if (lcs.m_r_heading[j] >= 0)
-                continue;
+        for (unsigned j : lcs.m_r_nbasis) {
             if (move_non_basic_column_to_bounds(j, shift_randomly))
                 change = true;
         }
@@ -439,7 +440,7 @@ namespace lp {
         switch (lcs.m_column_types()[j]) {
         case column_type::boxed: {
             bool at_l = val == lcs.m_r_lower_bounds()[j];
-            bool at_u = !at_l && (val == lcs.m_r_upper_bounds()[j]);
+            bool at_u = (!at_l && (val == lcs.m_r_upper_bounds()[j]));
             if (!at_l && !at_u) {
                 if (m_settings.random_next() % 2)
                     set_value_for_nbasic_column(j, lcs.m_r_lower_bounds()[j]);

diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h
@@ -564,6 +564,7 @@ class lp_core_solver_base {
     }
     void insert_column_into_inf_heap(unsigned j) {        
 		if (!m_inf_heap.contains(j)) {
+            m_inf_heap.reserve(j+1);
 	        m_inf_heap.insert(j);
             TRACE("lar_solver_inf_heap", tout << "insert into inf_heap j = " << j << "\n";);
         }

diff --git a/src/util/heap.h b/src/util/heap.h
@@ -159,7 +159,7 @@ class heap : private LT {
     }
 
     unsigned size() const {
-        return m_value2indices.size();
+        return m_values.size() - 1;
     }
 
     void reserve(int s) {