From ff875c936fdf1da3c863a7cda23ac2e38fddd37f Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 6 Jul 2023 16:45:22 -0700
Subject: [PATCH] add TRACE stmts, more efficient remove from inf_heap

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/lar_solver.h            | 4 ----
 src/math/lp/lp_core_solver_base.h   | 6 +++---
 src/math/lp/lp_primal_core_solver.h | 6 +++++-
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 96af2d4ce..fd6fef8fd 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -393,10 +393,6 @@ class lar_solver : public column_namer {
         m_mpq_lar_core_solver.m_r_solver.inf_heap().clear();
     }
 
-    inline void remove_column_from_inf_set(unsigned j) {
-        m_mpq_lar_core_solver.m_r_solver.remove_column_from_inf_heap(j);
-    }
-
     void pivot(int entering, int leaving) {
         m_mpq_lar_core_solver.pivot(entering, leaving);
     }
diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h
index d05d34753..00d079f77 100644
--- a/src/math/lp/lp_core_solver_base.h
+++ b/src/math/lp/lp_core_solver_base.h
@@ -55,7 +55,7 @@ private:
     lp_status m_status;
 public:
     bool current_x_is_feasible() const {
-        TRACE("feas",
+        TRACE("feas_bug",
               if (!m_inf_heap.empty()) {
                   tout << "column " << *m_inf_heap.begin() << " is infeasible" << std::endl;
                   print_column_info(*m_inf_heap.begin(), tout);
@@ -572,13 +572,13 @@ public:
     void insert_column_into_inf_heap(unsigned j) {        
 		if (!m_inf_heap.contains(j)) {
 	        m_inf_heap.insert(j);
-            TRACE("lar_solver", tout << "j = " << j << "\n";);
+            TRACE("lar_solver_inf_heap", tout << "insert into heap j = " << j << "\n";);
         }
         lp_assert(!column_is_feasible(j));
     }
     void remove_column_from_inf_heap(unsigned j) {
 		if (m_inf_heap.contains(j)) {
-            TRACE("lar_solver", tout << "j = " << j << "\n";);
+            TRACE("lar_solver_inf_heap", tout << "insert into heap j = " << j << "\n";);
         	m_inf_heap.erase(j);
         }
         lp_assert(column_is_feasible(j));
diff --git a/src/math/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h
index 2a4a278a6..79e0d7590 100644
--- a/src/math/lp/lp_primal_core_solver.h
+++ b/src/math/lp/lp_primal_core_solver.h
@@ -341,6 +341,7 @@ namespace lp {
     int find_smallest_inf_column() {
         if (this->inf_heap().empty())
             return -1;
+
         return this->inf_heap().min_value();
     }
 
@@ -393,7 +394,10 @@ namespace lp {
         const X &new_val_for_leaving = get_val_for_leaving(leaving);
         X theta = (this->m_x[leaving] - new_val_for_leaving) / a_ent;
         this->m_x[leaving] = new_val_for_leaving;
-        this->remove_column_from_inf_heap(leaving);
+        // this will remove the leaving from the heap
+        TRACE("lar_solver_inf_heap", tout << "leaving = " << leaving
+                                 << " removed from inf_heap()\n";);
+        this->inf_heap().erase_min();
         advance_on_entering_and_leaving_tableau_rows(entering, leaving, theta);
         if (this->current_x_is_feasible())
             this->set_status(lp_status::OPTIMAL);