From ff1dc0424ca73b70c314f710737213ea30a3fefe Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 3 Mar 2023 16:32:49 -0800 Subject: [PATCH] rm lp_solver --- src/math/lp/indexed_value.h | 11 - src/math/lp/lar_core_solver.h | 30 +- src/math/lp/lp_primal_core_solver.h | 1 - src/math/lp/lp_solver.cpp | 55 --- src/math/lp/lp_solver.h | 260 ------------- src/math/lp/lp_solver_def.h | 571 ---------------------------- src/sat/smt/arith_solver.h | 2 +- src/smt/theory_lra.cpp | 1 - 8 files changed, 2 insertions(+), 929 deletions(-) delete mode 100644 src/math/lp/lp_solver.cpp delete mode 100644 src/math/lp/lp_solver.h delete mode 100644 src/math/lp/lp_solver_def.h diff --git a/src/math/lp/indexed_value.h b/src/math/lp/indexed_value.h index c4837647099..92d8f2adf1f 100644 --- 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 -bool check_vector_for_small_values(indexed_vector & 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 index 8a6c64ef00f..de8fe68adb5 100644 --- 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& A, - vector & lower_bounds, - vector & upper_bounds) { - vector column_scale_vector; - vector right_side_vector(A.column_count()); - settings().reps_in_scaler = 5; - scaler 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 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 index 4b6163df810..a60395ab014 100644 --- 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 #include #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 deleted file mode 100644 index fc95140982b..00000000000 --- a/src/math/lp/lp_solver.cpp +++ /dev/null @@ -1,55 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - - -Abstract: - - - -Author: - - Lev Nachmanson (levnach) - -Revision History: - - ---*/ -#include -#include "math/lp/lp_solver_def.h" -template void lp::lp_solver::add_constraint(lp::lp_relation, double, unsigned int); -template void lp::lp_solver::cleanup(); -template void lp::lp_solver::count_slacks_and_artificials(); -template void lp::lp_solver::fill_m_b(); -template void lp::lp_solver::fill_matrix_A_and_init_right_side(); -template void lp::lp_solver::flip_costs(); -template double lp::lp_solver::get_column_cost_value(unsigned int, lp::column_info*) const; -template int lp::lp_solver::get_column_index_by_name(std::string) const; -template double lp::lp_solver::get_column_value_with_core_solver(unsigned int, lp::lp_core_solver_base*) const; -template lp::column_info* lp::lp_solver::get_or_create_column_info(unsigned int); -template void lp::lp_solver::give_symbolic_name_to_column(std::string, unsigned int); -template void lp::lp_solver::print_statistics_on_A(std::ostream & out); -template bool lp::lp_solver::problem_is_empty(); -template void lp::lp_solver::scale(); -template void lp::lp_solver::set_scaled_cost(unsigned int); -template lp::lp_solver::~lp_solver(); -template void lp::lp_solver::add_constraint(lp::lp_relation, lp::mpq, unsigned int); -template void lp::lp_solver::cleanup(); -template void lp::lp_solver::count_slacks_and_artificials(); -template void lp::lp_solver::fill_m_b(); -template void lp::lp_solver::fill_matrix_A_and_init_right_side(); -template void lp::lp_solver::flip_costs(); -template lp::mpq lp::lp_solver::get_column_cost_value(unsigned int, lp::column_info*) const; -template int lp::lp_solver::get_column_index_by_name(std::string) const; -template lp::mpq lp::lp_solver::get_column_value_by_name(std::string) const; -template lp::mpq lp::lp_solver::get_column_value_with_core_solver(unsigned int, lp::lp_core_solver_base*) const; -template lp::column_info* lp::lp_solver::get_or_create_column_info(unsigned int); -template void lp::lp_solver::give_symbolic_name_to_column(std::string, unsigned int); -template void lp::lp_solver::print_statistics_on_A(std::ostream & out); -template bool lp::lp_solver::problem_is_empty(); -template void lp::lp_solver::scale(); -template void lp::lp_solver::set_scaled_cost(unsigned int); -template lp::lp_solver::~lp_solver(); -template double lp::lp_solver::get_column_value_by_name(std::string) const; diff --git a/src/math/lp/lp_solver.h b/src/math/lp/lp_solver.h deleted file mode 100644 index ab16a686fd6..00000000000 --- a/src/math/lp/lp_solver.h +++ /dev/null @@ -1,260 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - - -Abstract: - - - -Author: - - Lev Nachmanson (levnach) - -Revision History: - - ---*/ - -#pragma once -#include -#include -#include -#include "util/vector.h" -#include "math/lp/lp_settings.h" -#include "math/lp/column_info.h" -#include "math/lp/static_matrix.h" -#include "math/lp/lp_core_solver_base.h" -#include "math/lp/scaler.h" -#include "math/lp/bound_analyzer_on_row.h" -namespace lp { -enum lp_relation { - Less_or_equal, - Equal, - Greater_or_equal -}; - -template -struct lp_constraint { - X m_rs; // right side of the constraint - lp_relation m_relation; - lp_constraint() {} // empty constructor - lp_constraint(T rs, lp_relation relation): m_rs(rs), m_relation(relation) {} -}; - - -template -class lp_solver : public column_namer { - column_info * get_or_create_column_info(unsigned column); - -protected: - T get_column_cost_value(unsigned j, column_info * ci) const; -public: - unsigned m_total_iterations; - static_matrix* m_A; // this is the matrix of constraints - vector m_b; // the right side vector - unsigned m_first_stage_iterations; - unsigned m_second_stage_iterations; - std::unordered_map> m_constraints; - std::unordered_map*> m_map_from_var_index_to_column_info; - std::unordered_map > m_A_values; - std::unordered_map m_names_to_columns; // don't have to use it - std::unordered_map m_external_rows_to_core_solver_rows; - std::unordered_map m_core_solver_rows_to_external_rows; - std::unordered_map m_core_solver_columns_to_external_columns; - vector m_column_scale; - std::unordered_map m_name_map; - unsigned m_artificials; - unsigned m_slacks; - vector m_column_types; - vector m_costs; - vector m_x; - vector m_upper_bounds; - vector m_basis; - vector m_nbasis; - vector m_heading; - - - lp_status m_status; - - lp_settings m_settings; - lp_solver(): - m_A(nullptr), // this is the matrix of constraints - m_first_stage_iterations (0), - m_second_stage_iterations (0), - m_artificials (0), - m_slacks (0), - m_status(lp_status::UNKNOWN) - {} - - unsigned row_count() const { return this->m_A->row_count(); } - - void add_constraint(lp_relation relation, T right_side, unsigned row_index); - - void set_cost_for_column(unsigned column, T column_cost) { - get_or_create_column_info(column)->set_cost(column_cost); - } - std::string get_variable_name(unsigned j) const override; - - void set_row_column_coefficient(unsigned row, unsigned column, T const & val) { - m_A_values[row][column] = val; - } - // returns the current cost - virtual T get_current_cost() const = 0; - // do not have to call it - void give_symbolic_name_to_column(std::string name, unsigned column); - - virtual T get_column_value(unsigned column) const = 0; - - T get_column_value_by_name(std::string name) const; - - // returns -1 if not found - virtual int get_column_index_by_name(std::string name) const; - - void set_lower_bound(unsigned i, T bound) { - column_info *ci = get_or_create_column_info(i); - ci->set_lower_bound(bound); - } - - void set_upper_bound(unsigned i, T bound) { - column_info *ci = get_or_create_column_info(i); - ci->set_upper_bound(bound); - } - - void unset_lower_bound(unsigned i) { - get_or_create_column_info(i)->unset_lower_bound(); - } - - void unset_upper_bound(unsigned i) { - get_or_create_column_info(i)->unset_upper_bound(); - } - - void set_fixed_value(unsigned i, T val) { - column_info *ci = get_or_create_column_info(i); - ci->set_fixed_value(val); - } - - void unset_fixed_value(unsigned i) { - get_or_create_column_info(i)->unset_fixed(); - } - - lp_status get_status() const { - return m_status; - } - - void set_status(lp_status st) { - m_status = st; - } - - - ~lp_solver() override; - - void flip_costs(); - - virtual void find_maximal_solution() = 0; - void set_time_limit(unsigned time_limit_in_seconds) { - m_settings.time_limit = time_limit_in_seconds; - } - - -protected: - bool problem_is_empty(); - - void scale(); - - - void print_rows_scale_stats(std::ostream & out); - - void print_columns_scale_stats(std::ostream & out); - - void print_row_scale_stats(unsigned i, std::ostream & out); - - void print_column_scale_stats(unsigned j, std::ostream & out); - - void print_scale_stats(std::ostream & out); - - void get_max_abs_in_row(std::unordered_map & row_map); - - void pin_vars_down_on_row(std::unordered_map & row) { - pin_vars_on_row_with_sign(row, - numeric_traits::one()); - } - - void pin_vars_up_on_row(std::unordered_map & row) { - pin_vars_on_row_with_sign(row, numeric_traits::one()); - } - - void pin_vars_on_row_with_sign(std::unordered_map & row, T sign ); - - bool get_minimal_row_value(std::unordered_map & row, T & lower_bound); - - bool get_maximal_row_value(std::unordered_map & row, T & lower_bound); - - bool row_is_zero(std::unordered_map & row); - - bool row_e_is_obsolete(std::unordered_map & row, unsigned row_index); - - bool row_ge_is_obsolete(std::unordered_map & row, unsigned row_index); - - bool row_le_is_obsolete(std::unordered_map & row, unsigned row_index); - - // analyse possible max and min values that are derived from var boundaries - // Let us say that the we have a "ge" constraint, and the min value is equal to the rs. - // Then we know what values of the variables are. For each positive coeff of the row it has to be - // the low boundary of the var and for a negative - the upper. - - // this routing also pins the variables to the boundaries - bool row_is_obsolete(std::unordered_map & row, unsigned row_index ); - - void remove_fixed_or_zero_columns(); - - void remove_fixed_or_zero_columns_from_row(unsigned i, std::unordered_map & row); - - unsigned try_to_remove_some_rows(); - - void cleanup(); - - void map_external_rows_to_core_solver_rows(); - - void map_external_columns_to_core_solver_columns(); - - unsigned number_of_core_structurals() { - return static_cast(m_core_solver_columns_to_external_columns.size()); - } - - void restore_column_scales_to_one() { - for (unsigned i = 0; i < m_column_scale.size(); i++) m_column_scale[i] = numeric_traits::one(); - } - - void unscale(); - - void fill_A_from_A_values(); - - void fill_matrix_A_and_init_right_side(); - - void count_slacks_and_artificials(); - - void count_slacks_and_artificials_for_row(unsigned i); - - T lower_bound_shift_for_row(unsigned i); - - void fill_m_b(); - - T get_column_value_with_core_solver(unsigned column, lp_core_solver_base * core_solver) const; - void set_scaled_cost(unsigned j); - void print_statistics_on_A(std::ostream & out) { - out << "extended A[" << this->m_A->row_count() << "," << this->m_A->column_count() << "]" << std::endl; - } - -public: - lp_settings & settings() { return m_settings;} - void print_model(std::ostream & s) const { - s << "objective = " << get_current_cost() << std::endl; - s << "column values\n"; - for (auto & it : m_names_to_columns) { - s << it.first << " = " << get_column_value(it.second) << std::endl; - } - } -}; -} diff --git a/src/math/lp/lp_solver_def.h b/src/math/lp/lp_solver_def.h deleted file mode 100644 index 191832a2487..00000000000 --- a/src/math/lp/lp_solver_def.h +++ /dev/null @@ -1,571 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - - -Abstract: - - - -Author: - - Lev Nachmanson (levnach) - -Revision History: - - ---*/ -#pragma once - -#include -#include -#include "util/vector.h" -#include "math/lp/lp_solver.h" -namespace lp { -template column_info * lp_solver::get_or_create_column_info(unsigned column) { - auto it = m_map_from_var_index_to_column_info.find(column); - return (it == m_map_from_var_index_to_column_info.end())? (m_map_from_var_index_to_column_info[column] = new column_info()) : it->second; -} - -template -std::string lp_solver::get_variable_name(unsigned j) const { // j here is the core solver index - if (!m_settings.print_external_var_name()) - return std::string("j")+T_to_string(j); - auto it = this->m_core_solver_columns_to_external_columns.find(j); - if (it == this->m_core_solver_columns_to_external_columns.end()) - return std::string("x")+T_to_string(j); - unsigned external_j = it->second; - auto t = this->m_map_from_var_index_to_column_info.find(external_j); - if (t == this->m_map_from_var_index_to_column_info.end()) { - return std::string("x") +T_to_string(external_j); - } - return t->second->get_name(); -} - -template T lp_solver::get_column_cost_value(unsigned j, column_info * ci) const { - if (ci->is_fixed()) { - return ci->get_cost() * ci->get_fixed_value(); - } - return ci->get_cost() * get_column_value(j); -} -template void lp_solver::add_constraint(lp_relation relation, T right_side, unsigned row_index) { - lp_assert(m_constraints.find(row_index) == m_constraints.end()); - lp_constraint cs(right_side, relation); - m_constraints[row_index] = cs; -} - -template void lp_solver::give_symbolic_name_to_column(std::string name, unsigned column) { - auto it = m_map_from_var_index_to_column_info.find(column); - column_info *ci; - if (it == m_map_from_var_index_to_column_info.end()){ - m_map_from_var_index_to_column_info[column] = ci = new column_info; - } else { - ci = it->second; - } - ci->set_name(name); - m_names_to_columns[name] = column; -} - - -template T lp_solver::get_column_value_by_name(std::string name) const { - auto it = m_names_to_columns.find(name); - if (it == m_names_to_columns.end()) { - std::stringstream s; - s << "get_column_value_by_name " << name; - throw_exception(s.str()); - } - return get_column_value(it -> second); -} - -// returns -1 if not found -template int lp_solver::get_column_index_by_name(std::string name) const { - auto t = m_names_to_columns.find(name); - if (t == m_names_to_columns.end()) { - return -1; - } - return t->second; -} - - -template lp_solver::~lp_solver(){ - delete m_A; - for (auto t : m_map_from_var_index_to_column_info) { - delete t.second; - } -} - -template void lp_solver::flip_costs() { - for (auto t : m_map_from_var_index_to_column_info) { - column_info *ci = t.second; - ci->set_cost(-ci->get_cost()); - } -} - -template bool lp_solver::problem_is_empty() { - for (auto & c : m_A_values) - if (!c.second.empty()) - return false; - return true; -} - -template void lp_solver::scale() { - if (numeric_traits::precise() || m_settings.use_scaling == false) { - m_column_scale.clear(); - m_column_scale.resize(m_A->column_count(), one_of_type()); - return; - } - - T smin = T(m_settings.scaling_minimum); - T smax = T(m_settings.scaling_maximum); - - scaler scaler(m_b, *m_A, smin, smax, m_column_scale, this->m_settings); - if (!scaler.scale()) { - unscale(); - } -} - - -template void lp_solver::print_rows_scale_stats(std::ostream & out) { - out << "rows max" << std::endl; - for (unsigned i = 0; i < m_A->row_count(); i++) { - print_row_scale_stats(i, out); - } - out << std::endl; -} - -template void lp_solver::print_columns_scale_stats(std::ostream & out) { - out << "columns max" << std::endl; - for (unsigned i = 0; i < m_A->column_count(); i++) { - print_column_scale_stats(i, out); - } - out << std::endl; -} - -template void lp_solver::print_row_scale_stats(unsigned i, std::ostream & out) { - out << "(" << std::min(m_A->get_min_abs_in_row(i), abs(m_b[i])) << " "; - out << std::max(m_A->get_max_abs_in_row(i), abs(m_b[i])) << ")"; -} - -template void lp_solver::print_column_scale_stats(unsigned j, std::ostream & out) { - out << "(" << m_A->get_min_abs_in_row(j) << " "; - out << m_A->get_max_abs_in_column(j) << ")"; -} - -template void lp_solver::print_scale_stats(std::ostream & out) { - print_rows_scale_stats(out); - print_columns_scale_stats(out); -} - -template void lp_solver::get_max_abs_in_row(std::unordered_map & row_map) { - T ret = numeric_traits::zero(); - for (auto jp : row_map) { - T ac = numeric_traits::abs(jp->second); - if (ac > ret) { - ret = ac; - } - } - return ret; -} - -template void lp_solver::pin_vars_on_row_with_sign(std::unordered_map & row, T sign ) { - for (auto t : row) { - unsigned j = t.first; - column_info * ci = m_map_from_var_index_to_column_info[j]; - T a = t.second; - if (a * sign > numeric_traits::zero()) { - lp_assert(ci->upper_bound_is_set()); - ci->set_fixed_value(ci->get_upper_bound()); - } else { - lp_assert(ci->lower_bound_is_set()); - ci->set_fixed_value(ci->get_lower_bound()); - } - } -} - -template bool lp_solver::get_minimal_row_value(std::unordered_map & row, T & lower_bound) { - lower_bound = numeric_traits::zero(); - for (auto & t : row) { - T a = t.second; - column_info * ci = m_map_from_var_index_to_column_info[t.first]; - if (a > numeric_traits::zero()) { - if (ci->lower_bound_is_set()) { - lower_bound += ci->get_lower_bound() * a; - } else { - return false; - } - } else { - if (ci->upper_bound_is_set()) { - lower_bound += ci->get_upper_bound() * a; - } else { - return false; - } - } - } - return true; -} - -template bool lp_solver::get_maximal_row_value(std::unordered_map & row, T & lower_bound) { - lower_bound = numeric_traits::zero(); - for (auto & t : row) { - T a = t.second; - column_info * ci = m_map_from_var_index_to_column_info[t.first]; - if (a < numeric_traits::zero()) { - if (ci->lower_bound_is_set()) { - lower_bound += ci->get_lower_bound() * a; - } else { - return false; - } - } else { - if (ci->upper_bound_is_set()) { - lower_bound += ci->get_upper_bound() * a; - } else { - return false; - } - } - } - return true; -} - -template bool lp_solver::row_is_zero(std::unordered_map & row) { - for (auto & t : row) { - if (!is_zero(t.second)) - return false; - } - return true; -} - -template bool lp_solver::row_e_is_obsolete(std::unordered_map & row, unsigned row_index) { - T rs = m_constraints[row_index].m_rs; - if (row_is_zero(row)) { - if (!is_zero(rs)) - m_status = lp_status::INFEASIBLE; - return true; - } - - T lower_bound; - bool lb = get_minimal_row_value(row, lower_bound); - if (lb) { - T diff = lower_bound - rs; - if (!val_is_smaller_than_eps(diff, m_settings.refactor_tolerance)){ - // lower_bound > rs + m_settings.refactor_epsilon - m_status = lp_status::INFEASIBLE; - return true; - } - if (val_is_smaller_than_eps(-diff, m_settings.refactor_tolerance)){ - pin_vars_down_on_row(row); - return true; - } - } - - T upper_bound; - bool ub = get_maximal_row_value(row, upper_bound); - if (ub) { - T diff = rs - upper_bound; - if (!val_is_smaller_than_eps(diff, m_settings.refactor_tolerance)) { - // upper_bound < rs - m_settings.refactor_tolerance - m_status = lp_status::INFEASIBLE; - return true; - } - if (val_is_smaller_than_eps(-diff, m_settings.refactor_tolerance)){ - pin_vars_up_on_row(row); - return true; - } - } - - return false; -} - -template bool lp_solver::row_ge_is_obsolete(std::unordered_map & row, unsigned row_index) { - T rs = m_constraints[row_index].m_rs; - if (row_is_zero(row)) { - if (rs > zero_of_type()) - m_status = lp_status::INFEASIBLE; - return true; - } - - T upper_bound; - if (get_maximal_row_value(row, upper_bound)) { - T diff = rs - upper_bound; - if (!val_is_smaller_than_eps(diff, m_settings.refactor_tolerance)) { - // upper_bound < rs - m_settings.refactor_tolerance - m_status = lp_status::INFEASIBLE; - return true; - } - if (val_is_smaller_than_eps(-diff, m_settings.refactor_tolerance)){ - pin_vars_up_on_row(row); - return true; - } - } - - return false; -} - -template bool lp_solver::row_le_is_obsolete(std::unordered_map & row, unsigned row_index) { - T lower_bound; - T rs = m_constraints[row_index].m_rs; - if (row_is_zero(row)) { - if (rs < zero_of_type()) - m_status = lp_status::INFEASIBLE; - return true; - } - - if (get_minimal_row_value(row, lower_bound)) { - T diff = lower_bound - rs; - if (!val_is_smaller_than_eps(diff, m_settings.refactor_tolerance)){ - // lower_bound > rs + m_settings.refactor_tolerance - m_status = lp_status::INFEASIBLE; - return true; - } - if (val_is_smaller_than_eps(-diff, m_settings.refactor_tolerance)){ - pin_vars_down_on_row(row); - return true; - } - } - - return false; -} - -// analyse possible max and min values that are derived from var boundaries -// Let us say that the we have a "ge" constraint, and the min value is equal to the rs. -// Then we know what values of the variables are. For each positive coeff of the row it has to be -// the low boundary of the var and for a negative - the upper. - -// this routing also pins the variables to the boundaries -template bool lp_solver::row_is_obsolete(std::unordered_map & row, unsigned row_index ) { - auto & constraint = m_constraints[row_index]; - switch (constraint.m_relation) { - case lp_relation::Equal: - return row_e_is_obsolete(row, row_index); - - case lp_relation::Greater_or_equal: - return row_ge_is_obsolete(row, row_index); - - case lp_relation::Less_or_equal: - return row_le_is_obsolete(row, row_index); - } - lp_unreachable(); - return false; // it is unreachable -} - -template void lp_solver::remove_fixed_or_zero_columns() { - for (auto & i_row : m_A_values) { - remove_fixed_or_zero_columns_from_row(i_row.first, i_row.second); - } -} - -template void lp_solver::remove_fixed_or_zero_columns_from_row(unsigned i, std::unordered_map & row) { - auto & constraint = m_constraints[i]; - vector removed; - for (auto & col : row) { - unsigned j = col.first; - lp_assert(m_map_from_var_index_to_column_info.find(j) != m_map_from_var_index_to_column_info.end()); - column_info * ci = m_map_from_var_index_to_column_info[j]; - if (ci->is_fixed()) { - removed.push_back(j); - T aj = col.second; - constraint.m_rs -= aj * ci->get_fixed_value(); - } else { - if (numeric_traits::is_zero(col.second)){ - removed.push_back(j); - } - } - } - - for (auto j : removed) { - row.erase(j); - } -} - -template unsigned lp_solver::try_to_remove_some_rows() { - vector rows_to_delete; - for (auto & t : m_A_values) { - if (row_is_obsolete(t.second, t.first)) { - rows_to_delete.push_back(t.first); - } - - if (m_status == lp_status::INFEASIBLE) { - return 0; - } - } - if (!rows_to_delete.empty()) { - for (unsigned k : rows_to_delete) { - m_A_values.erase(k); - } - } - remove_fixed_or_zero_columns(); - return static_cast(rows_to_delete.size()); -} - -template void lp_solver::cleanup() { - int n = 0; // number of deleted rows - int d; - while ((d = try_to_remove_some_rows()) > 0) - n += d; - - if (n == 1) { - LP_OUT(m_settings, "deleted one row" << std::endl); - } else if (n) { - LP_OUT(m_settings, "deleted " << n << " rows" << std::endl); - } -} - -template void lp_solver::map_external_rows_to_core_solver_rows() { - unsigned size = 0; - for (auto & row : m_A_values) { - m_external_rows_to_core_solver_rows[row.first] = size; - m_core_solver_rows_to_external_rows[size] = row.first; - size++; - } -} - -template void lp_solver::map_external_columns_to_core_solver_columns() { - unsigned size = 0; - for (auto & row : m_A_values) { - for (auto & col : row.second) { - if (col.second == numeric_traits::zero() || m_map_from_var_index_to_column_info[col.first]->is_fixed()) { - throw_exception("found fixed column"); - } - unsigned j = col.first; - auto column_info_it = m_map_from_var_index_to_column_info.find(j); - lp_assert(column_info_it != m_map_from_var_index_to_column_info.end()); - - auto j_column = column_info_it->second->get_column_index(); - if (!is_valid(j_column)) { // j is a newcomer - m_map_from_var_index_to_column_info[j]->set_column_index(size); - m_core_solver_columns_to_external_columns[size++] = j; - } - } - } -} - -template void lp_solver::unscale() { - delete m_A; - m_A = nullptr; - fill_A_from_A_values(); - restore_column_scales_to_one(); - fill_m_b(); -} - -template void lp_solver::fill_A_from_A_values() { - m_A = new static_matrix(static_cast(m_A_values.size()), number_of_core_structurals()); - for (auto & t : m_A_values) { - auto row_it = m_external_rows_to_core_solver_rows.find(t.first); - lp_assert(row_it != m_external_rows_to_core_solver_rows.end()); - unsigned row = row_it->second; - for (auto k : t.second) { - auto column_info_it = m_map_from_var_index_to_column_info.find(k.first); - lp_assert(column_info_it != m_map_from_var_index_to_column_info.end()); - column_info *ci = column_info_it->second; - unsigned col = ci->get_column_index(); - lp_assert(is_valid(col)); - bool col_is_flipped = m_map_from_var_index_to_column_info[k.first]->is_flipped(); - if (!col_is_flipped) { - (*m_A)(row, col) = k.second; - } else { - (*m_A)(row, col) = - k.second; - } - } - } -} - -template void lp_solver::fill_matrix_A_and_init_right_side() { - map_external_rows_to_core_solver_rows(); - map_external_columns_to_core_solver_columns(); - lp_assert(m_A == nullptr); - fill_A_from_A_values(); - m_b.resize(m_A->row_count()); -} - -template void lp_solver::count_slacks_and_artificials() { - for (int i = row_count() - 1; i >= 0; i--) { - count_slacks_and_artificials_for_row(i); - } -} - -template void lp_solver::count_slacks_and_artificials_for_row(unsigned i) { - lp_assert(this->m_constraints.find(this->m_core_solver_rows_to_external_rows[i]) != this->m_constraints.end()); - auto & constraint = this->m_constraints[this->m_core_solver_rows_to_external_rows[i]]; - switch (constraint.m_relation) { - case Equal: - m_artificials++; - break; - case Greater_or_equal: - m_slacks++; - if (this->m_b[i] > 0) { - m_artificials++; - } - break; - case Less_or_equal: - m_slacks++; - if (this->m_b[i] < 0) { - m_artificials++; - } - break; - } -} - -template T lp_solver::lower_bound_shift_for_row(unsigned i) { - T ret = numeric_traits::zero(); - - auto row = this->m_A_values.find(i); - if (row == this->m_A_values.end()) { - throw_exception("cannot find row"); - } - for (auto col : row->second) { - ret += col.second * this->m_map_from_var_index_to_column_info[col.first]->get_shift(); - } - return ret; -} - -template void lp_solver::fill_m_b() { - for (int i = this->row_count() - 1; i >= 0; i--) { - lp_assert(this->m_constraints.find(this->m_core_solver_rows_to_external_rows[i]) != this->m_constraints.end()); - unsigned external_i = this->m_core_solver_rows_to_external_rows[i]; - auto & constraint = this->m_constraints[external_i]; - this->m_b[i] = constraint.m_rs - lower_bound_shift_for_row(external_i); - } -} - -template T lp_solver::get_column_value_with_core_solver(unsigned column, lp_core_solver_base * core_solver) const { - auto cit = this->m_map_from_var_index_to_column_info.find(column); - if (cit == this->m_map_from_var_index_to_column_info.end()) { - return numeric_traits::zero(); - } - - column_info * ci = cit->second; - - if (ci->is_fixed()) { - return ci->get_fixed_value(); - } - - unsigned cj = ci->get_column_index(); - if (cj != static_cast(-1)) { - T v = core_solver->get_var_value(cj) * this->m_column_scale[cj]; - if (ci->is_free()) { - return v; - } - if (!ci->is_flipped()) { - return v + ci->get_lower_bound(); - } - - // the flipped case when there is only upper bound - return -v + ci->get_upper_bound(); // - } - - return numeric_traits::zero(); // returns zero for out of boundary columns -} - -template void lp_solver::set_scaled_cost(unsigned j) { - // grab original costs but modify it with the column scales - lp_assert(j < this->m_column_scale.size()); - column_info * ci = this->m_map_from_var_index_to_column_info[this->m_core_solver_columns_to_external_columns[j]]; - T cost = ci->get_cost(); - if (ci->is_flipped()){ - cost *= T(-1); - } - lp_assert(ci->is_fixed() == false); - this->m_costs[j] = cost * this->m_column_scale[j]; -} -} diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h index 3152485ec2e..68d5f802592 100644 --- a/src/sat/smt/arith_solver.h +++ b/src/sat/smt/arith_solver.h @@ -19,7 +19,7 @@ Module Name: #include "util/obj_pair_set.h" #include "ast/ast_trail.h" #include "ast/arith_decl_plugin.h" -#include "math/lp/lp_solver.h" + #include "math/lp/indexed_value.h" #include "math/lp/lar_solver.h" #include "math/lp/nla_solver.h" diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index a654366a2ca..2aa988282d2 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -19,7 +19,6 @@ --*/ #include "util/stopwatch.h" -#include "math/lp/lp_solver.h" #include "math/lp/indexed_value.h" #include "math/lp/lar_solver.h" #include "math/lp/nla_solver.h"