do not delay update for the polar case

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Z3Prover · Jan 11, 2024 · 2b974a0 · 2b974a0
1 parent 2ac866a
commit 2b974a0
Showing 1 changed file with 7 additions and 16 deletions.
diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
@@ -400,8 +400,6 @@ struct create_cut {
     lia_move gomory::get_gomory_cuts(unsigned num_cuts) {
         struct cut_result {u_dependency *dep; lar_term t; mpq k; int polarity; lpvar j;};
         vector<cut_result> big_cuts;
-        struct polar_info {lpvar j; int polarity;  u_dependency *dep;};
-        vector<polar_info> polar_vars;
         unsigned_vector columns_for_cuts = gomory_select_int_infeasible_vars(num_cuts);
         bool has_small_cut = false;
 
@@ -437,10 +435,14 @@ struct create_cut {
                     return lia_move::conflict;
                 continue;
             }
+
+            if (cc.m_polarity == 1) 
+                lra.update_column_type_and_bound(j, lp::lconstraint_kind::LE, floor(lra.get_column_value(j).x), cc.m_dep);
+            else if (cc.m_polarity == -1)
+                lra.update_column_type_and_bound(j, lp::lconstraint_kind::GE, ceil(lra.get_column_value(j).x), cc.m_dep);
+
+
             cut_result cr = {cc.m_dep, lia.m_t, lia.m_k, cc.m_polarity, j};
-            if (abs(cr.polarity) == 1)  // need to delay the update of the bounds for j in a polar case, because simplify_inequality relies on the old bounds
-                polar_vars.push_back( {j, cr.polarity,  cc.m_dep} ); 
-
             if (!is_small_cut(lia.m_t)) {
                 big_cuts.push_back(cr);
                 continue;
@@ -463,17 +465,6 @@ struct create_cut {
                     add_cut(cut);
 
         }
-
-// this way we create bounds for the variables in polar cases even where the terms have big numbers
-        for (auto const& p : polar_vars) {
-            if (p.polarity == 1) {
-                lra.update_column_type_and_bound(p.j, lp::lconstraint_kind::LE, floor(lra.get_column_value(p.j).x), p.dep);
-            }
-            else {
-                SASSERT(p.polarity == -1);
-                lra.update_column_type_and_bound(p.j, lp::lconstraint_kind::GE, ceil(lra.get_column_value(p.j).x), p.dep);
-            }
-        }
 
         if (!_check_feasible())
             return lia_move::conflict;