From 5964969f298d1c2cca297bdb5bfd14e9cdd7a09f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 9 Feb 2020 08:38:07 -0800 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/math/lp/gomory.cpp | 41 ++++++++++++++++++------------------ src/math/lp/int_gcd_test.cpp | 12 +++++++++-- src/math/lp/int_gcd_test.h | 11 +++++++++- src/math/lp/int_solver.cpp | 6 ------ src/math/lp/int_solver.h | 24 +-------------------- 5 files changed, 41 insertions(+), 53 deletions(-) diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index 7cc8e8f32..44f801ae8 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -31,7 +31,7 @@ class create_cut { explanation* m_ex; // the conflict explanation unsigned m_inf_col; // a basis column which has to be an integer but has a non integral value const row_strip& m_row; - const int_solver& m_int_solver; + const int_solver& lia; mpq m_lcm_den; mpq m_f; mpq m_one_minus_f; @@ -42,18 +42,18 @@ class create_cut { #endif struct found_big {}; - const impq & get_value(unsigned j) const { return m_int_solver.get_value(j); } - bool is_real(unsigned j) const { return m_int_solver.is_real(j); } - bool at_lower(unsigned j) const { return m_int_solver.at_lower(j); } - bool at_upper(unsigned j) const { return m_int_solver.at_upper(j); } - const impq & lower_bound(unsigned j) const { return m_int_solver.lower_bound(j); } - const impq & upper_bound(unsigned j) const { return m_int_solver.upper_bound(j); } - constraint_index column_lower_bound_constraint(unsigned j) const { return m_int_solver.column_lower_bound_constraint(j); } - constraint_index column_upper_bound_constraint(unsigned j) const { return m_int_solver.column_upper_bound_constraint(j); } - bool column_is_fixed(unsigned j) const { return m_int_solver.lra.column_is_fixed(j); } + const impq & get_value(unsigned j) const { return lia.get_value(j); } + bool is_real(unsigned j) const { return lia.is_real(j); } + bool at_lower(unsigned j) const { return lia.at_lower(j); } + bool at_upper(unsigned j) const { return lia.at_upper(j); } + const impq & lower_bound(unsigned j) const { return lia.lower_bound(j); } + const impq & upper_bound(unsigned j) const { return lia.upper_bound(j); } + constraint_index column_lower_bound_constraint(unsigned j) const { return lia.column_lower_bound_constraint(j); } + constraint_index column_upper_bound_constraint(unsigned j) const { return lia.column_upper_bound_constraint(j); } + bool column_is_fixed(unsigned j) const { return lia.lra.column_is_fixed(j); } void int_case_in_gomory_cut(unsigned j) { - lp_assert(m_int_solver.column_is_int(j) && m_fj.is_pos()); + lp_assert(lia.column_is_int(j) && m_fj.is_pos()); TRACE("gomory_cut_detail", tout << " k = " << m_k; tout << ", fj: " << m_fj << ", "; @@ -131,7 +131,7 @@ class create_cut { if (pol.size() == 1) { TRACE("gomory_cut_detail", tout << "pol.size() is 1" << std::endl;); unsigned v = pol[0].second; - lp_assert(m_int_solver.column_is_int(v)); + lp_assert(lia.column_is_int(v)); const mpq& a = pol[0].first; m_k /= a; if (a.is_pos()) { // we have av >= k @@ -153,7 +153,7 @@ class create_cut { // normalize coefficients of integer parameters to be integers. for (auto & pi: pol) { pi.first *= m_lcm_den; - SASSERT(!m_int_solver.column_is_int(pi.second) || pi.first.is_int()); + SASSERT(!lia.column_is_int(pi.second) || pi.first.is_int()); } m_k *= m_lcm_den; } @@ -207,7 +207,7 @@ class create_cut { } void dump_declaration(std::ostream& out, unsigned v) const { - out << "(declare-const " << var_name(v) << (m_int_solver.column_is_int(v) ? " Int" : " Real") << ")\n"; + out << "(declare-const " << var_name(v) << (lia.column_is_int(v) ? " Int" : " Real") << ")\n"; } void dump_declarations(std::ostream& out) const { @@ -217,7 +217,7 @@ class create_cut { } for (const auto& p : m_t) { unsigned v = p.var(); - if (m_int_solver.lra.is_term(v)) { + if (lia.lra.is_term(v)) { dump_declaration(out, v); } } @@ -276,7 +276,7 @@ public: void dump(std::ostream& out) { out << "applying cut at:\n"; print_linear_combination_indices_only, mpq>(m_row, out); out << std::endl; for (auto & p : m_row) { - m_int_solver.lra.m_mpq_lar_core_solver.m_r_solver.print_column_info(p.var(), out); + lia.lra.m_mpq_lar_core_solver.m_r_solver.print_column_info(p.var(), out); } out << "inf_col = " << m_inf_col << std::endl; } @@ -334,20 +334,20 @@ public: return report_conflict_from_gomory_cut(); if (some_int_columns) adjust_term_and_k_for_some_ints_case_gomory(); - lp_assert(m_int_solver.current_solution_is_inf_on_cut()); + lp_assert(lia.current_solution_is_inf_on_cut()); TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);); - m_int_solver.lra.subs_term_columns(m_t); + lia.lra.subs_term_columns(m_t); TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t.coeffs_as_vector(), tout << "gomory cut:"); tout << " <= " << m_k << std::endl;); return lia_move::cut; } - create_cut(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip& row, const int_solver& int_slv ) : + create_cut(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip& row, const int_solver& lia) : m_t(t), m_k(k), m_ex(ex), m_inf_col(basic_inf_int_j), m_row(row), - m_int_solver(int_slv), + lia(lia), m_lcm_den(1), m_f(fractional_part(get_value(basic_inf_int_j).x)), m_one_minus_f(1 - m_f) {} @@ -359,7 +359,6 @@ lia_move gomory::cut(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_ return cc.cut(); } - bool gomory::is_gomory_cut_target(const row_strip& row) { // All non base variables must be at their bounds and assigned to rationals (that is, infinitesimals are not allowed). unsigned j; diff --git a/src/math/lp/int_gcd_test.cpp b/src/math/lp/int_gcd_test.cpp index b5a9e8c05..78611bfc2 100644 --- a/src/math/lp/int_gcd_test.cpp +++ b/src/math/lp/int_gcd_test.cpp @@ -158,7 +158,7 @@ namespace lp { // u += ncoeff * lower_bound(j).get_rational(); u.addmul(ncoeff, lra.column_lower_bound(j).x); } - lia.add_to_explanation_from_fixed_or_boxed_column(j); + add_to_explanation_from_fixed_or_boxed_column(j); } else if (gcds.is_zero()) { gcds = abs_ncoeff; @@ -186,7 +186,15 @@ namespace lp { void int_gcd_test::fill_explanation_from_fixed_columns(const row_strip & row) { for (const auto & c : row) { if (lra.column_is_fixed(c.var())) - lia.add_to_explanation_from_fixed_or_boxed_column(c.var()); + add_to_explanation_from_fixed_or_boxed_column(c.var()); } } + + void int_gcd_test::add_to_explanation_from_fixed_or_boxed_column(unsigned j) { + constraint_index lc, uc; + lra.get_bound_constraint_witnesses_for_column(j, lc, uc); + lia.m_ex->push_justification(lc); + lia.m_ex->push_justification(uc); + } + } diff --git a/src/math/lp/int_gcd_test.h b/src/math/lp/int_gcd_test.h index 00c97ad6f..3b5e3baaa 100644 --- a/src/math/lp/int_gcd_test.h +++ b/src/math/lp/int_gcd_test.h @@ -9,6 +9,15 @@ Abstract: Gcd_Test heuristic + gcd test + 5*x + 3*y + 6*z = 5 + suppose x is fixed at 2. + so we have 10 + 3(y + 2z) = 5 + 5 = -3(y + 2z) + this is unsolvable because 5/3 is not an integer. + so we create a lemma that rules out this condition. + + Author: Nikolaj Bjorner (nbjorner) Lev Nachmanson (levnach) @@ -33,7 +42,7 @@ namespace lp { mpq const & lcm_den, mpq const & consts); void fill_explanation_from_fixed_columns(const row_strip & row); - + void add_to_explanation_from_fixed_or_boxed_column(unsigned j); public: int_gcd_test(int_solver& lia); ~int_gcd_test() {} diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 7aa6911ef..080183142 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -312,12 +312,6 @@ lia_move int_solver::patch_nbasic_columns() { } // TBD: move to gcd-test -void int_solver::add_to_explanation_from_fixed_or_boxed_column(unsigned j) { - constraint_index lc, uc; - lra.get_bound_constraint_witnesses_for_column(j, lc, uc); - m_ex->push_justification(lc); - m_ex->push_justification(uc); -} int_solver::int_solver(lar_solver& lar_slv) : diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h index 1cfe4a74b..735ab46b3 100644 --- a/src/math/lp/int_solver.h +++ b/src/math/lp/int_solver.h @@ -52,6 +52,7 @@ public: // methods int_solver(lar_solver& lp); + // main function to check that the solution provided by lar_solver is valid for integral values, // or provide a way of how it can be adjusted. lia_move check(explanation *); @@ -69,31 +70,8 @@ public: bool at_upper(unsigned j) const; private: - - // how to tighten bounds for integer variables. - - bool gcd_test_for_row(static_matrix> & A, unsigned i); - - // gcd test - // 5*x + 3*y + 6*z = 5 - // suppose x is fixed at 2. - // so we have 10 + 3(y + 2z) = 5 - // 5 = -3(y + 2z) - // this is unsolvable because 5/3 is not an integer. - // so we create a lemma that rules out this condition. - // - bool gcd_test(); // returns false in case of failure. Creates a theory lemma in case of failure. - - bool branch(const lp_constraint & new_inequality); - bool ext_gcd_test(const row_strip& row, - mpq const & least_coeff, - mpq const & lcm_den, - mpq const & consts); - void fill_explanation_from_fixed_columns(const row_strip & row); - void add_to_explanation_from_fixed_or_boxed_column(unsigned j); lia_move patch_nbasic_columns(); bool get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m); -private: bool is_boxed(unsigned j) const; bool is_fixed(unsigned j) const; bool is_free(unsigned j) const;