diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 34666e040..b4d703218 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -176,174 +176,7 @@ namespace lp { return; } - lia_move int_solver::patcher::patch_nbasic_columns() { - remove_fixed_vars_from_base(); - lia.settings().stats().m_patches++; - lp_assert(lia.is_feasible()); - m_patch_success = 0; - m_patch_fail = 0; - m_num_ones = 0; - m_num_divides = 0; - //unsigned non_int_before = count_non_int(); - unsigned num = lra.A_r().column_count(); - for (unsigned v = 0; v < num; v++) { - if (lia.is_base(v)) - continue; - patch_nbasic_column(v); - } - unsigned num_fixed = 0; - for (unsigned v = 0; v < num; v++) - if (lia.is_fixed(v)) - ++num_fixed; - - lp_assert(lia.is_feasible()); - //verbose_stream() << "patch " << m_patch_success << " fails " << m_patch_fail << " ones " << m_num_ones << " divides " << m_num_divides << " num fixed " << num_fixed << "\n"; - //lra.display(verbose_stream()); - //exit(0); - //unsigned non_int_after = count_non_int(); - - // verbose_stream() << non_int_before << " -> " << non_int_after << "\n"; - if (!lia.has_inf_int()) { - lia.settings().stats().m_patches_success++; - return lia_move::sat; - } - return lia_move::undef; - } - -void int_solver::patcher::patch_nbasic_column(unsigned j) { - impq & val = lrac.m_r_x[j]; - bool inf_l, inf_u; - impq l, u; - mpq m; - bool has_free = lia.get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m); - if (!has_free) - return; - bool m_is_one = m.is_one(); - bool val_is_int = lia.value_is_int(j); - -#if 0 -const auto & A = lra.A_r(); -#endif - // check whether value of j is already a multiple of m. - if (val_is_int && (m_is_one || (val.x / m).is_int())) { - if (m_is_one) - ++m_num_ones; - else - ++m_num_divides; -#if 0 - for (auto c : A.column(j)) { - unsigned row_index = c.var(); - unsigned i = lrac.m_r_basis[row_index]; - if (!lia.get_value(i).is_int() || - (lia.has_lower(i) && lia.get_value(i) < lra.get_lower_bound(i)) || - (lia.has_upper(i) && lia.get_value(i) > lra.get_upper_bound(i))) { - verbose_stream() << "skip " << j << " " << m << ": "; - lia.display_row(verbose_stream(), A.m_rows[row_index]); - verbose_stream() << "\n"; - } - } -#endif - return; - } - -#if 0 - if (!m_is_one) { - // lia.display_column(verbose_stream(), j); - for (auto c : A.column(j)) { - continue; - unsigned row_index = c.var(); - lia.display_row(verbose_stream(), A.m_rows[row_index]); - verbose_stream() << "\n"; - } - } -#endif - - TRACE("patch_int", - tout << "TARGET j" << j << " -> ["; - if (inf_l) tout << "-oo"; else tout << l; - tout << ", "; - if (inf_u) tout << "oo"; else tout << u; - tout << "]"; - tout << ", m: " << m << ", val: " << val << ", is_int: " << lra.column_is_int(j) << "\n";); - -#if 0 - verbose_stream() << "path " << m << " "; - if (!inf_l) verbose_stream() << "infl " << l.x << " "; - if (!inf_u) verbose_stream() << "infu " << u.x << " "; - verbose_stream() << "\n"; - if (m.is_big() || (!inf_l && l.x.is_big()) || (!inf_u && u.x.is_big())) { - return; - } -#endif - -#if 0 - verbose_stream() << "TARGET v" << j << " -> ["; - if (inf_l) verbose_stream() << "-oo"; else verbose_stream() << ceil(l.x) << " " << l << "\n"; - verbose_stream() << ", "; - if (inf_u) verbose_stream() << "oo"; else verbose_stream() << floor(u.x) << " " << u << "\n"; - verbose_stream() << "]"; - verbose_stream() << ", m: " << m << ", val: " << val << ", is_int: " << lra.column_is_int(j) << "\n"; -#endif - -#if 0 - if (!inf_l) - l = impq(ceil(l)); - if (!inf_u) - u = impq(floor(u)); -#endif - - if (!inf_l) { - l = impq(m_is_one ? ceil(l) : m * ceil(l / m)); - if (inf_u || l <= u) { - TRACE("patch_int", tout << "patching with l: " << l << '\n';); - lra.set_value_for_nbasic_column(j, l); - } - else { - //verbose_stream() << "fail: " << j << " " << m << "\n"; - ++m_patch_fail; - TRACE("patch_int", tout << "not patching " << l << "\n";); -#if 0 - verbose_stream() << "not patched\n"; - for (auto c : A.column(j)) { - unsigned row_index = c.var(); - unsigned i = lrac.m_r_basis[row_index]; - if (!lia.get_value(i).is_int() || - (lia.has_lower(i) && lia.get_value(i) < lra.get_lower_bound(i)) || - (lia.has_upper(i) && lia.get_value(i) > lra.get_upper_bound(i))) { - lia.display_row(verbose_stream(), A.m_rows[row_index]); - verbose_stream() << "\n"; - } - } -#endif - return; - } - } - else if (!inf_u) { - u = impq(m_is_one ? floor(u) : m * floor(u / m)); - lra.set_value_for_nbasic_column(j, u); - TRACE("patch_int", tout << "patching with u: " << u << '\n';); - } - else { - lra.set_value_for_nbasic_column(j, impq(0)); - TRACE("patch_int", tout << "patching with 0\n";); - } - ++m_patch_success; -#if 0 - verbose_stream() << "patched " << j << "\n"; - for (auto c : A.column(j)) { - unsigned row_index = c.var(); - unsigned i = lrac.m_r_basis[row_index]; - if (!lia.get_value(i).is_int() || - (lia.has_lower(i) && lia.get_value(i) < lra.get_lower_bound(i)) || - (lia.has_upper(i) && lia.get_value(i) > lra.get_upper_bound(i))) { - lia.display_row(verbose_stream(), A.m_rows[row_index]); - verbose_stream() << "\n"; - } - } -#endif - -} int_solver::int_solver(lar_solver& lar_slv) : lra(lar_slv), diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h index b9d09081a..56237a5b8 100644 --- a/src/math/lp/int_solver.h +++ b/src/math/lp/int_solver.h @@ -52,15 +52,13 @@ class int_solver { patcher(int_solver& lia); bool should_apply() const { return true; } lia_move operator()() { return patch_basic_columns(); } - void patch_nbasic_column(unsigned j); bool patch_basic_column_on_row_cell(unsigned v, row_cell const& c); void patch_basic_column(unsigned j); bool try_patch_column(unsigned v, unsigned j, mpq const& delta); unsigned count_non_int(); private: - void remove_fixed_vars_from_base(); - lia_move patch_nbasic_columns(); lia_move patch_basic_columns(); + void remove_fixed_vars_from_base(); }; lar_solver& lra; @@ -134,7 +132,6 @@ public: bool all_columns_are_bounded() const; void find_feasible_solution(); lia_move hnf_cut(); - void patch_nbasic_column(unsigned j) { m_patcher.patch_nbasic_column(j); } int select_int_infeasible_var(); diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index d5d2825bf..8a4fc3707 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -534,7 +534,6 @@ namespace lp { return lp_status::FEASIBLE; // it should not happen } } - m_int_solver->patch_nbasic_column(j); if (!column_value_is_integer(j)) { term_max = prev_value; m_mpq_lar_core_solver.m_r_x = backup; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index afedc460a..87de2d9e2 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1638,9 +1638,6 @@ public: return FC_DONE; return FC_GIVEUP; } - - unsigned m_final_check_idx = 0; - distribution m_dist { 0 }; final_check_status final_check_eh() { if (propagate_core())