From 178135486c5fb8f20bd433604208ffa54a79f4fd Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 6 Mar 2023 13:56:04 -0800 Subject: [PATCH] rm scaler --- src/math/lp/CMakeLists.txt | 1 - src/math/lp/lar_solver.h | 1 - src/math/lp/scaler.cpp | 22 --- src/math/lp/scaler.h | 94 ------------ src/math/lp/scaler_def.h | 270 ---------------------------------- src/math/lp/static_matrix.cpp | 1 - 6 files changed, 389 deletions(-) delete mode 100644 src/math/lp/scaler.cpp delete mode 100644 src/math/lp/scaler.h delete mode 100644 src/math/lp/scaler_def.h diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt index 5d21bba70..5ccc023ab 100644 --- a/src/math/lp/CMakeLists.txt +++ b/src/math/lp/CMakeLists.txt @@ -41,7 +41,6 @@ z3_add_component(lp permutation_matrix.cpp random_updater.cpp row_eta_matrix.cpp - scaler.cpp square_sparse_matrix.cpp static_matrix.cpp COMPONENT_DEPENDENCIES diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 09612d905..be255dd65 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -31,7 +31,6 @@ #include "math/lp/lar_constraints.h" #include "math/lp/lar_core_solver.h" #include "math/lp/numeric_pair.h" -#include "math/lp/scaler.h" #include "math/lp/lp_primal_core_solver.h" #include "math/lp/random_updater.h" #include "util/stacked_value.h" diff --git a/src/math/lp/scaler.cpp b/src/math/lp/scaler.cpp deleted file mode 100644 index 46330e2a1..000000000 --- a/src/math/lp/scaler.cpp +++ /dev/null @@ -1,22 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - - -Abstract: - - - -Author: - - Lev Nachmanson (levnach) - -Revision History: - - ---*/ -#include "math/lp/scaler_def.h" -template bool lp::scaler::scale(); -template bool lp::scaler::scale(); diff --git a/src/math/lp/scaler.h b/src/math/lp/scaler.h deleted file mode 100644 index dd21b5c28..000000000 --- a/src/math/lp/scaler.h +++ /dev/null @@ -1,94 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - - -Abstract: - - - -Author: - - Lev Nachmanson (levnach) - -Revision History: - - ---*/ - -#pragma once -#include "util/vector.h" -#include -#include -#include /* printf, fopen */ -#include /* exit, EXIT_FAILURE */ -#include "math/lp/lp_utils.h" -#include "math/lp/static_matrix.h" -namespace lp { -// for scaling an LP -template -class scaler { - vector & m_b; // right side - static_matrix &m_A; // the constraint matrix - const T & m_scaling_minimum; - const T & m_scaling_maximum; - vector& m_column_scale; - lp_settings & m_settings; -public: - // constructor - scaler(vector & b, static_matrix &A, const T & scaling_minimum, const T & scaling_maximum, vector & column_scale, - lp_settings & settings): - m_b(b), - m_A(A), - m_scaling_minimum(scaling_minimum), - m_scaling_maximum(scaling_maximum), - m_column_scale(column_scale), - m_settings(settings) { - lp_assert(m_column_scale.size() == 0); - m_column_scale.resize(m_A.column_count(), numeric_traits::one()); - } - - T right_side_balance(); - - T get_balance() { return m_A.get_balance(); } - - T A_min() const; - - T A_max() const; - - T get_A_ratio() const; - - T get_max_ratio_on_rows() const; - - T get_max_ratio_on_columns() const; - - void scale_rows_with_geometric_mean(); - - void scale_columns_with_geometric_mean(); - - void scale_once_for_ratio(); - - bool scale_with_ratio(); - - void bring_row_maximums_to_one(); - - void bring_column_maximums_to_one(); - - void bring_rows_and_columns_maximums_to_one(); - - bool scale_with_log_balance(); - // Returns true if and only if the scaling was successful. - // It is the caller responsibility to restore the matrix - bool scale(); - - void scale_rows(); - - void scale_row(unsigned i); - - void scale_column(unsigned i); - - void scale_columns(); -}; -} diff --git a/src/math/lp/scaler_def.h b/src/math/lp/scaler_def.h deleted file mode 100644 index 8604a67a1..000000000 --- a/src/math/lp/scaler_def.h +++ /dev/null @@ -1,270 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - - -Abstract: - - - -Author: - - Lev Nachmanson (levnach) - -Revision History: - - ---*/ -#pragma once - -#include -#include "math/lp/scaler.h" -#include "math/lp/numeric_pair.h" -namespace lp { -// for scaling an LP -template T scaler::right_side_balance() { - T ret = zero_of_type(); - unsigned i = m_A.row_count(); - while (i--) { - T rs = abs(convert_struct::convert(m_b[i])); - if (!is_zero(rs)) { - numeric_traits::log(rs); - ret += rs * rs; - } - } - return ret; -} - -template T scaler::A_min() const { - T min = zero_of_type(); - for (unsigned i = 0; i < m_A.row_count(); i++) { - T t = m_A.get_min_abs_in_row(i); - min = i == 0 ? t : std::min(t, min); - } - return min; -} - -template T scaler::A_max() const { - T max = zero_of_type(); - for (unsigned i = 0; i < m_A.row_count(); i++) { - T t = m_A.get_max_abs_in_row(i); - max = i == 0? t : std::max(t, max); - } - return max; -} - -template T scaler::get_A_ratio() const { - T min = A_min(); - T max = A_max(); - lp_assert(!m_settings.abs_val_is_smaller_than_zero_tolerance(min)); - T ratio = max / min; - return ratio; -} - -template T scaler::get_max_ratio_on_rows() const { - T ret = T(1); - unsigned i = m_A.row_count(); - while (i--) { - T den = m_A.get_min_abs_in_row(i); - lp_assert(!m_settings.abs_val_is_smaller_than_zero_tolerance(den)); - T t = m_A.get_max_abs_in_row(i)/ den; - if (t > ret) - ret = t; - } - return ret; -} - -template T scaler::get_max_ratio_on_columns() const { - T ret = T(1); - unsigned i = m_A.column_count(); - while (i--) { - T den = m_A.get_min_abs_in_column(i); - if (m_settings.abs_val_is_smaller_than_zero_tolerance(den)) - continue; // got a zero column - T t = m_A.get_max_abs_in_column(i)/den; - if (t > ret) - ret = t; - } - return ret; -} - -template void scaler::scale_rows_with_geometric_mean() { - unsigned i = m_A.row_count(); - while (i--) { - T max = m_A.get_max_abs_in_row(i); - T min = m_A.get_min_abs_in_row(i); - lp_assert(max > zero_of_type() && min > zero_of_type()); - if (is_zero(max) || is_zero(min)) - continue; - T gm = T(sqrt(numeric_traits::get_double(max*min))); - if (m_settings.is_eps_small_general(gm, 0.01)) { - continue; - } - m_A.multiply_row(i, one_of_type() / gm); - m_b[i] /= gm; - } -} - -template void scaler::scale_columns_with_geometric_mean() { - unsigned i = m_A.column_count(); - while (i--) { - T max = m_A.get_max_abs_in_column(i); - T min = m_A.get_min_abs_in_column(i); - T den = T(sqrt(numeric_traits::get_double(max*min))); - if (m_settings.is_eps_small_general(den, 0.01)) - continue; // got a zero column - T gm = T(1)/ den; - T cs = m_column_scale[i] * gm; - if (m_settings.is_eps_small_general(cs, 0.1)) - continue; - m_A.multiply_column(i, gm); - m_column_scale[i] = cs; - } -} - -template void scaler::scale_once_for_ratio() { - T max_ratio_on_rows = get_max_ratio_on_rows(); - T max_ratio_on_columns = get_max_ratio_on_columns(); - bool scale_rows_first = max_ratio_on_rows > max_ratio_on_columns; - // if max_ratio_on_columns is the largest then the rows are in worse shape than columns - if (scale_rows_first) { - scale_rows_with_geometric_mean(); - scale_columns_with_geometric_mean(); - } else { - scale_columns_with_geometric_mean(); - scale_rows_with_geometric_mean(); - } -} - -template bool scaler::scale_with_ratio() { - T ratio = get_A_ratio(); - // The ratio is greater than or equal to one. We would like to diminish it and bring it as close to 1 as possible - unsigned reps = m_settings.reps_in_scaler; - do { - scale_once_for_ratio(); - T new_r = get_A_ratio(); - if (new_r >= T(0.9) * ratio) - break; - } while (reps--); - - bring_rows_and_columns_maximums_to_one(); - return true; -} - -template void scaler::bring_row_maximums_to_one() { - unsigned i = m_A.row_count(); - while (i--) { - T t = m_A.get_max_abs_in_row(i); - if (m_settings.abs_val_is_smaller_than_zero_tolerance(t)) continue; - m_A.multiply_row(i, one_of_type() / t); - m_b[i] /= t; - } -} - -template void scaler::bring_column_maximums_to_one() { - unsigned i = m_A.column_count(); - while (i--) { - T max = m_A.get_max_abs_in_column(i); - if (m_settings.abs_val_is_smaller_than_zero_tolerance(max)) continue; - T t = T(1) / max; - m_A.multiply_column(i, t); - m_column_scale[i] *= t; - } -} - -template void scaler::bring_rows_and_columns_maximums_to_one() { - if (get_max_ratio_on_rows() > get_max_ratio_on_columns()) { - bring_row_maximums_to_one(); - bring_column_maximums_to_one(); - } else { - bring_column_maximums_to_one(); - bring_row_maximums_to_one(); - } -} - -template bool scaler::scale_with_log_balance() { - T balance = get_balance(); - T balance_before_scaling = balance; - // todo : analyze the scale order : rows-columns, or columns-rows. Iterate if needed - for (int i = 0; i < 10; i++) { - scale_rows(); - scale_columns(); - T nb = get_balance(); - if (nb < T(0.9) * balance) { - balance = nb; - } else { - balance = nb; - break; - } - } - return balance <= balance_before_scaling; -} -// Returns true if and only if the scaling was successful. -// It is the caller responsibility to restore the matrix -template bool scaler::scale() { - if (numeric_traits::precise()) return true; - if (m_settings.scale_with_ratio) - return scale_with_ratio(); - return scale_with_log_balance(); -} - -template void scaler::scale_rows() { - for (unsigned i = 0; i < m_A.row_count(); i++) - scale_row(i); -} - -template void scaler::scale_row(unsigned i) { - T row_max = std::max(m_A.get_max_abs_in_row(i), abs(convert_struct::convert(m_b[i]))); - T alpha = numeric_traits::one(); - if (numeric_traits::is_zero(row_max)) { - return; - } - if (row_max < m_scaling_minimum) { - do { - alpha *= T(2); - row_max *= T(2); - } while (row_max < m_scaling_minimum); - m_A.multiply_row(i, alpha); - m_b[i] *= alpha; - } else if (row_max > m_scaling_maximum) { - do { - alpha /= T(2); - row_max /= T(2); - } while (row_max > m_scaling_maximum); - m_A.multiply_row(i, alpha); - m_b[i] *= alpha; - } -} - -template void scaler::scale_column(unsigned i) { - T column_max = m_A.get_max_abs_in_column(i); - T alpha = numeric_traits::one(); - - if (numeric_traits::is_zero(column_max)){ - return; // the column has zeros only - } - if (column_max < m_scaling_minimum) { - do { - alpha *= T(2); - column_max *= T(2); - } while (column_max < m_scaling_minimum); - } else if (column_max > m_scaling_maximum) { - do { - alpha /= T(2); - column_max /= T(2); - } while (column_max > m_scaling_maximum); - } else { - return; - } - m_A.multiply_column(i, alpha); - m_column_scale[i] = alpha; -} - -template void scaler::scale_columns() { - for (unsigned i = 0; i < m_A.column_count(); i++) { - scale_column(i); - } -} -} diff --git a/src/math/lp/static_matrix.cpp b/src/math/lp/static_matrix.cpp index 93360b914..12d2f9f0d 100644 --- a/src/math/lp/static_matrix.cpp +++ b/src/math/lp/static_matrix.cpp @@ -24,7 +24,6 @@ Revision History: #include "math/lp/static_matrix_def.h" #include "math/lp/lp_core_solver_base.h" #include "math/lp/lp_primal_core_solver.h" -#include "math/lp/scaler.h" #include "math/lp/lar_solver.h" namespace lp { template void static_matrix::add_columns_at_the_end(unsigned int);