rm lu

Z3Prover · Mar 8, 2023 · e04e726 · e04e726
1 parent 2e9dc3d
commit e04e726
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 40 deletions.
diff --git a/src/math/lp/lar_core_solver.h b/src/math/lp/lar_core_solver.h
@@ -56,8 +56,6 @@ class lar_core_solver  {
 
 
     lp_primal_core_solver<mpq, numeric_pair<mpq>> m_r_solver; // solver in rational numbers
-
-    lp_primal_core_solver<double, double> m_d_solver; // solver in doubles
 
     lar_core_solver(
                     lp_settings & settings,
@@ -140,7 +138,6 @@ class lar_core_solver  {
 
     void push() {
         lp_assert(m_r_solver.basis_heading_is_correct());
-        lp_assert(!need_to_presolve_with_double_solver() || m_d_solver.basis_heading_is_correct());
         lp_assert(m_column_types.size() == m_r_A.column_count());
         m_stacked_simplex_strategy = settings().simplex_strategy();
         m_stacked_simplex_strategy.push();
@@ -196,13 +193,9 @@ class lar_core_solver  {
         m_stacked_simplex_strategy.pop(k);
         settings().set_simplex_strategy(m_stacked_simplex_strategy);
         lp_assert(m_r_solver.basis_heading_is_correct());
-        lp_assert(!need_to_presolve_with_double_solver() || m_d_solver.basis_heading_is_correct());
-    }
-
-    bool need_to_presolve_with_double_solver() const {
-        return false;
     }
 
+
     template <typename L>
     bool is_zero_vector(const vector<L> & b) {
         for (const L & m: b)

diff --git a/src/math/lp/lar_core_solver_def.h b/src/math/lp/lar_core_solver_def.h
@@ -31,18 +31,6 @@ lar_core_solver::lar_core_solver(
                m_r_lower_bounds(),
                m_r_upper_bounds(),
                settings,
-               column_names),
-    m_d_solver(m_d_A,
-               m_d_right_sides_dummy,
-               m_d_x,
-               m_d_basis,
-               m_d_nbasis,
-               m_d_heading,
-               m_d_costs_dummy,
-               m_column_types(),
-               m_d_lower_bounds,
-               m_d_upper_bounds,
-               settings,
                column_names) {
 }    
 
@@ -57,22 +45,7 @@ void lar_core_solver::prefix_r() {
     }
 }
 
-void lar_core_solver::prefix_d() {
-    // m_d_solver.m_b.resize(m_d_solver.m_m());
-    m_d_solver.m_copy_of_xB.resize(m_d_solver.m_n());
-    m_d_solver.m_costs.resize(m_d_solver.m_n());
-    m_d_solver.m_d.resize(m_d_solver.m_n());
-    m_d_solver.m_ed.resize(m_d_solver.m_m());
-    m_d_solver.m_pivot_row.resize(m_d_solver.m_n());
-    m_d_solver.m_pivot_row_of_B_1.resize(m_d_solver.m_m());
-    m_d_solver.m_w.resize(m_d_solver.m_m());
-    m_d_solver.m_y.resize(m_d_solver.m_m());
-    m_d_solver.m_steepest_edge_coefficients.resize(m_d_solver.m_n());
-    m_d_solver.m_column_norms.clear();
-    m_d_solver.m_column_norms.resize(m_d_solver.m_n(), 2);
-    m_d_solver.clear_inf_set();
-    m_d_solver.resize_inf_set(m_d_solver.m_n());
-}
+
 
 void lar_core_solver::fill_not_improvable_zero_sum_from_inf_row() {
     unsigned bj = m_r_basis[m_r_solver.m_inf_row_index_for_tableau];

diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
@@ -47,7 +47,6 @@ namespace lp {
 
 
     bool lar_solver::sizes_are_correct() const {
-        lp_assert(strategy_is_undecided() || !m_mpq_lar_core_solver.need_to_presolve_with_double_solver() || A_r().column_count() == A_d().column_count());
         lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_column_types.size());
         lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size());
         lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_x.size());
@@ -748,9 +747,6 @@ namespace lp {
 
 
     void lar_solver::solve_with_core_solver() {
-        if (m_mpq_lar_core_solver.need_to_presolve_with_double_solver()) {
-            add_last_rows_to_lu(m_mpq_lar_core_solver.m_d_solver);
-        }
         m_mpq_lar_core_solver.prefix_r();
         if (costs_are_used()) {
             m_basic_columns_with_changed_cost.resize(m_mpq_lar_core_solver.m_r_x.size());