cautious remove_basis

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

src/math/lp/lar_solver.cpp

@@ -565,6 +565,40 @@ bool lar_solver::remove_from_basis(unsigned j) {
     return m_mpq_lar_core_solver.m_r_solver.remove_from_basis(j);
 }
 
+// val is the new value to be assigned to x[j]
+// return true iff can find a new basic column that would be feasible
+// after the pivoting
+bool lar_solver::remove_from_basis(unsigned basic_j, const mpq& val) {
+    SASSERT(is_base(basic_j));
+    impq del(0);
+    const auto& slv = m_mpq_lar_core_solver.m_r_solver;
+    bool grow = val < get_column_value(basic_j).x; // grow = true means that the monomial of the pivoted var has to grow
+    for (auto &c : A_r().m_rows[row_of_basic_column(basic_j)]) {
+        lpvar j = c.var();
+        if (j == basic_j) {
+            SASSERT(c.coeff().is_one());
+            continue;
+        }
+
+        bool can_pivot = column_is_free(j);
+        if (!can_pivot &&
+            ((grow && slv.monoid_can_increase(c))|| (!grow && slv.monoid_can_decrease(c)))) {            
+            if (del.is_zero())
+                del = impq(val) - get_column_value(basic_j);
+            
+            impq j_val = get_column_value(j) - del / c.coeff();
+            if (inside_bounds(j, j_val))
+                can_pivot = true;
+        }
+        
+        if (can_pivot) {
+            pivot_column_tableau(c.var(), row_of_basic_column(basic_j));
+            return true;
+        }
+    }            
+    return false;    
+}
+
 lar_term lar_solver::get_term_to_maximize(unsigned j_or_term) const {
     if (tv::is_term(j_or_term)) {
         return get_term(j_or_term);

src/math/lp/lar_solver.h

@@ -260,6 +260,7 @@ class lar_solver : public column_namer {
     void update_delta_for_terms(const impq & delta, unsigned j, const vector<unsigned>&);
     void fill_vars_to_terms(vector<vector<unsigned>> & vars_to_terms);
     bool remove_from_basis(unsigned);
+    bool remove_from_basis(unsigned, const mpq&);
     lar_term get_term_to_maximize(unsigned ext_j) const;
     bool sum_first_coords(const lar_term& t, mpq & val) const;
     void collect_rounded_rows_to_fix();
@@ -361,7 +362,7 @@ public:
                       const ChangeReport& change_report) {
         if (is_base(j)) {
             TRACE("nla_solver", get_int_solver()->display_row_info(tout, row_of_basic_column(j)) << "\n";);
-            remove_from_basis(j);
+            remove_from_basis(j, val);
         }
 
         impq ival(val);

src/math/lp/lp_core_solver_base.cpp

@@ -145,5 +145,6 @@ template bool lp::lp_core_solver_base<lp::mpq, lp::mpq >::infeasibility_costs_ar
 template bool lp::lp_core_solver_base<double, double >::infeasibility_costs_are_correct() const;
 template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::calculate_pivot_row(unsigned int);
 template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::remove_from_basis(unsigned int);
+template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::remove_from_basis(unsigned int, lp::numeric_pair<lp::mpq> const&);
 template void lp::lp_core_solver_base<rational, rational>::solve_Bd(unsigned int, lp::indexed_vector<rational>&, lp::indexed_vector<rational>&) const;
 template void lp::lp_core_solver_base<rational, lp::numeric_pair<rational> >::solve_Bd(unsigned int, lp::indexed_vector<rational>&, lp::indexed_vector<rational>&) const;

src/math/lp/lp_core_solver_base.h

@@ -459,6 +459,7 @@ public:
     int pivots_in_column_and_row_are_different(int entering, int leaving) const;
     void pivot_fixed_vars_from_basis();
     bool remove_from_basis(unsigned j);
+    bool remove_from_basis(unsigned j, const impq&);
     bool pivot_column_general(unsigned j, unsigned j_basic, indexed_vector<T> & w);
     void init_basic_part_of_basis_heading() {
         unsigned m = m_basis.size();

src/math/lp/lp_core_solver_base_def.h

@@ -981,6 +981,18 @@ template <typename T, typename X> bool lp_core_solver_base<T, X>::remove_from_ba
     return false;
 }
 
+template <typename T, typename X> bool lp_core_solver_base<T, X>::remove_from_basis(unsigned basic_j, const impq& val) {
+    indexed_vector<T> w(m_basis.size()); // the buffer
+    unsigned i = m_basis_heading[basic_j];
+    for (auto &c : m_A.m_rows[i]) {
+        if (c.var() == basic_j)
+            continue;
+        if (pivot_column_general(c.var(), basic_j, w))
+            return true;
+    }
+    return false;
+}
+
 
 template <typename T, typename X> bool 
 lp_core_solver_base<T, X>::infeasibility_costs_are_correct() const {