remove operation with doubles

src/math/lp/CMakeLists.txt

@@ -4,7 +4,6 @@ z3_add_component(lp
     binary_heap_upair_queue.cpp
     core_solver_pretty_printer.cpp
     dense_matrix.cpp
-    eta_matrix.cpp
     emonics.cpp
     factorization.cpp
     factorization_factory_imp.cpp
@@ -19,13 +18,8 @@ z3_add_component(lp
     lar_solver.cpp
     lar_core_solver.cpp
     lp_core_solver_base.cpp
-    lp_dual_core_solver.cpp
-    lp_dual_simplex.cpp
     lp_primal_core_solver.cpp
-    lp_primal_simplex.cpp
     lp_settings.cpp
-    lp_solver.cpp
-    lu.cpp
     lp_utils.cpp
     matrix.cpp
     mon_eq.cpp
@@ -45,10 +39,6 @@ z3_add_component(lp
     nra_solver.cpp    
     permutation_matrix.cpp
     random_updater.cpp      
-    row_eta_matrix.cpp
-    scaler.cpp
-    square_dense_submatrix.cpp
-    square_sparse_matrix.cpp
     static_matrix.cpp
   COMPONENT_DEPENDENCIES
     util

src/math/lp/core_solver_pretty_printer.h

@@ -110,7 +110,6 @@ class core_solver_pretty_printer {
         return T_to_string(m_exact_column_norms[col]);
     }
 
-    void print_exact_norms();
 
     void print_approx_norms();
 

src/math/lp/core_solver_pretty_printer_def.h

@@ -59,22 +59,13 @@ core_solver_pretty_printer<T, X>::core_solver_pretty_printer(const lp_core_solve
 }
 
 template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_costs() {
-    if (!m_core_solver.use_tableau()) {
-        vector<T> local_y(m_core_solver.m_m());
-        m_core_solver.solve_yB(local_y);
-        for (unsigned i = 0; i < ncols(); i++) {
-            if (m_core_solver.m_basis_heading[i] < 0) {
-                T t = m_core_solver.m_costs[i] - m_core_solver.m_A.dot_product_with_column(local_y, i);
-                set_coeff(m_costs, m_cost_signs, i, t, m_core_solver.column_name(i));
-            }
-        }
-    } else {
+
         for (unsigned i = 0; i < ncols(); i++) {
             if (m_core_solver.m_basis_heading[i] < 0) {
                 set_coeff(m_costs, m_cost_signs, i, m_core_solver.m_d[i], m_core_solver.column_name(i));
             }
         }
-    }
+
 }
 
 template <typename T, typename X> core_solver_pretty_printer<T, X>::~core_solver_pretty_printer() {
@@ -97,7 +88,7 @@ template <typename T, typename X> T core_solver_pretty_printer<T, X>::current_co
 }
 
 template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_m_A_and_signs() { 
-    if (numeric_traits<T>::precise() && m_core_solver.m_settings.use_tableau()) {
+    if (numeric_traits<T>::precise() ) {
         for (unsigned column = 0; column < ncols(); column++) {
             vector<T> t(nrows(), zero_of_type<T>());
             for (const auto & c : m_core_solver.m_A.m_columns[column]){
@@ -125,23 +116,7 @@ template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_m_
                 m_rs[row] += t[row] * m_core_solver.m_x[column];
             }
         }
-    } else {
-        for (unsigned column = 0; column < ncols(); column++) {
-            m_core_solver.solve_Bd(column, m_ed_buff, m_w_buff); // puts the result into m_core_solver.m_ed
-            string name = m_core_solver.column_name(column);
-            for (unsigned row = 0; row < nrows(); row ++) {
-                set_coeff(
-                          m_A[row],
-                          m_signs[row],
-                          column,
-                          m_ed_buff[row],
-                          name);
-                m_rs[row] += m_ed_buff[row] * m_core_solver.m_x[column];
-            }
-            if (!m_core_solver.use_tableau())
-                m_exact_column_norms.push_back(current_column_norm() + T(1)); // a conversion missing 1 -> T
-        }
-    }
+    } 
 }
 
 template <typename T, typename X> void core_solver_pretty_printer<T, X>::init_column_widths() {
@@ -190,11 +165,7 @@ template <typename T, typename X> unsigned core_solver_pretty_printer<T, X>:: ge
             w = cellw;
         }
     }
-    if (!m_core_solver.use_tableau()) {
-        w = std::max(w, (unsigned)T_to_string(m_exact_column_norms[column]).size());
-        if (!m_core_solver.m_column_norms.empty())
-            w = std::max(w, (unsigned)T_to_string(m_core_solver.m_column_norms[column]).size());
-    }
+
     return w;
 }
 
@@ -315,41 +286,15 @@ template <typename T, typename X> void core_solver_pretty_printer<T, X>::print_u
     m_out << std::endl;
 }
 
-template <typename T, typename X> void core_solver_pretty_printer<T, X>::print_exact_norms() {
-    if (m_core_solver.use_tableau()) return;
-    int blanks = m_title_width + 1 - static_cast<int>(m_exact_norm_title.size());
-    m_out << m_exact_norm_title;
-    print_blanks_local(blanks, m_out);
-    for (unsigned i = 0; i < ncols(); i++) {
-        string s = get_exact_column_norm_string(i);
-        int blanks = m_column_widths[i] - static_cast<int>(s.size());
-        print_blanks_local(blanks, m_out);
-        m_out << s << "   ";
-    }
-    m_out << std::endl;
-}
 
 template <typename T, typename X> void core_solver_pretty_printer<T, X>::print_approx_norms() {
-    if (m_core_solver.use_tableau()) return;
-    int blanks = m_title_width + 1 - static_cast<int>(m_approx_norm_title.size());
-    m_out << m_approx_norm_title;
-    print_blanks_local(blanks, m_out);
-    for (unsigned i = 0; i < ncols(); i++) {
-        string s = T_to_string(m_core_solver.m_column_norms[i]);
-        int blanks = m_column_widths[i] - static_cast<int>(s.size());
-        print_blanks_local(blanks, m_out);
-        m_out << s << "   ";
-    }
-    m_out << std::endl;
+    return;
 }
 
 template <typename T, typename X> void core_solver_pretty_printer<T, X>::print() {
     for (unsigned i = 0; i < nrows(); i++) {
         print_row(i);
     }
-    print_exact_norms();
-    if (!m_core_solver.m_column_norms.empty())
-        print_approx_norms();
     m_out << std::endl;
     if (m_core_solver.inf_set().size()) {
         m_out << "inf columns: ";