rm lu

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

src/math/lp/lar_core_solver.h

@@ -274,47 +274,6 @@ class lar_core_solver  {
     }
 
 
-
-    void prepare_solver_x_with_signature_tableau(const lar_solution_signature & signature) {
-        lp_assert(m_r_solver.inf_set_is_correct());
-        for (auto &t : signature) {
-            unsigned j = t.first;
-            if (m_r_heading[j] >= 0)
-                continue;
-            auto pos_type = t.second;
-            numeric_pair<mpq> delta;
-            if (!update_xj_and_get_delta(j, pos_type, delta))
-                continue;
-            for (const auto & cc : m_r_solver.m_A.m_columns[j]){
-                unsigned i = cc.var();
-                unsigned jb = m_r_solver.m_basis[i];
-                m_r_solver.add_delta_to_x_and_track_feasibility(jb, - delta * m_r_solver.m_A.get_val(cc));
-            }
-
-        }
-        lp_assert(m_r_solver.inf_set_is_correct());
-    }
-
-
-
-    bool adjust_x_of_column(unsigned j) {
-        /*
-        if (m_r_solver.m_basis_heading[j] >= 0) {
-            return false;
-        }
-
-        if (m_r_solver.column_is_feasible(j)) {
-            return false;
-        }
-
-        m_r_solver.snap_column_to_bound_tableau(j);
-        lp_assert(m_r_solver.column_is_feasible(j));
-        m_r_solver.m_inf_set.erase(j);
-        */
-        lp_assert(false);
-        return true;
-    }
-
 
     bool r_basis_is_OK() const {
 #ifdef Z3DEBUG

src/math/lp/lar_solver.cpp

@@ -643,11 +643,6 @@ namespace lp {
     bool lar_solver::use_tableau_costs() const {
         return m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs;
     }
-
-    void lar_solver::adjust_x_of_column(unsigned j) {
-        lp_assert(false);
-    }
-
     bool lar_solver::row_is_correct(unsigned i) const {
         numeric_pair<mpq> r = zero_of_type<numeric_pair<mpq>>();
         for (const auto& c : A_r().m_rows[i]) {

src/math/lp/lar_solver.h

@@ -210,7 +210,6 @@ class lar_solver : public column_namer {
     void detect_rows_of_bound_change_column_for_nbasic_column_tableau(unsigned j);
     bool use_tableau_costs() const;
     void detect_rows_of_column_with_bound_change(unsigned j);
-    void adjust_x_of_column(unsigned j);
     bool tableau_with_costs() const;
     bool costs_are_used() const;
     void change_basic_columns_dependend_on_a_given_nb_column(unsigned j, const numeric_pair<mpq> & delta);

src/math/lp/lp_core_solver_base.cpp

@@ -24,7 +24,6 @@ Revision History:
 #include <functional>
 #include "math/lp/lp_core_solver_base_def.h"
 template bool lp::lp_core_solver_base<double, double>::basis_heading_is_correct() const;
-template void lp::lp_core_solver_base<double, double>::calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned);
 template bool lp::lp_core_solver_base<double, double>::column_is_dual_feasible(unsigned int) const;
 template void lp::lp_core_solver_base<double, double>::fill_reduced_costs_from_m_y_by_rows();
 template lp::non_basic_column_value_position lp::lp_core_solver_base<double, double>::get_non_basic_column_value_position(unsigned int) const;
@@ -44,20 +43,16 @@ template bool lp::lp_core_solver_base<double, double>::print_statistics_with_ite
 template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over(char const*, std::ostream &);
 template void lp::lp_core_solver_base<double, double>::restore_x(unsigned int, double const&);
 template void lp::lp_core_solver_base<double, double>::set_non_basic_x_to_correct_bounds();
-template void lp::lp_core_solver_base<double, double>::snap_xN_to_bounds_and_free_columns_to_zeroes();
-template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::snap_xN_to_bounds_and_free_columns_to_zeroes();
 template void lp::lp_core_solver_base<double, double>::solve_Ax_eq_b();
 template void lp::lp_core_solver_base<double, double>::add_delta_to_entering(unsigned int, const double&);
 template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::basis_heading_is_correct() const ;
-template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned);
 template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::column_is_dual_feasible(unsigned int) const;
 template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::fill_reduced_costs_from_m_y_by_rows();
 template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over(char const*, std::ostream &);
 template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::restore_x(unsigned int, lp::mpq const&);
 template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::set_non_basic_x_to_correct_bounds();
 template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::solve_Ax_eq_b();
 template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::add_delta_to_entering(unsigned int, const lp::mpq&);
-template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned);
 template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::init();
 template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::init_basis_heading_and_non_basic_columns_vector();
 template lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::lp_core_solver_base(lp::static_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&, 
@@ -85,18 +80,10 @@ template lp::lp_core_solver_base<lp::mpq, lp::mpq>::lp_core_solver_base(
 template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::print_statistics_with_iterations_and_check_that_the_time_is_over(std::ostream &);
 template std::string lp::lp_core_solver_base<double, double>::column_name(unsigned int) const;
 template void lp::lp_core_solver_base<double, double>::pretty_print(std::ostream & out);
-template void lp::lp_core_solver_base<double, double>::restore_state(double*, double*);
-template void lp::lp_core_solver_base<double, double>::save_state(double*, double*);
 template std::string lp::lp_core_solver_base<lp::mpq, lp::mpq>::column_name(unsigned int) const;
 template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::pretty_print(std::ostream & out);
-template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::restore_state(lp::mpq*, lp::mpq*);
-template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::save_state(lp::mpq*, lp::mpq*);
 template std::string lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::column_name(unsigned int) const;
 template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::pretty_print(std::ostream & out);
-template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::restore_state(lp::mpq*, lp::mpq*);
-template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::save_state(lp::mpq*, lp::mpq*);
-template void lp::lp_core_solver_base<double, double>::init_lu();
-template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::init_lu();
 template int lp::lp_core_solver_base<double, double>::pivots_in_column_and_row_are_different(int, int) const;
 template int lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::pivots_in_column_and_row_are_different(int, int) const;
 template int lp::lp_core_solver_base<lp::mpq, lp::mpq>::pivots_in_column_and_row_are_different(int, int) const;
@@ -109,7 +96,6 @@ template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::column_is_feasible(unsi
 // template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::print_linear_combination_of_column_indices(vector<std::pair<lp::mpq, unsigned int>, std::allocator<std::pair<lp::mpq, unsigned int> > > const&, std::ostream&) const;
 template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::column_is_feasible(unsigned int) const;
 template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::snap_non_basic_x_to_bound();
-template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::init_lu();
 template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::restore_x(unsigned int, lp::numeric_pair<lp::mpq> const&);
 template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq>>::pivot_column_tableau(unsigned int, unsigned int);
 template bool lp::lp_core_solver_base<double, double>::pivot_column_tableau(unsigned int, unsigned int);

src/math/lp/lp_core_solver_base.h

@@ -156,10 +156,6 @@ class lp_core_solver_base {
 
     void pretty_print(std::ostream & out);
 
-    void save_state(T * w_buffer, T * d_buffer);
-
-    void restore_state(T * w_buffer, T * d_buffer);
-
     X get_cost() const {
         return dot_product(m_costs, m_x);
     }
@@ -173,8 +169,6 @@ class lp_core_solver_base {
 
     void restore_m_ed(T * buffer);
 
-    void calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned pivot_row);
-
     void add_delta_to_entering(unsigned entering, const X & delta);
 
     const X & get_var_value(unsigned j) const {
@@ -422,11 +416,9 @@ class lp_core_solver_base {
     void snap_non_basic_x_to_bound_and_free_to_zeroes();
     void snap_xN_to_bounds_and_fill_xB();
 
-    void snap_xN_to_bounds_and_free_columns_to_zeroes();
-
+
     non_basic_column_value_position get_non_basic_column_value_position(unsigned j) const;
 
-    void init_lu();
     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);

src/math/lp/lp_core_solver_base_def.h

@@ -136,17 +136,6 @@ pretty_print(std::ostream & out) {
     pp.print();
 }
 
-template <typename T, typename X> void lp_core_solver_base<T, X>::
-save_state(T * w_buffer, T * d_buffer) {
-    copy_m_w(w_buffer);
-    copy_m_ed(d_buffer);
-}
-
-template <typename T, typename X> void lp_core_solver_base<T, X>::
-restore_state(T * w_buffer, T * d_buffer) {
-    restore_m_w(w_buffer);
-    restore_m_ed(d_buffer);
-}
 
 template <typename T, typename X> void lp_core_solver_base<T, X>::
 copy_m_w(T * buffer) {
@@ -185,26 +174,6 @@ restore_m_ed(T * buffer) {
 
 
 
-template <typename T, typename X> void lp_core_solver_base<T, X>::
-calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned pivot_row) {
-    m_pivot_row.clear();
-
-    for (unsigned i : m_pivot_row_of_B_1.m_index) {
-        const T & pi_1 = m_pivot_row_of_B_1[i];
-        if (numeric_traits<T>::is_zero(pi_1)) {
-            continue;
-        }
-        for (auto & c : m_A.m_rows[i]) {
-            unsigned j = c.var();
-            if (m_basis_heading[j] < 0) {
-                m_pivot_row.add_value_at_index_with_drop_tolerance(j, c.coeff() * pi_1);
-            }
-        }
-    }
-    if (precise()) {
-        m_rows_nz[pivot_row] = m_pivot_row.m_index.size();
-    }
-}
 
 template <typename T, typename X> void lp_core_solver_base<T, X>::
 add_delta_to_entering(unsigned entering, const X& delta) {
@@ -631,11 +600,6 @@ snap_xN_to_bounds_and_fill_xB() {
     solve_Ax_eq_b();
 }
 
-template <typename T, typename X> void lp_core_solver_base<T, X>::
-snap_xN_to_bounds_and_free_columns_to_zeroes() {
-    snap_non_basic_x_to_bound_and_free_to_zeroes();
-    solve_Ax_eq_b();
-}
 
 
 template <typename T, typename X> non_basic_column_value_position lp_core_solver_base<T, X>::
@@ -661,10 +625,6 @@ get_non_basic_column_value_position(unsigned j) const {
     return at_lower_bound;
 }
 
-template <typename T, typename X> void lp_core_solver_base<T, X>::init_lu() {
-    init_factorization(this->m_factorization, this->m_A, this->m_basis, this->m_settings);
-}
-
 template <typename T, typename X> int lp_core_solver_base<T, X>::pivots_in_column_and_row_are_different(int entering, int leaving) const {
     const T & column_p = this->m_ed[this->m_basis_heading[leaving]];
     const T & row_p = this->m_pivot_row[entering];