solve all smt2 from QF_LIA/calypto with int_solver

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

src/util/lp/int_solver.cpp

@@ -8,15 +8,21 @@
 namespace lean {
 
 void int_solver::fix_non_base_columns() {
+	lean_assert(is_feasible() && inf_int_set_is_correct());
     auto & lcs = m_lar_solver->m_mpq_lar_core_solver;
+    bool change = false;
     for (unsigned j : lcs.m_r_nbasis) {
         if (column_is_int_inf(j)) {
+            change = true;
             set_value_for_nbasic_column(j, floor(lcs.m_r_x[j].x));
         }
     }
+    if (!change)
+        return;
     if (m_lar_solver->find_feasible_solution() == INFEASIBLE)
         failed();
-	lean_assert(is_feasible() && inf_int_set_is_correct());
+    init_inf_int_set();
+    lean_assert(is_feasible() && inf_int_set_is_correct());
 }
 
 void int_solver::failed() {
@@ -390,8 +396,9 @@ void int_solver::set_value_for_nbasic_column(unsigned j, const impq & new_val) {
     auto delta = new_val - x;
     x = new_val;
     m_lar_solver->change_basic_x_by_delta_on_column(j, delta);
-    update_column_in_int_inf_set(j);
+
 	auto * it = get_column_iterator(j);
+    update_column_in_int_inf_set(j);
 	unsigned i;
 	while (it->next(i))
 		update_column_in_int_inf_set(m_lar_solver->m_mpq_lar_core_solver.m_r_basis[i]);
@@ -711,7 +718,7 @@ bool int_solver::get_freedom_interval_for_column(unsigned x_j, bool & inf_l, imp
         else {
             if (x_i_upper) {
                 impq new_l = x_j_val + ((x_i_val - lcs.m_r_upper_bounds()[x_i]) / a_ij);
-                set_lower(l, inf_u, new_l);
+                set_lower(l, inf_l, new_l);
                 if (!inf_l && !inf_u && l == u) break;;                
             }
             if (x_i_lower) {
@@ -730,7 +737,11 @@ bool int_solver::get_freedom_interval_for_column(unsigned x_j, bool & inf_l, imp
           if (inf_l) tout << "-oo"; else tout << l;
           tout << "; ";
           if (inf_u) tout << "oo";  else tout << u;
-          tout << "]\n";);
+          tout << "]\n";
+          tout << "val = " << get_value(x_j) << "\n";
+          );
+    lean_assert(inf_l || l <= get_value(x_j));
+    lean_assert(inf_u || u >= get_value(x_j));
     return true;
 
 }

src/util/lp/lar_core_solver.hpp

@@ -145,23 +145,7 @@ int lar_core_solver::column_is_out_of_bounds(unsigned j) {
 
 
 void lar_core_solver::calculate_pivot_row(unsigned i) {
-    lean_assert(!m_r_solver.use_tableau());
+    m_r_solver.calculate_pivot_row(i);
-    lean_assert(m_r_solver.m_pivot_row.is_OK());
-    m_r_solver.m_pivot_row_of_B_1.clear();
-    m_r_solver.m_pivot_row_of_B_1.resize(m_r_solver.m_m());
-    m_r_solver.m_pivot_row.clear();
-    m_r_solver.m_pivot_row.resize(m_r_solver.m_n());
-    if (m_r_solver.m_settings.use_tableau()) {
-        unsigned basis_j = m_r_solver.m_basis[i];
-        for (auto & c : m_r_solver.m_A.m_rows[i]) {
-            if (c.m_j != basis_j)
-                m_r_solver.m_pivot_row.set_value(c.get_val(), c.m_j);
-        }
-        return;
-    }
-
-    m_r_solver.calculate_pivot_row_of_B_1(i);
-    m_r_solver.calculate_pivot_row_when_pivot_row_of_B1_is_ready(i);
 }
 
 

src/util/lp/lar_solver.cpp

@@ -648,6 +648,10 @@ void lar_solver::change_basic_x_by_delta_on_column(unsigned j, const numeric_pai
                 m_basic_columns_with_changed_cost.insert(bj);
             }
             m_mpq_lar_core_solver.m_r_solver.update_column_in_inf_set(bj);
+            TRACE("change_x_del",
+                  tout << "changed basis column " << bj << ", it is " <<
+                  ( m_mpq_lar_core_solver.m_r_solver.column_is_feasible(bj)?  "feas":"inf") << std::endl;);
+                  
         }
     } else {
         m_column_buffer.clear();

src/util/lp/lp_core_solver_base.h

@@ -13,6 +13,9 @@
 #include "util/lp/lu.h"
 #include "util/lp/permutation_matrix.h"
 #include "util/lp/column_namer.h"
+#include "util/lp/iterator_on_row.h"
+#include "util/lp/iterator_on_pivot_row.h"
+
 namespace lean {
 
 template <typename T, typename X> // X represents the type of the x variable and the bounds
@@ -688,5 +691,14 @@ public:
     const unsigned & iters_with_no_cost_growing() const {
         return m_iters_with_no_cost_growing;
     }
+
+    linear_combination_iterator<T> * get_iterator_on_row(unsigned i) {
+        if (m_settings.use_tableau())
+            return new iterator_on_row<T>(m_A.m_rows[i]);
+        calculate_pivot_row(i);
+        return new iterator_on_pivot_row<T>(m_pivot_row, m_basis[i]);
+    }
+
+    void calculate_pivot_row(unsigned i);
 };
 }

src/util/lp/lp_core_solver_base.hpp

@@ -956,26 +956,23 @@ template <typename T, typename X>  void lp_core_solver_base<T, X>::pivot_fixed_v
     // run over basis and non-basis at the same time
     indexed_vector<T> w(m_basis.size()); // the buffer
     unsigned i = 0; // points to basis
-    unsigned j = 0; // points to nonbasis
+    for (; i < m_basis.size(); i++) {
-    
+        unsigned basic_j = m_basis[i];
-    for (; i < m_basis.size() && j < m_nbasis.size(); i++) {
-        unsigned ii = m_basis[i];
-        unsigned jj;
 
-        if (get_column_type(ii) != column_type::fixed) continue;
+        if (get_column_type(basic_j) != column_type::fixed) continue;
-		//todo run over the row here!!!!!
+		//todo run over the row here!!!!! call get_iterator_on_row();
-        while (j < m_nbasis.size()) {
+        T a;
-            for (; j < m_nbasis.size(); j++) {
+        unsigned j;
-                jj = m_nbasis[j];
+        auto * it = get_iterator_on_row(i);
-                if (get_column_type(jj) != column_type::fixed)
+        while (it->next(a, j)) {
+            if (j == basic_j)
+                continue;
+            if (get_column_type(j) != column_type::fixed) {
+                if (pivot_column_general(j, basic_j, w))
                     break;
             }
-            if (j >= m_nbasis.size())
+        }
-                break;
+        delete it;
-            j++;
-			if (pivot_column_general(jj, ii, w))
-				break;
-        } 
     }
 }
 
@@ -1033,4 +1030,26 @@ lp_core_solver_base<T, X>::infeasibility_cost_is_correct_for_column(unsigned j)
     }
 }
 
+template <typename T, typename X>
+void lp_core_solver_base<T, X>::calculate_pivot_row(unsigned i) {
+    lean_assert(!use_tableau());
+    lean_assert(m_pivot_row.is_OK());
+    m_pivot_row_of_B_1.clear();
+    m_pivot_row_of_B_1.resize(m_m());
+    m_pivot_row.clear();
+    m_pivot_row.resize(m_n());
+    if (m_settings.use_tableau()) {
+        unsigned basis_j = m_basis[i];
+        for (auto & c : m_A.m_rows[i]) {
+            if (c.m_j != basis_j)
+                m_pivot_row.set_value(c.get_val(), c.m_j);
+        }
+        return;
+    }
+
+    calculate_pivot_row_of_B_1(i);
+    calculate_pivot_row_when_pivot_row_of_B1_is_ready(i);
+}
+
+
 }

src/util/lp/lp_core_solver_base_instances.cpp

@@ -129,3 +129,4 @@ template bool lean::lp_core_solver_base<lean::mpq, lean::mpq>::inf_set_is_correc
 template bool lean::lp_core_solver_base<lean::mpq, lean::numeric_pair<lean::mpq> >::infeasibility_costs_are_correct() const;
 template bool lean::lp_core_solver_base<lean::mpq, lean::mpq >::infeasibility_costs_are_correct() const;
 template bool lean::lp_core_solver_base<double, double >::infeasibility_costs_are_correct() const;
+template void lean::lp_core_solver_base<lean::mpq, lean::numeric_pair<lean::mpq> >::calculate_pivot_row(unsigned int);