rm lp_solver

Z3Prover · Mar 4, 2023 · ff1dc04 · ff1dc04
1 parent 5e4bca3
commit ff1dc04
Show file tree

Hide file tree

Showing 8 changed files with 2 additions and 929 deletions.
diff --git a/src/math/lp/indexed_value.h b/src/math/lp/indexed_value.h
@@ -43,15 +43,4 @@ class indexed_value {
         m_value = val;
     }
 };
-#ifdef Z3DEBUG
-template <typename X>
-bool check_vector_for_small_values(indexed_vector<X> & w, lp_settings & settings) {
-    for (unsigned i : w.m_index) {
-        const X & v = w[i];
-        if ((!is_zero(v)) && settings.abs_val_is_smaller_than_drop_tolerance(v))
-            return false;
-    }
-    return true;
-}
-#endif
 }
diff --git a/src/math/lp/lar_core_solver.h b/src/math/lp/lar_core_solver.h
@@ -651,35 +651,7 @@ class lar_core_solver  {
         }
     }
 
-    void scale_problem_for_doubles(
-                        static_matrix<double, double>& A,        
-                        vector<double> & lower_bounds,
-                        vector<double> & upper_bounds) {
-        vector<double> column_scale_vector;
-        vector<double> right_side_vector(A.column_count());
-        settings().reps_in_scaler = 5;
-        scaler<double, double > scaler(right_side_vector,
-                                       A,
-                                       settings().scaling_minimum,
-                                       settings().scaling_maximum,
-                                       column_scale_vector,
-                                       settings());
-        if (! scaler.scale()) {
-            // the scale did not succeed, unscaling
-            A.clear();
-            create_double_matrix(A);
-        } else {
-            for (unsigned j = 0; j < A.column_count(); j++) {
-                if (m_r_solver.column_has_upper_bound(j)) {
-                    upper_bounds[j] /= column_scale_vector[j];
-                }
-                if (m_r_solver.column_has_lower_bound(j)) {
-                    lower_bounds[j] /= column_scale_vector[j];
-                }
-            }
-        }
-
-    }
+
     // returns the trace of basis changes
     vector<unsigned> find_solution_signature_with_doubles(lar_solution_signature & signature) {
         if (m_d_solver.m_factorization == nullptr || m_d_solver.m_factorization->get_status() != LU_status::OK) {

diff --git a/src/math/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h
@@ -30,7 +30,6 @@ Revision History:
 #include <cstdlib>
 #include <algorithm>
 #include "math/lp/lu.h"
-#include "math/lp/lp_solver.h"
 #include "math/lp/static_matrix.h"
 #include "math/lp/core_solver_pretty_printer.h"
 #include "math/lp/lp_core_solver_base.h"

diff --git a/src/math/lp/lp_solver.cpp b/src/math/lp/lp_solver.cpp
diff --git a/src/math/lp/lp_solver.h b/src/math/lp/lp_solver.h