rm lu related fields from lp_core_solver_base.h

src/math/lp/core_solver_pretty_printer.h

@@ -59,7 +59,7 @@ class core_solver_pretty_printer {
     unsigned m_artificial_start;
     indexed_vector<T> m_w_buff;
     indexed_vector<T> m_ed_buff;
-    vector<T> m_exact_column_norms;
+    
 
 public:
     core_solver_pretty_printer(const lp_core_solver_base<T, X > & core_solver, std::ostream & out);
@@ -85,14 +85,7 @@ public:
     }
 
     unsigned get_column_width(unsigned column);
-
-    unsigned regular_cell_width(unsigned row, unsigned column, const std::string & name) {
-        return regular_cell_string(row, column, name).size();
-    }
-
-    std::string regular_cell_string(unsigned row, unsigned column, std::string name);
-
-
+    
     void set_coeff(vector<string>& row, vector<string> & row_signs, unsigned col, const T & t, string name);
 
     void print_x();
@@ -105,12 +98,7 @@ public:
     void print_lows();
 
     void print_upps();
-
-    string get_exact_column_norm_string(unsigned col) {
-        return T_to_string(m_exact_column_norms[col]);
-    }
-
-
+    
     void print_approx_norms();
 
     void print();

src/math/lp/core_solver_pretty_printer_def.h

@@ -37,9 +37,8 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(const lp_core_solve
     m_signs(core_solver.m_A.row_count(), vector<string>(core_solver.m_A.column_count(), " ")),
     m_costs(ncols(), ""),
     m_cost_signs(ncols(), " "),
-    m_rs(ncols(), zero_of_type<X>()),
-    m_w_buff(core_solver.m_w),
-    m_ed_buff(core_solver.m_ed) {
+    m_rs(ncols(), zero_of_type<X>())
+     {
     m_lower_bounds_title = "low";
     m_upp_bounds_title = "upp";
     m_exact_norm_title = "exact cn";
@@ -80,13 +79,6 @@ template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_rs
     }
 }
 
-template <typename T, typename X> T core_solver_pretty_printer<T, X>::current_column_norm() {
-    T ret = zero_of_type<T>();
-    for (auto i : m_core_solver.m_ed.m_index)
-        ret += m_core_solver.m_ed[i] * m_core_solver.m_ed[i];
-    return ret;
-}
-
 template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_m_A_and_signs() { 
         for (unsigned column = 0; column < ncols(); column++) {
             vector<T> t(nrows(), zero_of_type<T>());
@@ -167,13 +159,6 @@ template <typename T, typename X> unsigned core_solver_pretty_printer<T, X>:: ge
     return w;
 }
 
-template <typename T, typename X> std::string core_solver_pretty_printer<T, X>::regular_cell_string(unsigned row, unsigned /* column */, std::string name) {
-    T t = fabs(m_core_solver.m_ed[row]);
-    if ( t == 1) return name;
-    return T_to_string(t) + name;
-}
-
-
 template <typename T, typename X> void core_solver_pretty_printer<T, X>::set_coeff(vector<string>& row, vector<string> & row_signs, unsigned col, const T & t, string name) {
     if (numeric_traits<T>::is_zero(t)) {
         return;

src/math/lp/indexed_vector_def.h

@@ -24,14 +24,6 @@ Revision History:
 #include "math/lp/lp_settings.h"
 namespace lp {
 
-template <typename T>
-void print_sparse_vector(const vector<T> & t, std::ostream & out) {
-    for (unsigned i = 0; i < t.size(); i++) {
-        if (is_zero(t[i]))continue;
-        out << "[" << i << "] = " << t[i] << ", ";
-    }
-    out << std::endl;
-}
 
 void print_vector_as_doubles(const vector<mpq> & t, std::ostream & out) {
     for (unsigned i = 0; i < t.size(); i++)

src/math/lp/lp_core_solver_base.cpp

@@ -29,9 +29,7 @@ template lp::non_basic_column_value_position lp::lp_core_solver_base<lp::mpq, lp
 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 bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::basis_heading_is_correct() const ;
 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>::add_delta_to_entering(unsigned int, const lp::mpq&);
 template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::init();
@@ -68,7 +66,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> >::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<lp::mpq, lp::mpq>::pivot_column_tableau(unsigned int, unsigned int);
 template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::transpose_rows_tableau(unsigned int, unsigned int);

src/math/lp/lp_core_solver_base.h

@@ -74,7 +74,6 @@ public:
     void set_using_infeas_costs(bool val)  { m_using_infeas_costs = val; }
     vector<unsigned>      m_columns_nz; // m_columns_nz[i] keeps an approximate value of non zeroes the i-th column
     vector<unsigned>      m_rows_nz; // m_rows_nz[i] keeps an approximate value of non zeroes in the i-th row
-    indexed_vector<T>     m_pivot_row_of_B_1;  // the pivot row of the reverse of B
     indexed_vector<T>     m_pivot_row; // this is the real pivot row of the simplex tableu
     static_matrix<T, X> & m_A; // the matrix A
     // vector<X> const &           m_b; // the right side
@@ -85,15 +84,11 @@ public:
     vector<T> &           m_costs;
     lp_settings &         m_settings;
     
-    vector<T>             m_y; // the buffer for yB = cb
     const column_namer &  m_column_names;
-    indexed_vector<T>     m_w; // the vector featuring in 24.3 of the Chvatal book
     vector<T>             m_d; // the vector of reduced costs
-    indexed_vector<T>     m_ed; // the solution of B*m_ed = a
     const vector<column_type> & m_column_types;
     const vector<X> &     m_lower_bounds;
     const vector<X> &     m_upper_bounds; 
-    vector<X>             m_copy_of_xB;
     unsigned              m_basis_sort_counter;
     vector<unsigned>      m_trace_of_basis_change_vector; // the even positions are entering, the odd positions are leaving
     bool                  m_tracing_basis_changes;
@@ -162,10 +157,6 @@ public:
         return dot_product(m_costs, m_x);
     }
 
-    void copy_m_w(T * buffer);
-
-    void restore_m_w(T * buffer);
-
     void add_delta_to_entering(unsigned entering, const X & delta);
 
     const X & get_var_value(unsigned j) const {
@@ -298,11 +289,6 @@ public:
 
     bool basis_heading_is_correct() const;
 
-    void restore_x(unsigned entering, X const & t);
-
-    void fill_reduced_costs_from_m_y_by_rows();
-
-    void copy_rs_to_xB(vector<X> & rs);
     virtual bool lower_bounds_are_set() const { return false; }
     X lower_bound_value(unsigned j) const { return m_lower_bounds[j]; }
     X upper_bound_value(unsigned j) const { return m_upper_bounds[j]; }
@@ -316,10 +302,6 @@ public:
 
     std::string column_name(unsigned column) const;
 
-    void add_delta_to_xB(vector<X> & del);
-
-    void find_error_in_BxB(vector<X>& rs);
-
     bool snap_non_basic_x_to_bound() {
         bool ret = false;
         for (unsigned j : non_basis())

src/math/lp/lp_core_solver_base_def.h

@@ -44,25 +44,19 @@ lp_core_solver_base(static_matrix<T, X> & A,
     m_status(lp_status::FEASIBLE),
     m_inf_set(A.column_count()),
     m_using_infeas_costs(false),
-    m_pivot_row_of_B_1(A.row_count()),
     m_pivot_row(A.column_count()),
     m_A(A),
-    // m_b(b),
     m_basis(basis),
     m_nbasis(nbasis),
     m_basis_heading(heading),
     m_x(x),
     m_costs(costs),
     m_settings(settings),
-    m_y(m_m()),
     m_column_names(column_names),
-    m_w(m_m()),
     m_d(m_n()),
-    m_ed(m_m()),
     m_column_types(column_types),
     m_lower_bounds(lower_bound_values),
     m_upper_bounds(upper_bound_values),
-    m_copy_of_xB(m_m()),
     m_basis_sort_counter(0),
     m_tracing_basis_changes(false),
     m_pivoted_rows(nullptr),
@@ -122,25 +116,6 @@ pretty_print(std::ostream & out) {
 }
 
 
-template <typename T, typename X> void lp_core_solver_base<T, X>::
-copy_m_w(T * buffer) {
-    unsigned i = m_m();
-    while (i --) {
-        buffer[i] = m_w[i];
-    }
-}
-
-template <typename T, typename X> void lp_core_solver_base<T, X>::
-restore_m_w(T * buffer) {
-    m_w.m_index.clear();
-    unsigned i = m_m();
-    while (i--) {
-        if (!is_zero(m_w[i] = buffer[i]))
-            m_w.m_index.push_back(i);
-    }
-}
-
-
 template <typename T, typename X> void lp_core_solver_base<T, X>::
 add_delta_to_entering(unsigned entering, const X& delta) {
     m_x[entering] += delta;
@@ -443,73 +418,11 @@ template <typename T, typename X> bool lp_core_solver_base<T, X>::
     return true;
 }
 
-template <typename T, typename X> void lp_core_solver_base<T, X>::
-restore_x(unsigned entering, X const & t) {
-    if (is_zero(t)) return;
-    m_x[entering] -= t;
-    for (unsigned i : m_ed.m_index) {
-        m_x[m_basis[i]]  = m_copy_of_xB[i];
-    }
-}
-
-template <typename T, typename X> void lp_core_solver_base<T, X>::
-fill_reduced_costs_from_m_y_by_rows() {
-    unsigned j = m_n();
-    while (j--) {
-        if (m_basis_heading[j] < 0)
-            m_d[j] = m_costs[j];
-        else
-            m_d[j] = numeric_traits<T>::zero();
-    }
-
-    unsigned i = m_m();
-    while (i--) {
-        const T & y = m_y[i];
-        if (is_zero(y)) continue;
-        for (row_cell<T> & c : m_A.m_rows[i]) {
-            j = c.var();
-            if (m_basis_heading[j] < 0) {
-                m_d[j] -= y * c.coeff();
-            }
-        }
-    }
-}
-
-template <typename T, typename X> void lp_core_solver_base<T, X>::
-copy_rs_to_xB(vector<X> & rs) {
-    unsigned j = m_m();
-    while (j--) {
-        m_x[m_basis[j]] = rs[j];
-    }
-}
-
 template <typename T, typename X> std::string lp_core_solver_base<T, X>::
 column_name(unsigned column) const {
     return m_column_names.get_variable_name(column);
 }
 
-template <typename T, typename X> void lp_core_solver_base<T, X>::
-add_delta_to_xB(vector<X> & del) {
-    unsigned i = m_m();
-    while (i--) {
-        this->m_x[this->m_basis[i]] -= del[i];
-    }
-}
-
-template <typename T, typename X> void lp_core_solver_base<T, X>::
-find_error_in_BxB(vector<X>& rs){
-    unsigned row = m_m();
-    while (row--) {
-        auto &rsv = rs[row];
-        for (auto & it : m_A.m_rows[row]) {
-            unsigned j = it.var();
-            if (m_basis_heading[j] >= 0) {
-                rsv -= m_x[j] * it.coeff();
-            }
-        }
-    }
-}
-
 template <typename T, typename X> non_basic_column_value_position lp_core_solver_base<T, X>::
 get_non_basic_column_value_position(unsigned j) const {
     switch (m_column_types[j]) {
@@ -543,9 +456,9 @@ template <typename T, typename X> bool lp_core_solver_base<T, X>::pivot_column_g
 	lp_assert(m_basis_heading[j_basic] >= 0);
 	unsigned row_index = m_basis_heading[j_basic];
 	  // the tableau case
-		if (pivot_column_tableau(j, row_index))
-			change_basis(j, j_basic);
-		else return false;
+	if (pivot_column_tableau(j, row_index))
+		change_basis(j, j_basic);
+	else return false;
 	
 	return true;
 }

src/math/lp/permutation_matrix.h

@@ -22,7 +22,6 @@ Revision History:
 #include <algorithm>
 #include "util/debug.h"
 #include <string>
-#include "math/lp/sparse_vector.h"
 #include "math/lp/indexed_vector.h"
 #include "math/lp/lp_settings.h"
 #include "math/lp/matrix.h"

src/math/lp/sparse_vector.h

@@ -1,52 +0,0 @@
-/*++
-Copyright (c) 2017 Microsoft Corporation
-
-Module Name:
-
-    <name>
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Lev Nachmanson (levnach)
-
-Revision History:
-
-
---*/
-
-#pragma once
-#include "util/vector.h"
-#include <utility>
-#include "util/debug.h"
-#include "math/lp/lp_utils.h"
-#include "math/lp/lp_settings.h"
-namespace lp {
-
-template <typename T>
-class sparse_vector {
-public:
-    vector<std::pair<unsigned, T>>  m_data;
-    void push_back(unsigned index, T val) {
-        m_data.push_back(std::make_pair(index, val));
-    }
-#ifdef Z3DEBUG
-    T operator[] (unsigned i) const {
-        for (auto &t : m_data) {
-            if (t.first == i) return t.second;
-        }
-        return numeric_traits<T>::zero();
-    }
-#endif
-    void divide(T const & a) {
-        for (auto & t : m_data) {  t.second /= a; }
-    }
-
-    unsigned size() const {
-        return m_data.size();
-    }
-};
-}

src/math/lp/static_matrix.h

@@ -12,7 +12,6 @@ Author:
 #include <set>
 #include <unordered_map>
 #include <utility>
-#include "math/lp/sparse_vector.h"
 #include "math/lp/indexed_vector.h"
 #include "math/lp/permutation_matrix.h"
 #include <stack>