diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index a791bfb05..9a5bc5032 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -139,7 +139,41 @@ namespace lp { return solver.get_status() == lp_status::INFEASIBLE; } } - }; + void require_nbasis_sort() { m_mpq_lar_core_solver.m_r_solver.m_nbasis_sort_counter = 0; } + void register_in_fixed_var_table(unsigned j, unsigned& equal_to_j) { + SASSERT(lra.column_is_fixed(j)); + equal_to_j = null_lpvar; + const impq& bound = lra.get_lower_bound(j); + if (!bound.y.is_zero()) + return; + + const mpq& key = bound.x; + unsigned k; + bool j_is_int = lra.column_is_int(j); + if (j_is_int) { + if (!m_fixed_var_table_int.find(key, k)) { + m_fixed_var_table_int.insert(key, j); + return; + } + } + else { // j is not integral column + if (!m_fixed_var_table_real.find(key, k)) { + m_fixed_var_table_real.insert(key, j); + return; + } + } + + CTRACE("arith", !lra.column_is_fixed(k), lra.print_terms(tout);); + // SASSERT(column_is_fixed(k)); + if (j != k && lra.column_is_fixed(k)) { + SASSERT(lra.column_is_int(j) == lra.column_is_int(k)); + equal_to_j = k; + TRACE("lar_solver", tout << "found equal column k = " << k << + ", external = " << equal_to_j << "\n";); + } + } + + }; // imp unsigned_vector& lar_solver::row_bounds_to_replay() { return m_imp->m_row_bounds_to_replay; } trail_stack& lar_solver::trail() { return m_imp->m_trail; } @@ -211,8 +245,6 @@ namespace lp { indexed_uint_set& lar_solver::basic_columns_with_changed_cost() { return m_imp->m_basic_columns_with_changed_cost; } - void lar_solver::require_nbasis_sort() { m_imp->m_mpq_lar_core_solver.m_r_solver.m_nbasis_sort_counter = 0; } - mpq lar_solver::bound_span_x(lpvar j) const { SASSERT(column_has_upper_bound(j) && column_has_lower_bound(j)); return get_upper_bound(j).x - get_lower_bound(j).x; @@ -533,7 +565,7 @@ namespace lp { m_imp->m_usage_in_terms.pop(k); m_imp->m_dependencies.pop_scope(k); // init the nbasis sorting - require_nbasis_sort(); + m_imp->require_nbasis_sort(); set_status(lp_status::UNKNOWN); } @@ -759,7 +791,7 @@ namespace lp { TRACE("lar_solver", print_term(term, tout << "maximize: ") << "\n" << constraints() << ", strategy = " << (int)settings().simplex_strategy() << "\n";); if (settings().simplex_strategy() != simplex_strategy_enum::tableau_costs) - require_nbasis_sort(); + m_imp->require_nbasis_sort(); flet f(settings().simplex_strategy(), simplex_strategy_enum::tableau_costs); prepare_costs_for_r_solver(term); ret = maximize_term_on_tableau(term, term_max); @@ -1962,7 +1994,7 @@ namespace lp { else { get_core_solver().m_r_heading.push_back(-static_cast(get_core_solver().m_r_nbasis.size()) - 1); get_core_solver().m_r_nbasis.push_back(j); - require_nbasis_sort(); + m_imp->require_nbasis_sort(); } } @@ -2099,38 +2131,6 @@ namespace lp { remove_non_fixed_from_table(m_imp->m_fixed_var_table_real); } - void lar_solver::register_in_fixed_var_table(unsigned j, unsigned& equal_to_j) { - SASSERT(column_is_fixed(j)); - equal_to_j = null_lpvar; - const impq& bound = get_lower_bound(j); - if (!bound.y.is_zero()) - return; - - const mpq& key = bound.x; - unsigned k; - bool j_is_int = column_is_int(j); - if (j_is_int) { - if (!m_imp->m_fixed_var_table_int.find(key, k)) { - m_imp->m_fixed_var_table_int.insert(key, j); - return; - } - } - else { // j is not integral column - if (!m_imp->m_fixed_var_table_real.find(key, k)) { - m_imp->m_fixed_var_table_real.insert(key, j); - return; - } - } - - CTRACE("arith", !column_is_fixed(k), print_terms(tout);); - // SASSERT(column_is_fixed(k)); - if (j != k && column_is_fixed(k)) { - SASSERT(column_is_int(j) == column_is_int(k)); - equal_to_j = k; - TRACE("lar_solver", tout << "found equal column k = " << k << - ", external = " << equal_to_j << "\n";); - } - } void lar_solver::activate_check_on_equal(constraint_index ci, unsigned& equal_column) { auto const& c = m_imp->m_constraints[ci]; @@ -2318,7 +2318,7 @@ namespace lp { update_column_type_and_bound(j, right_side, constr_index); equal_to_j = null_lpvar; if (column_is_fixed(j)) { - register_in_fixed_var_table(j, equal_to_j); + m_imp->register_in_fixed_var_table(j, equal_to_j); } } diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 7ba2696c3..db27fe8eb 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -54,7 +54,6 @@ class lar_solver : public column_namer { ////////////////// methods //////////////////////////////// - static bool valid_index(unsigned j) { return static_cast(j) >= 0; } bool row_has_a_big_num(unsigned i) const; // init region void register_new_external_var(unsigned ext_v, bool is_int); @@ -95,16 +94,14 @@ class lar_solver : public column_namer { public: bool validate_blocker() const { return m_validate_blocker; } bool & validate_blocker() { return m_validate_blocker; } - void update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); + void update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); private: - void require_nbasis_sort(); void update_column_type_and_bound_with_ub(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); void update_column_type_and_bound_with_no_ub(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); void update_bound_with_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); void update_bound_with_no_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); void update_bound_with_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); void update_bound_with_no_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); - void register_in_fixed_var_table(unsigned, unsigned&); void remove_non_fixed_from_fixed_var_table(); constraint_index add_var_bound_on_constraint_for_term(lpvar j, lconstraint_kind kind, const mpq& right_side); void set_crossed_bounds_column_and_deps(unsigned j, bool lower_bound, u_dependency* dep);