From f7f9c15676de2c18dfa538db3166836bca0ca0d4 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 15 Jun 2020 16:08:53 -0700
Subject: [PATCH] cheap_eqs tree

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/bound_analyzer_on_row.h | 18 +-----------------
 src/math/lp/lar_solver.h            | 20 ++++++++++++++++++++
 src/math/lp/lp_bound_propagator.h   | 10 +++++++---
 3 files changed, 28 insertions(+), 20 deletions(-)

diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h
index 38ea9e10b..6084145c2 100644
--- a/src/math/lp/bound_analyzer_on_row.h
+++ b/src/math/lp/bound_analyzer_on_row.h
@@ -61,7 +61,6 @@ public :
                             B & bp) {
         bound_analyzer_on_row a(row, bj, rs, row_or_term_index, bp);
         a.analyze();
-        a.analyze_eq();
     }
 
 private:
@@ -327,22 +326,7 @@ private:
         default:
             break;
         }
-    }
-
-    void analyze_eq() {
-        switch (m_bp.lp().settings().cheap_eqs()) {
-        case 0:
-            return;
-        case 1:
-            m_bp.cheap_eq_tree(m_row_index);
-            break;
-        case 2:
-            m_bp.cheap_eq_table(m_row_index);
-            break;
-        default:
-            return;
-        }
-    }
+    }   
 };
 }
 
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 05d828c43..9dc04df11 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -342,8 +342,28 @@ public:
             if (settings().get_cancel_flag())
                 return;
         }
+        // these two loops should be run sequentially
+        // since the first loop might change column bounds
+        // and add fixed columns this way
+        bp.clear_for_eq();
+        if (settings().cheap_eqs()) {
+            for (unsigned i : m_rows_with_changed_bounds) {
+                calculate_cheap_eqs_for_row(i, bp);
+                if (settings().get_cancel_flag())
+                    return;
+            }
+        }
         m_rows_with_changed_bounds.clear();
     }
+    template <typename T>
+    void calculate_cheap_eqs_for_row(unsigned i, lp_bound_propagator<T> & bp) {
+        if (settings().cheap_eqs() == 1) {
+            bp.cheap_eq_tree(i);
+        } else {
+            bp.cheap_eq_table(i);
+        }
+    }
+    
     bool is_fixed(column_index const& j) const { return column_is_fixed(j); }
     inline column_index to_column_index(unsigned v) const { return column_index(external_to_column_index(v)); }
     bool external_is_used(unsigned) const;
diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index bd13a6bf1..2d25830f6 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -501,8 +501,10 @@ public:
         clear_for_eq();
         unsigned x_index, y_index;
         mpq offset;
-        if (!is_offset_row_wrong(row_index, x_index, y_index, offset))
+        if (!is_offset_row_wrong(row_index, x_index, y_index, offset)) {
+            m_visited_rows.insert(row_index);
             return;
+        }
         TRACE("cheap_eq", lp().get_int_solver()->display_row_info(tout, row_index););
         m_root = alloc(vertex, row_index, x_index, mpq(0));
         vertex* v_y = alloc(vertex, row_index, y_index, offset);
@@ -541,11 +543,13 @@ public:
             unsigned row_index = c.var();
             if (m_visited_rows.contains(row_index))
                 continue;
-            m_visited_rows.insert(row_index);
             unsigned x_index, y_index;
             mpq row_offset;
-            if (!is_offset_row_wrong(row_index, x_index, y_index, row_offset))
+            if (!is_offset_row_wrong(row_index, x_index, y_index, row_offset)) {
+                m_visited_rows.insert(row_index);
                 continue;
+            }
+            m_visited_rows.insert(row_index);
             TRACE("cheap_eq", lp().get_int_solver()->display_row_info(tout, row_index););
             // who is it the same column?
             if (lp().get_row(row_index)[x_index].var() == j) { // conected to x