patching merge (#6780)

* patching merge

* fix the format and some warnings

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* a fix in the delta calculation

* test patching

* try a new version of get_patching_deltas

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* remove dead code from lp_tst and try optimizing patching

* add comments, replace VERIFY with lp_assert

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* cleanup

---------

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/lp/.clang-format

@@ -0,0 +1,4 @@
+BasedOnStyle: Google
+IndentWidth: 4
+ColumnLimit: 0
+NamespaceIndentation: All

src/math/lp/explanation.h

@@ -49,6 +49,15 @@ public:
         m_set.insert(j);
     }
 
+    void remove(constraint_index j) {
+        m_set.remove(j);
+        unsigned i = 0;
+        for (auto& p : m_vector) 
+            if (p.first != j)
+                m_vector[i++] = p;
+        m_vector.shrink(i);
+    }
+    
     void add_expl(const explanation& e) {
         if (e.m_vector.empty()) {
             for (constraint_index j : e.m_set)

src/math/lp/int_solver.cpp

@@ -2,8 +2,7 @@
   Copyright (c) 2017 Microsoft Corporation
   Author: Lev Nachmanson
 */
-
+// clang-format off
-#include <utility>
 #include "math/lp/int_solver.h"
 #include "math/lp/lar_solver.h"
 #include "math/lp/lp_utils.h"
@@ -17,51 +16,211 @@ namespace lp {
     int_solver::patcher::patcher(int_solver& lia):
         lia(lia),
         lra(lia.lra),
-    lrac(lia.lrac),
+        lrac(lia.lrac)
-    m_num_nbasic_patches(0),
-    m_patch_cost(0),
-    m_next_patch(0),
-    m_delay(0)
     {}
     
-bool int_solver::patcher::should_apply() {
+    void int_solver::patcher::remove_fixed_vars_from_base() {
-#if 1
+        unsigned num = lra.A_r().column_count();
-    return true;
+        for (unsigned v = 0; v < num; v++) {
-#else
+            if (!lia.is_base(v) || !lia.is_fixed(v))
-    if (m_delay == 0) {
+                continue;
-        return true;
+            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;
+                }
+            }        
         }
-    --m_delay;
-    return false;
-#endif
     }
 
-lia_move int_solver::patcher::operator()() {
+
-    return patch_nbasic_columns();
+    unsigned int_solver::patcher::count_non_int() {
+        unsigned non_int = 0;
+        for (auto j : lra.r_basis()) 
+            if (lra.column_is_int(j) && !lra.column_value_is_int(j))
+                ++non_int;
+        return non_int;
+    }
+
+    lia_move int_solver::patcher::patch_basic_columns() {
+        remove_fixed_vars_from_base();
+        lia.settings().stats().m_patches++;
+        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;
+        }
+        return lia_move::undef;
+    }
+
+    // clang-format on
+    /**
+     * \brief find integral and minimal, in the absolute values, deltas such that x - alpha*delta is integral too.
+    */
+    bool get_patching_deltas(const rational& x, const rational& alpha,
+                             rational& delta_0, rational& delta_1) {
+        auto a1 = numerator(alpha);
+        auto a2 = denominator(alpha);
+        auto x1 = numerator(x);
+        auto x2 = denominator(x);
+        if (!divides(x2, a2))
+            return false;
+
+        // delta has to be integral.
+        // We need to find delta such that x1/x2 + (a1/a2)*delta is integral (we are going to flip the delta sign later).
+        // Then a2*x1/x2 + a1*delta is integral, but x2 and x1 are coprime:
+        // that means that t = a2/x2 is
+        // integral. We established that a2 = x2*t Then x1 + a1*delta*(x2/a2)  = x1
+        // + a1*(delta/t)  is integral. Taking into account that t and a1 are
+        // coprime we have delta = t*k, where k is an integer.
+        rational t = a2 / x2;
+        // std::cout << "t = " << t << std::endl;
+        // Now we have x1/x2 + (a1/x2)*k is integral, or (x1 + a1*k)/x2 is integral.
+        // It is equivalent to x1 + a1*k = x2*m, where m is an integer
+        // We know that a2 and a1 are coprime, and x2 divides a2, so x2 and a1 are
+        // coprime. We can find u and v such that u*a1 + v*x2 = 1.
+        rational u, v;
+        gcd(a1, x2, u, v);
+        lp_assert(gcd(a1, x2, u, v).is_one());
+        // std::cout << "u = " << u << ", v = " << v << std::endl;
+        // std::cout << "x= " << (x1 / x2) << std::endl;
+        // std::cout << "x + (a1 / a2) * (-u * t) * x1 = "
+        //           << x + (a1 / a2) * (-u * t) * x1 << std::endl;
+        lp_assert((x + (a1 / a2) * (-u * t) * x1).is_int());
+        // 1 = (u- l*x2 ) * a1 + (v + l*a1)*x2, for every integer l.
+        rational l_low, l_high;
+        auto sign = u.is_pos() ? 1 : -1;
+        auto p = sign * floor(abs(u / x2));
+        auto p_ = p + sign;
+        lp_assert(p * x2 <= u && u <= p_ * x2 || p * x2 >= u && u >= p_ * x2);
+        // std::cout << "u = " << u << ", v = " << v << std::endl;
+        // std::cout << "p = " << p << ", p_ = " << p_ << std::endl;
+        // std::cout << "u - p*x2 = " << u - p * x2 << ", u - p_*x2 = " << u - p_ * x2
+        //           << std::endl;
+        mpq d_0 = (u - p * x2) * t * x1;
+        mpq d_1 = (u - p_ * x2) * t * x1;
+        if (abs(d_0) < abs(d_1)) {
+            delta_0 = d_0;
+            delta_1 = d_1;
+        } else {
+            delta_0 = d_1;
+            delta_1 = d_0;
+        }
+        return true;
+        // std::cout << "delta_0 = " << delta_0 << std::endl;
+        // std::cout << "delta_1 = " << delta_1 << std::endl;
+    }
+    // clang-format off
+    /**
+     * \brief try to patch the basic column v
+     */
+    bool int_solver::patcher::patch_basic_column_on_row_cell(unsigned v, row_cell<mpq> const& c) {
+        if (v == c.var())
+            return false;
+        if (!lra.column_is_int(c.var())) // could use real to patch integer
+            return false;
+        if (c.coeff().is_int())
+            return false;
+        mpq a = fractional_part(c.coeff());
+        mpq r = fractional_part(lra.get_value(v));
+        lp_assert(0 < r && r < 1);
+        lp_assert(0 < a && a < 1);
+        mpq delta_0, delta_1;
+        if (!get_patching_deltas(r, a, delta_0, delta_1))
+            return false;
+        
+        if (try_patch_column(v, c.var(), delta_0))
+            return true;
+
+        if (try_patch_column(v, c.var(), delta_1)) 
+            return true;
+       
+        return false;
+    }
+
+    bool int_solver::patcher::try_patch_column(unsigned v, unsigned j, mpq const& delta) {
+        const auto & A = lra.A_r();
+        if (delta < 0) {
+            if (lia.has_lower(j) && lia.get_value(j) + impq(delta) < lra.get_lower_bound(j))
+                return false;
+        }
+        else {
+            if (lia.has_upper(j) && lia.get_value(j) + impq(delta) > lra.get_upper_bound(j))
+                return false;
+        }
+        for (auto const& c : A.column(j)) {
+            unsigned row_index = c.var();
+            unsigned i = lrac.m_r_basis[row_index];
+            auto old_val = lia.get_value(i);
+            auto new_val = old_val - impq(c.coeff()*delta);
+            if (lia.has_lower(i) && new_val < lra.get_lower_bound(i))
+                return false;
+            if (lia.has_upper(i) && new_val > lra.get_upper_bound(i))
+                return false;
+            if (old_val.is_int() && !new_val.is_int()){
+                return false; // do not waste resources on this case
+            }
+            lp_assert(i != v || new_val.is_int())
+        }
+        
+        lra.set_value_for_nbasic_column(j, lia.get_value(j) + impq(delta));
+         
+        return true;
+    }
+    
+    void int_solver::patcher::patch_basic_column(unsigned v) {
+        SASSERT(!lia.is_fixed(v));
+        for (auto const& c : lra.basic2row(v))
+            if (patch_basic_column_on_row_cell(v, c))
+                return;                                       
     }
 
     lia_move int_solver::patcher::patch_nbasic_columns() {
+        remove_fixed_vars_from_base();
         lia.settings().stats().m_patches++;
         lp_assert(lia.is_feasible());
-    m_num_nbasic_patches = 0;
+        m_patch_success = 0;
-    m_patch_cost = 0;
+        m_patch_fail = 0;
-    for (unsigned j : lia.lrac.m_r_nbasis) {
+        m_num_ones = 0;
-        patch_nbasic_column(j);
+        m_num_divides = 0;
+        //unsigned non_int_before = count_non_int();
+
+        unsigned num = lra.A_r().column_count();
+        for (unsigned v = 0; v < num; v++) {
+            if (lia.is_base(v))
+                continue;
+            patch_nbasic_column(v);
         }
+        unsigned num_fixed = 0;
+        for (unsigned v = 0; v < num; v++) 
+            if (lia.is_fixed(v))
+                ++num_fixed;
+            
         lp_assert(lia.is_feasible());
+        //verbose_stream() << "patch " << m_patch_success << " fails " << m_patch_fail << " ones " << m_num_ones << " divides " << m_num_divides << " num fixed " << num_fixed << "\n";
+        //lra.display(verbose_stream());
+        //exit(0);
+        //unsigned 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++;
-        m_delay = 0;
-        m_next_patch = 0;
             return lia_move::sat;
         }
-    if (m_patch_cost > 0 && m_num_nbasic_patches * 10 < m_patch_cost) {
-        m_delay = std::min(20u, m_next_patch++);
-    }
-    else {
-        m_delay = 0;
-        m_next_patch = 0;
-    }
         return lia_move::undef;
     }
 
@@ -71,17 +230,48 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
     impq l, u;
     mpq m;
     bool has_free = lia.get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m);
-    m_patch_cost += lra.A_r().number_of_non_zeroes_in_column(j);
+    if (!has_free) 
-    if (!has_free) {
         return;
-    }
     bool m_is_one = m.is_one();
     bool val_is_int = lia.value_is_int(j);
 
+#if 0
+const auto & A = lra.A_r();
+#endif
     // check whether value of j is already a multiple of m.
     if (val_is_int && (m_is_one || (val.x / m).is_int())) {
+        if (m_is_one)
+            ++m_num_ones;
+        else
+            ++m_num_divides;
+#if 0
+        for (auto c : A.column(j)) {
+            unsigned row_index = c.var();
+            unsigned i = lrac.m_r_basis[row_index];
+            if (!lia.get_value(i).is_int() ||
+                (lia.has_lower(i) && lia.get_value(i) < lra.get_lower_bound(i)) ||
+                (lia.has_upper(i) && lia.get_value(i) > lra.get_upper_bound(i))) {
+                verbose_stream() << "skip " << j << " " << m << ": ";
+                lia.display_row(verbose_stream(), A.m_rows[row_index]);
+                verbose_stream() << "\n";                    
+            }
+        }
+#endif
         return;
     }
+
+#if 0
+    if (!m_is_one) {
+        // lia.display_column(verbose_stream(), j);
+        for (auto c : A.column(j)) {
+            continue;
+            unsigned row_index = c.var();
+            lia.display_row(verbose_stream(), A.m_rows[row_index]);
+            verbose_stream() << "\n";
+        }
+    }
+#endif
+
     TRACE("patch_int",
           tout << "TARGET j" << j << " -> [";
           if (inf_l) tout << "-oo"; else tout << l;
@@ -89,9 +279,33 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
           if (inf_u) tout << "oo"; else tout << u;
           tout << "]";
           tout << ", m: " << m << ", val: " << val << ", is_int: " << lra.column_is_int(j) << "\n";);
+
+#if 0
+    verbose_stream() << "path " << m << " ";
+    if (!inf_l) verbose_stream() << "infl " << l.x << " ";
+    if (!inf_u) verbose_stream() << "infu " << u.x << " ";
+    verbose_stream() << "\n";
     if (m.is_big() || (!inf_l && l.x.is_big()) || (!inf_u && u.x.is_big())) {
         return;
     }
+#endif
+
+#if 0
+    verbose_stream() << "TARGET v" << j << " -> [";
+    if (inf_l) verbose_stream() << "-oo"; else verbose_stream() << ceil(l.x) << " " << l << "\n";
+    verbose_stream() << ", ";
+    if (inf_u) verbose_stream() << "oo"; else verbose_stream() << floor(u.x) << " " << u << "\n";
+    verbose_stream() << "]";
+    verbose_stream() << ", m: " << m << ", val: " << val << ", is_int: " << lra.column_is_int(j) << "\n";
+#endif
+
+#if 0
+    if (!inf_l)
+        l = impq(ceil(l));
+    if (!inf_u)
+        u = impq(floor(u));
+#endif
+    
     if (!inf_l) {
         l = impq(m_is_one ? ceil(l) : m * ceil(l / m));
         if (inf_u || l <= u) {
@@ -99,8 +313,23 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
             lra.set_value_for_nbasic_column(j, l);
         }
         else {
-            --m_num_nbasic_patches;
+            //verbose_stream() << "fail: " << j << " " << m << "\n";
+            ++m_patch_fail;
             TRACE("patch_int", tout << "not patching " << l << "\n";);
+#if 0
+            verbose_stream() << "not patched\n";
+            for (auto c : A.column(j)) {
+                unsigned row_index = c.var();
+                unsigned i = lrac.m_r_basis[row_index];
+                if (!lia.get_value(i).is_int() ||
+                    (lia.has_lower(i) && lia.get_value(i) < lra.get_lower_bound(i)) ||
+                    (lia.has_upper(i) && lia.get_value(i) > lra.get_upper_bound(i))) {
+                    lia.display_row(verbose_stream(), A.m_rows[row_index]);
+                    verbose_stream() << "\n";                    
+                }
+            }
+#endif
+            return;
         }
     }
     else if (!inf_u) {
@@ -112,7 +341,21 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
         lra.set_value_for_nbasic_column(j, impq(0));
         TRACE("patch_int", tout << "patching with 0\n";);
     }
-    ++m_num_nbasic_patches;
+    ++m_patch_success;
+#if 0
+    verbose_stream() << "patched " << j << "\n";
+    for (auto c : A.column(j)) {
+        unsigned row_index = c.var();
+        unsigned i = lrac.m_r_basis[row_index];
+        if (!lia.get_value(i).is_int() ||
+            (lia.has_lower(i) && lia.get_value(i) < lra.get_lower_bound(i)) ||
+            (lia.has_upper(i) && lia.get_value(i) > lra.get_upper_bound(i))) {
+            lia.display_row(verbose_stream(), A.m_rows[row_index]);
+            verbose_stream() << "\n";                    
+        }
+    }
+#endif
+    
 }
 
 int_solver::int_solver(lar_solver& lar_slv) :
@@ -326,7 +569,7 @@ static void set_upper(impq & u, bool & inf_u, impq const & v) {
 
 // this function assumes that all basic columns dependend on j are feasible
 bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m) {
-    if (lrac.m_r_heading[j] >= 0) // the basic var
+    if (lrac.m_r_heading[j] >= 0 || is_fixed(j)) // basic or fixed var
         return false;
 
     TRACE("random_update", display_column(tout, j) << ", is_int = " << column_is_int(j) << "\n";);
@@ -361,10 +604,9 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
         unsigned i = lrac.m_r_basis[row_index];
         impq const & xi = get_value(i);
         lp_assert(lrac.m_r_solver.column_is_feasible(i));
-        if (column_is_int(i) && !a.is_int())
+        if (column_is_int(i) && !a.is_int() && xi.is_int()) 
             m = lcm(m, denominator(a));
         
-
         if (!inf_l && !inf_u) {
             if (l == u) 
                 continue;            
@@ -372,15 +614,15 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
 
         if (a.is_neg()) {
             if (has_lower(i)) 
-                set_lower(l, inf_l, delta(a, xi, lrac.m_r_lower_bounds()[i]));
+                set_lower(l, inf_l, delta(a, xi, lra.get_lower_bound(i)));
             if (has_upper(i)) 
-                set_upper(u, inf_u, delta(a, xi, lrac.m_r_upper_bounds()[i]));
+                set_upper(u, inf_u, delta(a, xi, lra.get_upper_bound(i)));
         }
         else {
             if (has_upper(i)) 
-                set_lower(l, inf_l, delta(a, xi, lrac.m_r_upper_bounds()[i]));
+                set_lower(l, inf_l, delta(a, xi, lra.get_upper_bound(i)));
             if (has_lower(i)) 
-                set_upper(u, inf_u, delta(a, xi, lrac.m_r_lower_bounds()[i]));
+                set_upper(u, inf_u, delta(a, xi, lra.get_lower_bound(i)));
         }
     }
 
@@ -481,12 +723,9 @@ bool int_solver::at_upper(unsigned j) const {
 std::ostream & int_solver::display_row(std::ostream & out, lp::row_strip<rational> const & row) const {
     bool first = true;
     auto & rslv = lrac.m_r_solver;
-for (const auto &c : row)
+    for (const auto &c : row) {
-    {
+        if (is_fixed(c.var())) {
-        if (is_fixed(c.var()))
+            if (!get_value(c.var()).is_zero()) {
-        {
-            if (!get_value(c.var()).is_zero())
-            {
                 impq val = get_value(c.var()) * c.coeff();
                 if (!first && val.is_pos())
                     out << "+";
@@ -505,17 +744,11 @@ for (const auto &c : row)
         }
         else if (c.coeff().is_minus_one())
             out << "-";
-        else
+        else {
-        {
+            if (c.coeff().is_pos() && !first)
-            if (c.coeff().is_pos())
-            {
-                if (!first)
                 out << "+";
-            }
             if (c.coeff().is_big())
-            {
                 out << " b*";
-            }
             else
                 out << c.coeff();
         }
@@ -523,8 +756,7 @@ for (const auto &c : row)
         first = false;
     }
     out << "\n";
-    for (const auto &c : row)
+    for (const auto &c : row) {
-    {
         if (is_fixed(c.var()))
             continue;
         rslv.print_column_info(c.var(), out);
@@ -533,14 +765,13 @@ for (const auto &c : row)
     }
     return out;
 }
+    
 std::ostream& int_solver::display_row_info(std::ostream & out, unsigned row_index) const  {    
     auto & rslv = lrac.m_r_solver;
     auto const& row = rslv.m_A.m_rows[row_index];
     return display_row(out, row);
 }
 
-
-
 bool int_solver::shift_var(unsigned j, unsigned range) {
     if (is_fixed(j) || is_base(j))
         return false;
@@ -549,11 +780,13 @@ bool int_solver::shift_var(unsigned j, unsigned range) {
     bool inf_l = false, inf_u = false;
     impq l, u;
     mpq m;
-    VERIFY(get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m) || settings().get_cancel_flag());
+    if (!get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m))
+        return false;
     if (settings().get_cancel_flag())
         return false;
     const impq & x = get_value(j);
     // x, the value of j column, might be shifted on a multiple of m
+
     if (inf_l && inf_u) {
         impq new_val = m * impq(random() % (range + 1)) + x;
         lra.set_value_for_nbasic_column(j, new_val);
@@ -570,6 +803,7 @@ bool int_solver::shift_var(unsigned j, unsigned range) {
     if (!inf_l && !inf_u && l >= u)
         return false;
 
+
     if (inf_u) {
         SASSERT(!inf_l);
         impq new_val = x + m * impq(random() % (range + 1));
@@ -640,9 +874,6 @@ int int_solver::select_int_infeasible_var() {
     unsigned n = 0;
     lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
     unsigned prev_usage = 0; // to quiet down the compile
-    unsigned k = 0;
-    unsigned usage;
-    unsigned j;
 
     enum state { small_box, is_small_value,  any_value, not_found };
     state st = not_found;
@@ -650,11 +881,10 @@ int int_solver::select_int_infeasible_var() {
     // 1. small box
     // 2. small value
     // 3. any value
-    for (; k < lra.r_basis().size(); k++) {
+    for (unsigned j : lra.r_basis()) {
-        j = lra.r_basis()[k];
         if (!column_is_int_inf(j))
             continue;
-        usage = lra.usage_in_terms(j);
+        unsigned usage = lra.usage_in_terms(j);
         if (is_boxed(j) && (new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage)) <= small_value) {
             SASSERT(!is_fixed(j));
             if (st != small_box) {
@@ -688,12 +918,12 @@ int int_solver::select_int_infeasible_var() {
             continue;
         SASSERT(st == not_found || st == any_value);
         st = any_value;
-        if (n == 0 /*|| usage > prev_usage*/) {
+        if (n == 0 || usage > prev_usage) {
             result = j;
             prev_usage = usage;
             n = 1;
         } 
-        else if (usage > 0 && /*usage == prev_usage && */ (random() % (++n) == 0)) 
+        else if (usage > 0 && usage == prev_usage && (random() % (++n) == 0)) 
             result = j;
     }
     

src/math/lp/int_solver.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+// clang-format off
 #pragma once
 #include "math/lp/lp_settings.h"
 #include "math/lp/static_matrix.h"
@@ -44,17 +45,23 @@ class int_solver {
         int_solver&         lia;
         lar_solver&         lra;
         lar_core_solver&    lrac;
-        unsigned            m_num_nbasic_patches;
+        unsigned            m_patch_success = 0;
-        unsigned            m_patch_cost;
+        unsigned            m_patch_fail = 0;
-        unsigned            m_next_patch;
+        unsigned            m_num_ones = 0;
-        unsigned            m_delay;
+        unsigned            m_num_divides = 0;
     public:
         patcher(int_solver& lia);
-        bool should_apply();
+        bool should_apply() const { return true; }
-        lia_move operator()();
+        lia_move operator()() { return patch_basic_columns(); }
         void patch_nbasic_column(unsigned j);
+        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:
+        void remove_fixed_vars_from_base();
         lia_move patch_nbasic_columns();
+        lia_move patch_basic_columns();
     };
 
     lar_solver&         lra;

src/math/lp/lar_core_solver.h

@@ -93,6 +93,8 @@ public:
 
     void solve();
 
+    void pivot(int entering, int leaving) { m_r_solver.pivot(entering, leaving); }
+    
     bool lower_bounds_are_set() const { return true; }
 
     const indexed_vector<mpq> & get_pivot_row() const {

src/math/lp/lar_solver.cpp

@@ -2,7 +2,7 @@
   Copyright (c) 2017 Microsoft Corporation
   Author: Nikolaj Bjorner, Lev Nachmanson
 */
-
+// clang-format off
 #include "math/lp/lar_solver.h"
 #include "smt/params/smt_params_helper.hpp"
 
@@ -42,7 +42,6 @@ namespace lp {
             delete t;
     }
     
-    
     bool lar_solver::sizes_are_correct() const {
         lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_column_types.size());
         lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size());
@@ -50,7 +49,6 @@ namespace lp {
         return true;
     }
 
-
     std::ostream& lar_solver::print_implied_bound(const implied_bound& be, std::ostream& out) const {
         out << "implied bound\n";
         unsigned v = be.m_j;
@@ -1354,8 +1352,8 @@ namespace lp {
     }
 
     bool lar_solver::term_is_int(const vector<std::pair<mpq, unsigned int>>& coeffs) const {
-        for (auto const& p : coeffs)
+        for (auto const& [coeff, v] : coeffs)
-            if (!(column_is_int(p.second) && p.first.is_int()))
+            if (!(column_is_int(v) && coeff.is_int()))
                 return false;
         return true;
     }
@@ -1386,7 +1384,7 @@ namespace lp {
     // the lower/upper bound is not strict.
     // the LP obtained by making the bound strict is infeasible
     // -> the column has to be fixed
-    bool lar_solver::is_fixed_at_bound(column_index const& j) {
+    bool lar_solver::is_fixed_at_bound(column_index const& j, vector<std::tuple<explanation, column_index, bool, mpq>>& bounds) {
         if (column_is_fixed(j))
             return false;
         mpq val;
@@ -1395,50 +1393,56 @@ namespace lp {
         lp::lconstraint_kind k;
         if (column_has_upper_bound(j) &&
             get_upper_bound(j).x == val) {
-            verbose_stream() << "check upper " << j << "\n";
             push();   
-            if (column_is_int(j))
+            k = column_is_int(j) ? LE : LT;
-                k = LE, val -= 1;
+            auto ci = mk_var_bound(j, k, column_is_int(j) ? val - 1 : val);
-            else
+            update_column_type_and_bound(j, k, column_is_int(j) ? val - 1 : val, ci);
-                k = LT;
-            auto ci = mk_var_bound(j, k, val);
-            update_column_type_and_bound(j, k, val, ci);
             auto st = find_feasible_solution();
+            bool infeasible = st == lp_status::INFEASIBLE;
+            if (infeasible) {
+                explanation exp;
+                get_infeasibility_explanation(exp);
+                unsigned_vector cis;
+                exp.remove(ci);
+                verbose_stream() << "tight upper bound " << j << " " << val << "\n";
+                bounds.push_back({exp, j, true, val});
+            }
             pop(1);
-            return st == lp_status::INFEASIBLE;            
+            return infeasible;            
         }
         if (column_has_lower_bound(j) &&
             get_lower_bound(j).x == val) {
-            verbose_stream() << "check lower " << j << "\n";
             push();
-            if (column_is_int(j))
+            k = column_is_int(j) ? GE : GT;
-                k = GE, val += 1;
+            auto ci = mk_var_bound(j, k, column_is_int(j) ? val + 1 : val);
-            else
+            update_column_type_and_bound(j, k, column_is_int(j) ? val + 1 : val, ci);
-                k = GT;
-            auto ci = mk_var_bound(j, k, val);
-            update_column_type_and_bound(j, k, val, ci);
             auto st = find_feasible_solution();
+            bool infeasible = st == lp_status::INFEASIBLE;
+            if (infeasible) {
+                explanation exp;
+                get_infeasibility_explanation(exp);
+                exp.remove(ci);
+                verbose_stream() << "tight lower bound " << j << " " << val << "\n";
+                bounds.push_back({exp, j, false, val});
+            }
             pop(1);
-            return st == lp_status::INFEASIBLE;                        
+            return infeasible;
         }
         
         return false;
     }
 
-    bool lar_solver::has_fixed_at_bound() {
+    bool lar_solver::has_fixed_at_bound(vector<std::tuple<explanation, column_index, bool, mpq>>& bounds) {
         verbose_stream() << "has-fixed-at-bound\n";
-        unsigned num_fixed = 0;
         for (unsigned j = 0; j < A_r().m_columns.size(); ++j) {
             auto ci = column_index(j);
-            if (is_fixed_at_bound(ci)) {
+            if (is_fixed_at_bound(ci, bounds)) 
-                ++num_fixed;
                 verbose_stream() << "fixed " << j << "\n";
         }
-        }
+        verbose_stream() << "num fixed " << bounds.size() << "\n";
-        verbose_stream() << "num fixed " << num_fixed << "\n";
+        if (!bounds.empty())
-        if (num_fixed > 0)
             find_feasible_solution();
-        return num_fixed > 0;
+        return !bounds.empty();
     }
 
 
@@ -1617,6 +1621,18 @@ namespace lp {
         return ret;
     }
 
+    /**
+    * \brief ensure there is a column index corresponding to vi
+    * If vi is already a column, just return vi
+    * If vi is for a term, then create a row that uses the term.
+    */
+    var_index lar_solver::ensure_column(var_index vi) {
+        if (lp::tv::is_term(vi))
+            return to_column(vi);
+        else
+            return vi;
+    }
+
 
     void lar_solver::add_row_from_term_no_constraint(const lar_term* term, unsigned term_ext_index) {
         TRACE("dump_terms", print_term(*term, tout) << std::endl;);

src/math/lp/lar_solver.h

@@ -18,29 +18,30 @@
 
   --*/
 #pragma once
-#include "util/vector.h"
+#include <algorithm>
-#include <utility>
+#include <functional>
-#include "util/debug.h"
+#include <stack>
-#include "util/buffer.h"
+#include <string>
 #include <unordered_map>
 #include <unordered_set>
-#include <string>
+#include <utility>
-#include <algorithm>
+
-#include <stack>
+#include "math/lp/bound_analyzer_on_row.h"
-#include <functional>
+#include "math/lp/implied_bound.h"
+#include "math/lp/int_solver.h"
 #include "math/lp/lar_constraints.h"
 #include "math/lp/lar_core_solver.h"
-#include "math/lp/numeric_pair.h"
-#include "math/lp/lp_primal_core_solver.h"
-#include "math/lp/random_updater.h"
-#include "util/stacked_value.h"
-#include "math/lp/stacked_vector.h"
-#include "math/lp/implied_bound.h"
-#include "math/lp/bound_analyzer_on_row.h"
-#include "math/lp/int_solver.h"
-#include "math/lp/nra_solver.h"
-#include "math/lp/lp_types.h"
 #include "math/lp/lp_bound_propagator.h"
+#include "math/lp/lp_primal_core_solver.h"
+#include "math/lp/lp_types.h"
+#include "math/lp/nra_solver.h"
+#include "math/lp/numeric_pair.h"
+#include "math/lp/random_updater.h"
+#include "math/lp/stacked_vector.h"
+#include "util/buffer.h"
+#include "util/debug.h"
+#include "util/stacked_value.h"
+#include "util/vector.h"
 
 namespace lp {
 
@@ -48,10 +49,9 @@ class int_branch;
 class int_solver;
 class lar_solver : public column_namer {
     struct term_hasher {
-        std::size_t operator()(const lar_term &t) const
+        std::size_t operator()(const lar_term& t) const {
-        {            
-            using std::size_t;
             using std::hash;
+            using std::size_t;
             using std::string;
             size_t seed = 0;
             int i = 0;
@@ -66,8 +66,7 @@ class lar_solver : public column_namer {
     };
 
     struct term_comparer {
-        bool operator()(const lar_term &a, const lar_term& b) const
+        bool operator()(const lar_term& a, const lar_term& b) const {
-        {
             return a == b;
         }
     };
@@ -161,12 +160,10 @@ class lar_solver : public column_namer {
     bool sizes_are_correct() const;
     bool implied_bound_is_correctly_explained(implied_bound const& be, const vector<std::pair<mpq, unsigned>>& explanation) const;
 
-
     void substitute_basis_var_in_terms_for_row(unsigned i);
 
     template <typename T>
     unsigned calculate_implied_bounds_for_row(unsigned row_index, lp_bound_propagator<T>& bp) {
-        
         if (A_r().m_rows[row_index].size() > settings().max_row_length_for_bound_propagation || row_has_a_big_num(row_index))
             return 0;
 
@@ -180,7 +177,6 @@ class lar_solver : public column_namer {
 
     static void clean_popped_elements_for_heap(unsigned n, lpvar_heap& set);
     static void clean_popped_elements(unsigned n, u_set& set);
-    
     bool maximize_term_on_tableau(const lar_term& term,
                                   impq& term_max);
     bool costs_are_zeros_for_r_solver() const;
@@ -258,7 +254,6 @@ public:
         return m_fixed_var_table_int;
     }
 
-    
     const map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>>& fixed_var_table_real() const {
         return m_fixed_var_table_real;
     }
@@ -271,7 +266,8 @@ public:
         return is_int ? fixed_var_table_int().find(mpq, j) : fixed_var_table_real().find(mpq, j);
     }
 
-    template <typename T> void remove_non_fixed_from_table(T&);
+    template <typename T>
+    void remove_non_fixed_from_table(T&);
 
     unsigned external_to_column_index(unsigned) const;
 
@@ -368,8 +364,8 @@ public:
                 }
     }
 
-    bool is_fixed_at_bound(column_index const& j);
+    bool is_fixed_at_bound(column_index const& j, vector<std::tuple<explanation, column_index, bool, mpq>>& bounds);
-    bool has_fixed_at_bound();
+    bool has_fixed_at_bound(vector<std::tuple<explanation, column_index, bool, mpq>>& bounds);
 
     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)); }
@@ -378,6 +374,7 @@ public:
     bool compare_values(var_index j, lconstraint_kind kind, const mpq& right_side);
     var_index add_term(const vector<std::pair<mpq, var_index>>& coeffs, unsigned ext_i);
     void register_existing_terms();
+    var_index ensure_column(var_index vi);
     constraint_index add_var_bound(var_index, lconstraint_kind, const mpq&);
     constraint_index add_var_bound_check_on_equal(var_index, lconstraint_kind, const mpq&, var_index&);
 
@@ -385,34 +382,40 @@ public:
     void set_cut_strategy(unsigned cut_frequency);
     inline unsigned column_count() const { return A_r().column_count(); }
     inline var_index local_to_external(var_index idx) const {
-        return tv::is_term(idx)?
+        return tv::is_term(idx) ? m_term_register.local_to_external(idx) : m_var_register.local_to_external(idx);
-            m_term_register.local_to_external(idx) : m_var_register.local_to_external(idx);
+    }
+    bool column_corresponds_to_term(unsigned) const;
+    const lar_term& column_to_term(unsigned j) const {
+        SASSERT(column_corresponds_to_term(j));
+        return get_term(column2tv(to_column_index(j)));
     }
 
-    bool column_corresponds_to_term(unsigned) const;
     inline unsigned row_count() const { return A_r().row_count(); }
     bool var_is_registered(var_index vj) const;
     void clear_inf_heap() {
         m_mpq_lar_core_solver.m_r_solver.inf_heap().clear();
     }
-    inline void remove_column_from_inf_heap(unsigned j) {
+
+    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);
+    }
+
     template <typename ChangeReport>
     void change_basic_columns_dependend_on_a_given_nb_column_report(unsigned j,
                                                                     const numeric_pair<mpq>& delta,
                                                                     const ChangeReport& after) {
-        
         for (const auto& c : A_r().m_columns[j]) {
             unsigned bj = m_mpq_lar_core_solver.m_r_basis[c.var()];
-                if (tableau_with_costs()) {
+            if (tableau_with_costs())
                 m_basic_columns_with_changed_cost.insert(bj);
-                }
             m_mpq_lar_core_solver.m_r_solver.add_delta_to_x_and_track_feasibility(bj, -A_r().get_val(c) * delta);
             after(bj);
             TRACE("change_x_del",
-                      tout << "changed basis column " << bj << ", it is " <<
+                  tout << "changed basis column " << bj << ", it is " << (m_mpq_lar_core_solver.m_r_solver.column_is_feasible(bj) ? "feas" : "inf") << std::endl;);
-                      ( m_mpq_lar_core_solver.m_r_solver.column_is_feasible(bj)?  "feas":"inf") << std::endl;);
         }
     }
 
@@ -420,7 +423,6 @@ public:
     void set_value_for_nbasic_column_report(unsigned j,
                                             const impq& new_val,
                                             const ChangeReport& after) {
-
         lp_assert(!is_base(j));
         auto& x = m_mpq_lar_core_solver.m_r_x[j];
         auto delta = new_val - x;
@@ -465,21 +467,18 @@ public:
         return m_mpq_lar_core_solver.m_r_solver.column_has_lower_bound(j);
     }
 
-    inline
+    inline constraint_index get_column_upper_bound_witness(unsigned j) const {
-    constraint_index get_column_upper_bound_witness(unsigned j) const {
         if (tv::is_term(j)) {
             j = m_var_register.external_to_local(j);
         }
         return m_columns_to_ul_pairs()[j].upper_bound_witness();
     }
 
-    inline
+    inline const impq& get_upper_bound(column_index j) const {
-    const impq& get_upper_bound(column_index j) const {
         return m_mpq_lar_core_solver.m_r_solver.m_upper_bounds[j];
     }
 
-    inline
+    inline const impq& get_lower_bound(column_index j) const {
-    const impq& get_lower_bound(column_index j) const {
         return m_mpq_lar_core_solver.m_r_solver.m_lower_bounds[j];
     }
     bool has_lower_bound(var_index var, constraint_index& ci, mpq& value, bool& is_strict) const;
@@ -586,7 +585,10 @@ public:
     inline void set_int_solver(int_solver* int_slv) { m_int_solver = int_slv; }
     inline int_solver* get_int_solver() { return m_int_solver; }
     inline const int_solver* get_int_solver() const { return m_int_solver; }
-    inline const lar_term & get_term(tv const& t) const { lp_assert(t.is_term()); return *m_terms[t.id()]; }
+    inline const lar_term& get_term(tv const& t) const {
+        lp_assert(t.is_term());
+        return *m_terms[t.id()];
+    }
     lp_status find_feasible_solution();
     void move_non_basic_columns_to_bounds(bool);
     bool move_non_basic_column_to_bounds(unsigned j, bool);
@@ -629,14 +631,12 @@ public:
     bool column_is_int(column_index const& j) const { return column_is_int((unsigned)j); }
     //    const impq& get_ivalue(column_index const& j) const { return get_column_value(j); }
     const impq& get_column_value(column_index const& j) const { return m_mpq_lar_core_solver.m_r_x[j]; }
-    inline
+    inline var_index external_to_local(unsigned j) const {
-    var_index external_to_local(unsigned j) const {
         var_index local_j;
         if (m_var_register.external_is_used(j, local_j) ||
             m_term_register.external_is_used(j, local_j)) {
             return local_j;
-        }
+        } else {
-        else {
             return -1;
         }
     }
@@ -647,6 +647,5 @@ public:
     }
     friend int_solver;
     friend int_branch;
-    
 };
-}
+}  // namespace lp

src/math/lp/lp_bound_propagator.h

@@ -4,20 +4,23 @@
   Nikolaj Bjorner (nbjorner)
   Lev Nachmanson   (levnach)
 */
+//clang-format off
 #pragma once
-#include "math/lp/lp_settings.h"
 #include <utility>
+
+#include "math/lp/lp_settings.h"
+#include "util/uint_set.h"
 namespace lp {
 template <typename T>
 class lp_bound_propagator {
     class edge;  // forward definition
     // vertex represents a column
-    // The set of vertices is organised in a tree.
+    // The set of vertices is organized in a tree.
     // The edges of the tree are rows,
     // Vertices with m_neg set to false grow with the same rate as the root.
     // Vertices with m_neq set to true diminish with the same rate as the roow grows.
     // When two vertices with the same m_neg have the same value of columns
-    // then we have an equality betweet the columns.
+    // then we have an equality between the columns.
     class vertex {
         unsigned m_column;
         vector<edge> m_edges;
@@ -26,10 +29,8 @@ class lp_bound_propagator {
                            // it is handy to find the common ancestor
        public:
         vertex() {}
-        vertex(unsigned column) :
+        vertex(unsigned column) : m_column(column),
-            m_column(column),
+                                  m_level(0) {}
-            m_level(0)
-        {}
         unsigned column() const { return m_column; }
         const vertex* parent() const { return m_edge_from_parent.source(); }
         vertex* parent() { return m_edge_from_parent.source(); }
@@ -58,6 +59,7 @@ class lp_bound_propagator {
         vertex* m_source;
         vertex* m_target;
         int m_row;
+
        public:
         edge(vertex* source, vertex* target, int row) : m_source(source), m_target(target), m_row(row) {}
         edge() : m_source(nullptr), m_target(nullptr), m_row(-1) {}
@@ -69,7 +71,10 @@ class lp_bound_propagator {
         edge reverse() const { return edge(m_target, m_source, m_row); }
     };
 
-    static int other(int x, int y, int z) { SASSERT(x == z || y == z); return x == z ? y : x; }
+    static int other(int x, int y, int z) {
+        SASSERT(x == z || y == z);
+        return x == z ? y : x;
+    }
     std::ostream& print_vert(std::ostream& out, const vertex* v) const {
         out << "(c = " << v->column() << ", parent = {";
         if (v->parent())
@@ -113,8 +118,6 @@ class lp_bound_propagator {
     T& m_imp;
     vector<implied_bound> m_ibounds;
 
-
-
     map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_val2fixed_row;
 
     bool is_fixed_row(unsigned r, unsigned& x) {
@@ -165,7 +168,8 @@ class lp_bound_propagator {
         }
 
         TRACE("cheap_eq",
-              tout << "v_j = "; lp().print_column_info(v_j, tout) << std::endl;
+              tout << "v_j = ";
+              lp().print_column_info(v_j, tout) << std::endl;
               tout << "v = "; print_vert(tout, v) << std::endl;
               tout << "found j " << j << std::endl; lp().print_column_info(j, tout) << std::endl;
               tout << "found j = " << j << std::endl;);
@@ -214,8 +218,7 @@ class lp_bound_propagator {
         if (not_set(y)) {
             set_fixed_vertex(m_root);
             explain_fixed_in_row(row_index, m_fixed_vertex_explanation);
-        }
+        } else {
-        else {            
             vertex* v = add_child_with_check(row_index, y, m_root, polarity);
             if (v)
                 explore_under(v);
@@ -243,19 +246,15 @@ class lp_bound_propagator {
                 if (c.coeff().is_one() || c.coeff().is_minus_one()) {
                     x = c.var();
                     x_cell = &c;
-                }
+                } else
-                else 
                     return false;
-            }
+            } else if (not_set(y)) {
-            else if (not_set(y)) {
                 if (c.coeff().is_one() || c.coeff().is_minus_one()) {
                     y = c.var();
                     y_cell = &c;
-                }
+                } else
-                else
                     return false;
-            }
+            } else
-            else
                 return false;
         }
         if (is_set(x)) {
@@ -302,11 +301,8 @@ class lp_bound_propagator {
         ~reset_cheap_eq() { p.reset_cheap_eq_eh(); }
     };
 
-
    public:
-    
+    lp_bound_propagator(T& imp) : m_imp(imp) {}
-    lp_bound_propagator(T& imp):
-        m_imp(imp) {}
 
     const vector<implied_bound>& ibounds() const { return m_ibounds; }
 
@@ -361,22 +357,19 @@ public:
                     found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict);
                     TRACE("try_add_bound", m_imp.lp().print_implied_bound(found_bound, tout););
                 }
-            }
+            } else {
-            else {
                 m_improved_lower_bounds[j] = m_ibounds.size();
                 m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict));
                 TRACE("try_add_bound", m_imp.lp().print_implied_bound(m_ibounds.back(), tout););
             }
-        }
+        } else {  // the upper bound case
-        else { // the upper bound case
             if (try_get_value(m_improved_upper_bounds, j, k)) {
                 auto& found_bound = m_ibounds[k];
                 if (v < found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && strict)) {
                     found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict);
                     TRACE("try_add_bound", m_imp.lp().print_implied_bound(found_bound, tout););
                 }
-            }
+            } else {
-            else {
                 m_improved_upper_bounds[j] = m_ibounds.size();
                 m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict));
                 TRACE("try_add_bound", m_imp.lp().print_implied_bound(m_ibounds.back(), tout););
@@ -430,10 +423,14 @@ public:
         explain_fixed_in_row(row_index, m_fixed_vertex_explanation);
         set_fixed_vertex(v);
         TRACE("cheap_eq",
-              tout << "polarity switch: " << polarity << "\nv = "; print_vert(tout , v) << "\nu = ";        tout << "fixed vertex explanation\n";
+              tout << "polarity switch: " << polarity << "\nv = ";
-              for (auto p : m_fixed_vertex_explanation) 
+              print_vert(tout, v) << "\nu = "; tout << "fixed vertex explanation\n";
-                  lp().constraints().display(tout, [this](lpvar j) { return lp().get_variable_name(j);}, p.ci()););
+              for (auto p
-
+                   : m_fixed_vertex_explanation)
+                  lp()
+                      .constraints()
+                      .display(
+                          tout, [this](lpvar j) { return lp().get_variable_name(j); }, p.ci()););
     }
 
     bool tree_contains(vertex* v) const {
@@ -449,19 +446,18 @@ public:
         return v;
     }
 
-
     unsigned column(unsigned row, unsigned index) {
         return lp().get_row(row)[index].var();
     }
 
     bool fixed_phase() const { return m_fixed_vertex; }
 
-    
     // Returns the vertex to start exploration from, or nullptr.
     // It is assumed that parent->column() is present in the row
     vertex* get_child_from_row(unsigned row_index, vertex* parent) {
         TRACE("cheap_eq_det", print_row(tout, row_index););
-        unsigned x, y; int row_polarity;
+        unsigned x, y;
+        int row_polarity;
         if (!is_tree_offset_row(row_index, x, y, row_polarity)) {
             TRACE("cheap_eq_det", tout << "not an offset row\n";);
             return nullptr;
@@ -508,12 +504,10 @@ public:
                 is_int(k->column()) == is_int(v->column()) &&
                 !is_equal(k->column(), v->column())) {
                 report_eq(k, v);
-            }
+            } else {
-            else {
                 TRACE("cheap_eq", tout << "no report\n";);
             }
-        }
+        } else {
-        else {
             TRACE("cheap_eq", tout << "registered: " << val(v) << " -> { "; print_vert(tout, v) << "} \n";);
             table.insert(val(v), v);
         }
@@ -557,12 +551,12 @@ public:
         vector<edge> path = connect_in_tree(v_i, v_j);
         lp::explanation exp = get_explanation_from_path(path);
         add_eq_on_columns(exp, v_i->column(), v_j->column(), false);
-        
     }
 
     std::ostream& print_expl(std::ostream& out, const explanation& exp) const {
         for (auto p : exp)
-            lp().constraints().display(out, [this](lpvar j) { return lp().get_variable_name(j);}, p.ci());
+            lp().constraints().display(
+                out, [this](lpvar j) { return lp().get_variable_name(j); }, p.ci());
         return out;
     }
 
@@ -574,8 +568,7 @@ public:
               tout << "reporting eq " << j << ", " << k << "\n";
               tout << "reported idx " << je << ", " << ke << "\n";
               print_expl(tout, exp);
-              tout << "theory_vars v" << lp().local_to_external(je) << " == v" << lp().local_to_external(ke) << "\n";
+              tout << "theory_vars v" << lp().local_to_external(je) << " == v" << lp().local_to_external(ke) << "\n";);
-              );
 
         bool added = m_imp.add_eq(je, ke, exp, is_fixed);
         if (added) {
@@ -693,7 +686,6 @@ public:
             try_add_equation_with_fixed_tables(row_index, e.target());
     }
 
-    
     void cheap_eq_tree(unsigned row_index) {
         reset_cheap_eq _reset(*this);
         TRACE("cheap_eq_det", tout << "row_index = " << row_index << "\n";);
@@ -713,7 +705,8 @@ public:
     }
 
     std::ostream& print_row(std::ostream& out, unsigned row_index) const {
-        unsigned x, y; int polarity;
+        unsigned x, y;
+        int polarity;
         if (true || !is_tree_offset_row(row_index, x, y, polarity))
             return lp().get_int_solver()->display_row_info(out, row_index);
 
@@ -724,8 +717,7 @@ public:
             if (c.coeff().is_one()) {
                 if (!first)
                     out << "+";
-                }
+            } else if (c.coeff().is_minus_one())
-                else if (c.coeff().is_minus_one())
                 out << "-";
             out << lp().get_variable_name(c.var()) << " ";
             first = false;
@@ -764,6 +756,5 @@ public:
         table.insert(j);
         return true;
     }
-
 };
-}
+}  // namespace lp

src/math/lp/lp_primal_core_solver.h

@@ -17,7 +17,7 @@ Revision History:
 
 
 --*/
-
+// clang-format off
 #pragma once
 #include "math/lp/core_solver_pretty_printer.h"
 #include "math/lp/lp_core_solver_base.h"
@@ -98,22 +98,12 @@ public:
             case column_type::fixed:
                 return false;
             case column_type::lower_bound:
-      if (is_pos(rc.coeff())) {
+                return !is_pos(rc.coeff()) || this->x_above_lower_bound(j);
-        return this->x_above_lower_bound(j);
-      }
-
-      return true;
             case column_type::upper_bound:
-      if (is_pos(rc.coeff())) {
+                return is_pos(rc.coeff()) || this->x_below_upper_bound(j);
-        return true;
-      }
-
-      return this->x_below_upper_bound(j);
             case column_type::boxed:
-      if (is_pos(rc.coeff())) {
+                if (is_pos(rc.coeff())) 
                     return this->x_above_lower_bound(j);
-      }
-
                 return this->x_below_upper_bound(j);
             default:
                 return false;
@@ -131,22 +121,16 @@ public:
             case column_type::fixed:
                 return false;
             case column_type::lower_bound:
-      if (is_neg(rc.coeff())) {
+                if (is_neg(rc.coeff())) 
                     return this->x_above_lower_bound(j);
-      }
-
                 return true;
             case column_type::upper_bound:
-      if (is_neg(rc.coeff())) {
+                if (is_neg(rc.coeff())) 
                     return true;
-      }
-
                 return this->x_below_upper_bound(j);
             case column_type::boxed:
-      if (is_neg(rc.coeff())) {
+                if (is_neg(rc.coeff())) 
                     return this->x_above_lower_bound(j);
-      }
-
                 return this->x_below_upper_bound(j);
             default:
                 return false;
@@ -154,6 +138,7 @@ public:
             UNREACHABLE(); // unreachable
             return false;
         }
+
 /**
  * Return the number of base non-free variables depending on the column j,
  * different from bj,
@@ -174,7 +159,7 @@ public:
     }
     return r;
   }
-
+    // clang-format on
     int find_beneficial_entering_in_row_tableau_rows_bland_mode(int i, T &a_ent) {
         int j = -1;
         unsigned bj = this->m_basis[i];
@@ -194,13 +179,11 @@ public:
                 a_ent = rc.coeff();
             }
         }
-    if (j == -1) {
+        if (j == -1)
             m_inf_row_index_for_tableau = i;
-    }
-
         return j;
     }
-
+    //clang-format off
     int find_beneficial_entering_tableau_rows(int i, T &a_ent) {
         if (m_bland_mode_tableau)
             return find_beneficial_entering_in_row_tableau_rows_bland_mode(i, a_ent);
@@ -248,54 +231,48 @@ public:
         return rc.var();
     }
 
-  bool try_jump_to_another_bound_on_entering(unsigned entering, const X &theta,
+    bool try_jump_to_another_bound_on_entering(unsigned entering, const X &theta, X &t, bool &unlimited);
-                                             X &t, bool &unlimited);
+
     bool try_jump_to_another_bound_on_entering_unlimited(unsigned entering, X &t);
+
     int find_leaving_and_t_tableau(unsigned entering, X &t);
 
     void limit_theta(const X &lim, X &theta, bool &unlimited) {
         if (unlimited) {
             theta = lim;
             unlimited = false;
-    } else {
+        } else
             theta = std::min(lim, theta);
     }
-  }
 
     void limit_theta_on_basis_column_for_inf_case_m_neg_upper_bound(
         unsigned j, const T &m, X &theta, bool &unlimited) {
         lp_assert(m < 0 && this->m_column_types[j] == column_type::upper_bound);
-    limit_inf_on_upper_bound_m_neg(m, this->m_x[j], this->m_upper_bounds[j],
+        limit_inf_on_upper_bound_m_neg(m, this->m_x[j], this->m_upper_bounds[j], theta, unlimited);
-                                   theta, unlimited);
     }
 
     void limit_theta_on_basis_column_for_inf_case_m_neg_lower_bound(
         unsigned j, const T &m, X &theta, bool &unlimited) {
         lp_assert(m < 0 && this->m_column_types[j] == column_type::lower_bound);
-    limit_inf_on_bound_m_neg(m, this->m_x[j], this->m_lower_bounds[j], theta,
+        limit_inf_on_bound_m_neg(m, this->m_x[j], this->m_lower_bounds[j], theta, unlimited);
-                             unlimited);
     }
 
     void limit_theta_on_basis_column_for_inf_case_m_pos_lower_bound(
         unsigned j, const T &m, X &theta, bool &unlimited) {
         lp_assert(m > 0 && this->m_column_types[j] == column_type::lower_bound);
-    limit_inf_on_lower_bound_m_pos(m, this->m_x[j], this->m_lower_bounds[j],
+        limit_inf_on_lower_bound_m_pos(m, this->m_x[j], this->m_lower_bounds[j], theta, unlimited);
-                                   theta, unlimited);
     }
 
     void limit_theta_on_basis_column_for_inf_case_m_pos_upper_bound(
         unsigned j, const T &m, X &theta, bool &unlimited) {
         lp_assert(m > 0 && this->m_column_types[j] == column_type::upper_bound);
-    limit_inf_on_bound_m_pos(m, this->m_x[j], this->m_upper_bounds[j], theta,
+        limit_inf_on_bound_m_pos(m, this->m_x[j], this->m_upper_bounds[j], theta, unlimited);
-                             unlimited);
     };
 
     void get_bound_on_variable_and_update_leaving_precisely(
         unsigned j, vector<unsigned> &leavings, T m, X &t,
         T &abs_of_d_of_leaving);
 
- 
-
 #ifdef Z3DEBUG
     void check_Ax_equal_b();
     void check_the_bounds();
@@ -303,12 +280,16 @@ public:
     void check_correctness();
 #endif
 
-
     void backup_and_normalize_costs();
 
     void advance_on_entering_and_leaving_tableau(int entering, int leaving, X &t);
     void advance_on_entering_equal_leaving_tableau(int entering, X &t);
 
+    void pivot(int entering, int leaving) {
+        this->pivot_column_tableau(entering, this->m_basis_heading[leaving]);
+        this->change_basis(entering, leaving);
+    }
+
     bool need_to_switch_costs() const {
         if (this->m_settings.simplex_strategy() ==
             simplex_strategy_enum::tableau_rows)
@@ -338,13 +319,11 @@ public:
     void update_x_tableau_rows(unsigned entering, unsigned leaving,
                                const X &delta) {
         this->add_delta_to_x(entering, delta);
-    for (const auto &c : this->m_A.m_columns[entering]) {
+        for (const auto &c : this->m_A.m_columns[entering])
-       if (leaving != this->m_basis[c.var()]) {
+            if (leaving != this->m_basis[c.var()])
                 this->add_delta_to_x_and_track_feasibility(
                     this->m_basis[c.var()], -delta * this->m_A.get_val(c));
     }
-    }    
-  }
 
     void update_basis_and_x_tableau_rows(int entering, int leaving, X const &tt) {
         lp_assert(entering != leaving);
@@ -365,8 +344,6 @@ public:
         return this->inf_heap().min_value();
     }
 
-  
-
     const X &get_val_for_leaving(unsigned j) const {
         lp_assert(!this->column_is_feasible(j));
         switch (this->m_column_types[j]) {

src/math/lp/lp_primal_core_solver_tableau_def.h

@@ -59,6 +59,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_e
     }
     unsigned j_nz = this->m_m() + 1; // this number is greater than the max column size
     std::list<unsigned>::iterator entering_iter = m_non_basis_list.end();
+    unsigned n = 0;
     for (auto non_basis_iter = m_non_basis_list.begin(); number_of_benefitial_columns_to_go_over && non_basis_iter != m_non_basis_list.end(); ++non_basis_iter) {
         unsigned j = *non_basis_iter;
         if (!column_is_benefitial_for_entering_basis(j))
@@ -71,8 +72,9 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_e
             entering_iter = non_basis_iter;
             if (number_of_benefitial_columns_to_go_over)
                 number_of_benefitial_columns_to_go_over--;
+            n = 1;
         }
-        else if (t == j_nz && this->m_settings.random_next() % 2 == 0) {
+        else if (t == j_nz && this->m_settings.random_next(++n) == 0) {
             entering_iter = non_basis_iter;
         }
     }// while (number_of_benefitial_columns_to_go_over && initial_offset_in_non_basis != offset_in_nb);
@@ -166,7 +168,8 @@ template <typename T, typename X>void lp_primal_core_solver<T, X>::advance_on_en
         }
         this->update_basis_and_x_tableau(entering, leaving, t);
         this->iters_with_no_cost_growing() = 0;
-    } else {
+    }
+    else {
         this->pivot_column_tableau(entering, this->m_basis_heading[leaving]);
         this->change_basis(entering, leaving);
     }

src/math/lp/lp_types.h

@@ -20,8 +20,9 @@ Revision History:
 #pragma once
 
 #include <sstream>
-
+// clang-format off
-
+#include <limits.h>
+#include "util/debug.h"
 namespace nla {
     class core;
 }

src/test/lp/.clang-format

@@ -0,0 +1,3 @@
+BasedOnStyle: Google
+IndentWidth: 4
+ColumnLimit: 0