From 0fbf8f92f51ce7f1df8027e4771b4757bbf0bbed Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Sat, 5 Aug 2023 09:31:55 -1000
Subject: [PATCH] delete remove_fixed_vars_from_base() from int_solver

---
 src/math/lp/int_solver.cpp | 29 +----------------------------
 src/math/lp/int_solver.h   |  3 +--
 src/math/lp/lar_solver.h   |  3 ++-
 3 files changed, 4 insertions(+), 31 deletions(-)

diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index b4d703218..e03aa785e 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -18,22 +18,6 @@ namespace lp {
         lrac(lia.lrac)
     {}
     
-    void int_solver::patcher::remove_fixed_vars_from_base() {
-        unsigned num = lra.A_r().column_count();
-        for (unsigned v = 0; v < num; v++) {
-            if (!lia.is_base(v) || !lia.is_fixed(v))
-                continue;
-            auto const & r = lra.basic2row(v);
-            for (auto const& c : r) {
-                if (c.var() != v && !lia.is_fixed(c.var())) {
-                    lra.pivot(c.var(), v); 
-                    break;
-                }
-            }        
-        }
-    }
-
-
     unsigned int_solver::patcher::count_non_int() {
         unsigned non_int = 0;
         for (auto j : lra.r_basis()) 
@@ -43,22 +27,12 @@ namespace lp {
     }
 
     lia_move int_solver::patcher::patch_basic_columns() {
-        remove_fixed_vars_from_base();
         lia.settings().stats().m_patches++;
+        lra.remove_fixed_vars_from_base();
         lp_assert(lia.is_feasible());
-        
-       // unsigned non_int_before, non_int_after;
-
-       // non_int_before = count_non_int();
-
-
-        // unsigned num = lra.A_r().column_count();
         for (unsigned j : lra.r_basis()) 
             if (!lra.get_value(j).is_int())
                 patch_basic_column(j);
-        // non_int_after = count_non_int();
-        // verbose_stream() << non_int_before << " -> " << non_int_after << "\n";
-
         if (!lia.has_inf_int()) {
             lia.settings().stats().m_patches_success++;
             return lia_move::sat;
@@ -177,7 +151,6 @@ namespace lp {
     }
 
 
-
 int_solver::int_solver(lar_solver& lar_slv) :
     lra(lar_slv),
     lrac(lra.m_mpq_lar_core_solver),
diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h
index 56237a5b8..c6b1bb1d0 100644
--- a/src/math/lp/int_solver.h
+++ b/src/math/lp/int_solver.h
@@ -52,13 +52,12 @@ class int_solver {
         patcher(int_solver& lia);
         bool should_apply() const { return true; }
         lia_move operator()() { return patch_basic_columns(); }
-        bool patch_basic_column_on_row_cell(unsigned v, row_cell<mpq> const& c);
         void patch_basic_column(unsigned j);
         bool try_patch_column(unsigned v, unsigned j, mpq const& delta);
         unsigned count_non_int();
     private:
+        bool patch_basic_column_on_row_cell(unsigned v, row_cell<mpq> const& c);
         lia_move patch_basic_columns();
-        void remove_fixed_vars_from_base();
     };
 
     lar_solver&         lra;
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index a4a0e87b0..ab61a32e9 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -333,8 +333,9 @@ class lar_solver : public column_namer {
     void add_column_rows_to_touched_rows(lpvar j);
     template <typename T>
     void propagate_bounds_for_touched_rows(lp_bound_propagator<T>& bp) {
-        remove_fixed_vars_from_base();
         if (settings().propagate_eqs()) {
+            if (settings().random_next() % 10 == 0) 
+                remove_fixed_vars_from_base();
             bp.clear_for_eq();
             for (unsigned i : m_touched_rows) {
                 unsigned offset_eqs = stats().m_offset_eqs;