remove unnecessery call

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

src/math/lp/lar_solver.cpp

@@ -419,7 +419,9 @@ namespace lp {
     void lar_solver::move_non_basic_columns_to_bounds(bool shift_randomly) {
         auto& lcs = m_mpq_lar_core_solver;
         bool change = false;
-        for (unsigned j : lcs.m_r_nbasis) {
+        for (unsigned j : m_columns_with_changed_bounds) {
+            if (lcs.m_r_heading[j] >= 0)
+                continue;
             if (move_non_basic_column_to_bounds(j, shift_randomly))
                 change = true;
         }
@@ -2374,6 +2376,7 @@ namespace lp {
         u_dependency* bdep = lower_bound? ul.lower_bound_witness() : ul.upper_bound_witness();
         SASSERT(bdep != nullptr);
         m_crossed_bounds_deps = m_dependencies.mk_join(bdep, dep);
+        insert_to_columns_with_changed_bounds(j);
     }
 
     void lar_solver::collect_more_rows_for_lp_propagation(){

src/math/lp/lar_solver.h

@@ -140,7 +140,8 @@ class lar_solver : public column_namer {
     bool compare_values(impq const& lhs, lconstraint_kind k, const mpq& rhs);
 
     inline void clear_columns_with_changed_bounds() { m_columns_with_changed_bounds.reset(); }
- public:   
+ public:
+    const auto& columns_with_changed_bounds() const { return m_columns_with_changed_bounds; }
     void insert_to_columns_with_changed_bounds(unsigned j);
     const u_dependency* crossed_bounds_deps() const { return m_crossed_bounds_deps;}
     u_dependency*& crossed_bounds_deps() { return m_crossed_bounds_deps;}

src/math/lp/monomial_bounds.cpp

@@ -268,15 +268,14 @@ namespace nla {
                 c().lra.get_infeasibility_explanation(exp);
                 new_lemma lemma(c(), "propagate fixed - infeasible lra");
                 lemma &= exp;
-                return;
+                break;
             }
             if (c().m_conflicts > 0 ) {
-                return;
+                break;
             }
         }   
     }
 
-
     void monomial_bounds::unit_propagate(monic & m) {
         if (m.is_propagated())
             return;
@@ -288,9 +287,8 @@ namespace nla {
 
         rational k = fixed_var_product(m);
         lpvar w = non_fixed_var(m);
-        if (w == null_lpvar || k == 0) {
+        if (w == null_lpvar || k == 0)
             propagate_fixed(m, k);
-        }
         else
             propagate_nonfixed(m, k, w);
     }
@@ -310,6 +308,7 @@ namespace nla {
             lp::impq val(k);
             c().lra.set_value_for_nbasic_column(m.var(), val);
         }
+        TRACE("nla_solver", tout << "propagate fixed " << m << " = " << k << "\n";);
         c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep);
 
         // propagate fixed equality
@@ -325,6 +324,7 @@ namespace nla {
         lp::lpvar term_index = c().lra.add_term(coeffs, UINT_MAX);
         auto* dep = explain_fixed(m, k);
         term_index = c().lra.map_term_index_to_column_index(term_index);
+        TRACE("nla_solver", tout << "propagate nonfixed " << m << " = " << k << "\n";);
         c().lra.update_column_type_and_bound(term_index, lp::lconstraint_kind::EQ, mpq(0), dep);
 
         if (k == 1) {

src/math/lp/monomial_bounds.h

@@ -39,7 +39,6 @@ namespace nla {
         bool is_linear(monic const& m);
         rational fixed_var_product(monic const& m);
         lpvar non_fixed_var(monic const& m);
-
     public:
         monomial_bounds(core* core);
         void propagate();

src/smt/theory_lra.cpp

@@ -3205,8 +3205,6 @@ class theory_lra::imp {
     lbool make_feasible() {
         TRACE("pcs",  tout << lp().constraints(););
         TRACE("arith_verbose", tout << "before calling lp().find_feasible_solution()\n"; display(tout););
-        // todo: remove later : debug!!!!!
-        lp().move_non_basic_columns_to_bounds(false);
         auto status = lp().find_feasible_solution();
         TRACE("arith_verbose", display(tout););
         if (lp().is_feasible())