diff --git a/src/math/lp/lar_core_solver.h b/src/math/lp/lar_core_solver.h index 59929e34f52..4aa62f0df09 100644 --- a/src/math/lp/lar_core_solver.h +++ b/src/math/lp/lar_core_solver.h @@ -14,7 +14,6 @@ Copyright (c) 2017 Microsoft Corporation #include "math/lp/indexed_vector.h" #include "math/lp/lp_primal_core_solver.h" #include "math/lp/stacked_vector.h" -#include "math/lp/lar_solution_signature.h" #include "util/stacked_value.h" namespace lp { diff --git a/src/math/lp/lar_core_solver_def.h b/src/math/lp/lar_core_solver_def.h index 2e205291e6f..e22d77c1b30 100644 --- a/src/math/lp/lar_core_solver_def.h +++ b/src/math/lp/lar_core_solver_def.h @@ -14,7 +14,6 @@ Revision History: #include #include "util/vector.h" #include "math/lp/lar_core_solver.h" -#include "math/lp/lar_solution_signature.h" namespace lp { lar_core_solver::lar_core_solver( lp_settings & settings, diff --git a/src/math/lp/lar_solution_signature.h b/src/math/lp/lar_solution_signature.h deleted file mode 100644 index 5b8bfae48aa..00000000000 --- a/src/math/lp/lar_solution_signature.h +++ /dev/null @@ -1,28 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - - -Abstract: - - - -Author: - - Lev Nachmanson (levnach) - -Revision History: - - ---*/ - -#pragma once -#include "util/vector.h" -#include "util/debug.h" -#include "math/lp/lp_settings.h" -#include -namespace lp { -typedef std::unordered_map lar_solution_signature; -} diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 952f2ad43e0..1c9f5461beb 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -221,9 +221,6 @@ namespace lp { evidence.add_pair(ul.lower_bound_witness(), -numeric_traits::one()); } - - unsigned lar_solver::get_total_iterations() const { return m_mpq_lar_core_solver.m_r_solver.total_iterations(); } - void lar_solver::push() { m_simplex_strategy = m_settings.simplex_strategy(); m_simplex_strategy.push(); @@ -761,20 +758,6 @@ namespace lp { return r; } - bool lar_solver::x_is_correct() const { - if (m_mpq_lar_core_solver.m_r_x.size() != A_r().column_count()) { - return false; - } - for (unsigned i = 0; i < A_r().row_count(); i++) { - numeric_pair delta = A_r().dot_product_with_row(i, m_mpq_lar_core_solver.m_r_x); - if (!delta.is_zero()) { - return false; - } - } - return true;; - - } - bool lar_solver::var_is_registered(var_index vj) const { if (tv::is_term(vj)) { return tv::unmask_term(vj) < m_terms.size(); @@ -824,28 +807,6 @@ namespace lp { return false; // it is unreachable } - bool lar_solver::the_relations_are_of_same_type(const vector>& evidence, lconstraint_kind& the_kind_of_sum) const { - unsigned n_of_G = 0, n_of_L = 0; - bool strict = false; - for (auto& it : evidence) { - mpq coeff = it.first; - constraint_index con_ind = it.second; - lconstraint_kind kind = coeff.is_pos() ? - m_constraints[con_ind].kind() : - flip_kind(m_constraints[con_ind].kind()); - if (kind == GT || kind == LT) - strict = true; - if (kind == GE || kind == GT) - n_of_G++; - else if (kind == LE || kind == LT) - n_of_L++; - } - the_kind_of_sum = n_of_G ? GE : (n_of_L ? LE : EQ); - if (strict) - the_kind_of_sum = static_cast((static_cast(the_kind_of_sum) / 2)); - - return n_of_G == 0 || n_of_L == 0; - } void lar_solver::register_in_map(std::unordered_map& coeffs, const lar_base_constraint& cn, const mpq& a) { for (auto& it : cn.coeffs()) { @@ -1227,12 +1188,6 @@ namespace lp { insert_row_with_changed_bounds(r.var()); } - - - void lar_solver::pivot_fixed_vars_from_basis() { - m_mpq_lar_core_solver.m_r_solver.pivot_fixed_vars_from_basis(); - } - void lar_solver::pop() { pop(1); } diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 5c77c679a47..955710b3c52 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -212,11 +212,9 @@ class lar_solver : public column_namer { void update_x_and_inf_costs_for_columns_with_changed_bounds_tableau(); void solve_with_core_solver(); numeric_pair get_basic_var_value_from_row(unsigned i); - bool x_is_correct() const; bool all_constrained_variables_are_registered(const vector>& left_side); bool all_constraints_hold() const; bool constraint_holds(const lar_base_constraint & constr, std::unordered_map & var_map) const; - bool the_relations_are_of_same_type(const vector> & evidence, lconstraint_kind & the_kind_of_sum) const; static void register_in_map(std::unordered_map & coeffs, const lar_base_constraint & cn, const mpq & a); static void register_monoid_in_map(std::unordered_map & coeffs, const mpq & a, unsigned j); bool the_left_sides_sum_to_zero(const vector> & evidence) const; @@ -229,7 +227,6 @@ class lar_solver : public column_namer { int inf_sign) const; mpq get_left_side_val(const lar_base_constraint & cns, const std::unordered_map & var_map) const; void fill_var_set_for_random_update(unsigned sz, var_index const * vars, vector& column_list); - void pivot_fixed_vars_from_basis(); bool column_represents_row_in_tableau(unsigned j); void make_sure_that_the_bottom_right_elem_not_zero_in_tableau(unsigned i, unsigned j); void remove_last_row_and_column_from_tableau(unsigned j); @@ -264,10 +261,7 @@ class lar_solver : public column_namer { return m_fixed_var_table_int; } - map, default_eq>& fixed_var_table_int() { - return m_fixed_var_table_int; - } - + const map, default_eq>& fixed_var_table_real() const { return m_fixed_var_table_real; } @@ -293,9 +287,7 @@ class lar_solver : public column_namer { inline void set_column_value_test(unsigned j, const impq& v) { set_column_value(j, v); } - - unsigned get_total_iterations() const; - + var_index add_named_var(unsigned ext_j, bool is_integer, const std::string&); lp_status maximize_term(unsigned j_or_term, impq &term_max); diff --git a/src/math/lp/lp_core_solver_base.cpp b/src/math/lp/lp_core_solver_base.cpp index ccd6bf41927..61eae344f6c 100644 --- a/src/math/lp/lp_core_solver_base.cpp +++ b/src/math/lp/lp_core_solver_base.cpp @@ -23,9 +23,6 @@ Revision History: #include "util/vector.h" #include #include "math/lp/lp_core_solver_base_def.h" -template lp::non_basic_column_value_position lp::lp_core_solver_base >::get_non_basic_column_value_position(unsigned int) const; -template lp::non_basic_column_value_position lp::lp_core_solver_base::get_non_basic_column_value_position(unsigned int) const; - template bool lp::lp_core_solver_base >::print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over(char const*, std::ostream &); template bool lp::lp_core_solver_base::basis_heading_is_correct() const ; template bool lp::lp_core_solver_base::column_is_dual_feasible(unsigned int) const; @@ -61,7 +58,6 @@ template std::string lp::lp_core_solver_base template void lp::lp_core_solver_base >::pretty_print(std::ostream & out); template bool lp::lp_core_solver_base::calc_current_x_is_feasible_include_non_basis(void)const; template bool lp::lp_core_solver_base >::calc_current_x_is_feasible_include_non_basis() const; -template void lp::lp_core_solver_base >::pivot_fixed_vars_from_basis(); template bool lp::lp_core_solver_base::column_is_feasible(unsigned int) const; // template void lp::lp_core_solver_base >::print_linear_combination_of_column_indices(vector, std::allocator > > const&, std::ostream&) const; template bool lp::lp_core_solver_base >::column_is_feasible(unsigned int) const; diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h index 9fb4d4333cd..2e751330b69 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -383,11 +383,6 @@ class lp_core_solver_base { } - - - non_basic_column_value_position get_non_basic_column_value_position(unsigned j) const; - - void pivot_fixed_vars_from_basis(); bool remove_from_basis(unsigned j); bool remove_from_basis(unsigned j, const impq&); bool pivot_column_general(unsigned j, unsigned j_basic, indexed_vector & w); diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h index 2d729656724..a1255ade3e2 100644 --- a/src/math/lp/lp_core_solver_base_def.h +++ b/src/math/lp/lp_core_solver_base_def.h @@ -423,29 +423,6 @@ column_name(unsigned column) const { return m_column_names.get_variable_name(column); } -template non_basic_column_value_position lp_core_solver_base:: -get_non_basic_column_value_position(unsigned j) const { - switch (m_column_types[j]) { - case column_type::fixed: - return x_is_at_lower_bound(j)? at_fixed : not_at_bound; - case column_type::free_column: - return free_of_bounds; - case column_type::boxed: - return x_is_at_lower_bound(j)? at_lower_bound :( - x_is_at_upper_bound(j)? at_upper_bound: - not_at_bound - ); - case column_type::lower_bound: - return x_is_at_lower_bound(j)? at_lower_bound : not_at_bound; - case column_type::upper_bound: - return x_is_at_upper_bound(j)? at_upper_bound : not_at_bound; - default: - lp_unreachable(); - } - lp_unreachable(); - return at_lower_bound; -} - template void lp_core_solver_base::transpose_rows_tableau(unsigned i, unsigned j) { transpose_basis(i, j); m_A.transpose_rows(i, j); @@ -463,27 +440,6 @@ template bool lp_core_solver_base::pivot_column_g return true; } -template void lp_core_solver_base::pivot_fixed_vars_from_basis() { - // run over basis and non-basis at the same time - indexed_vector w(m_basis.size()); // the buffer - unsigned i = 0; // points to basis - for (; i < m_basis.size(); i++) { - unsigned basic_j = m_basis[i]; - - if (get_column_type(basic_j) != column_type::fixed) continue; - T a; - unsigned j; - for (auto &c : m_A.m_rows[i]) { - j = c.var(); - if (j == basic_j) - continue; - if (get_column_type(j) != column_type::fixed) { - if (pivot_column_general(j, basic_j, w)) - break; - } - } - } -} template bool lp_core_solver_base::remove_from_basis(unsigned basic_j) { indexed_vector w(m_basis.size()); // the buffer diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 314930fc175..9a38fd582cb 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -90,8 +90,6 @@ inline std::ostream& operator<<(std::ostream& out, lp_status status) { lp_status lp_status_from_string(std::string status); -enum non_basic_column_value_position { at_lower_bound, at_upper_bound, at_fixed, free_of_bounds, not_at_bound }; - class lp_resource_limit { public: