From 54f447d118a80c7201bda1acd3e5de994ca2e1b8 Mon Sep 17 00:00:00 2001 From: Lev Date: Tue, 13 Nov 2018 11:04:06 -0800 Subject: [PATCH] change the signature of int_solver::check by adding explanation* parameter Signed-off-by: Lev --- src/smt/theory_lra.cpp | 30 ++++++++++++++---------------- src/test/lp/lp.cpp | 3 ++- src/util/lp/gomory.cpp | 14 +++++++------- src/util/lp/gomory.h | 2 +- src/util/lp/hnf_cutter.h | 2 +- src/util/lp/int_solver.cpp | 11 ++++++----- src/util/lp/int_solver.h | 5 ++--- src/util/lp/nla_solver.cpp | 28 ++++++++++++++++++++++++++-- src/util/lp/vars_equivalence.h | 2 ++ 9 files changed, 61 insertions(+), 36 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 8f014134d..80832947d 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -415,7 +415,6 @@ class theory_lra::imp { return var; } app_ref cnst(a.mk_numeral(rational(c), is_int), m); - TRACE("arith", tout << "add " << cnst << "\n";); mk_enode(cnst); theory_var v = mk_var(cnst); var = m_solver->add_var(v, true); @@ -424,6 +423,7 @@ class theory_lra::imp { m_var_trail.push_back(v); add_def_constraint(m_solver->add_var_bound(var, lp::GE, rational(c))); add_def_constraint(m_solver->add_var_bound(var, lp::LE, rational(c))); + TRACE("arith", tout << "add " << cnst << ", var = " << var << "\n";); return var; } @@ -785,7 +785,7 @@ class theory_lra::imp { m_constraint_sources.setx(index, inequality_source, null_source); m_inequalities.setx(index, lit, null_literal); ++m_stats.m_add_rows; - TRACE("arith", m_solver->print_constraint(index, tout) << "\n";); + TRACE("arith", m_solver->print_constraint(index, tout) << " m_stats.m_add_rows = " << m_stats.m_add_rows << "\n";); } void add_def_constraint(lp::constraint_index index) { @@ -1709,7 +1709,7 @@ public: return st; case l_false: - set_conflict(); + get_infeasibility_explanation_and_set_conflict(); return FC_CONTINUE; case l_undef: TRACE("arith", tout << "check feasiable is undef\n";); @@ -2023,8 +2023,7 @@ public: if (!check_idiv_bounds()) { return l_false; } - m_explanation.clear(); - switch (m_lia->check()) { + switch (m_lia->check(&m_explanation)) { case lp::lia_move::sat: lia_check = l_true; break; @@ -2057,11 +2056,11 @@ public: m.trace_stream() << "[end-of-instance]\n"; } IF_VERBOSE(2, verbose_stream() << "cut " << b << "\n"); - TRACE("arith", dump_cut_lemma(tout, m_lia->get_term(), m_lia->get_offset(), m_lia->get_explanation(), m_lia->is_upper());); + TRACE("arith", dump_cut_lemma(tout, m_lia->get_term(), m_lia->get_offset(), m_explanation, m_lia->is_upper());); m_eqs.reset(); m_core.reset(); m_params.reset(); - for (auto const& ev : m_lia->get_explanation()) { + for (auto const& ev : m_explanation) { if (!ev.first.is_zero()) { set_evidence(ev.second); } @@ -2077,9 +2076,8 @@ public: case lp::lia_move::conflict: TRACE("arith", tout << "conflict\n";); // ex contains unsat core - set_conflict1(); - lia_check = l_false; - break; + set_conflict(); + return l_false; case lp::lia_move::undef: TRACE("arith", tout << "lia undef\n";); lia_check = l_undef; @@ -2098,7 +2096,7 @@ public: m_a2 = alloc(scoped_anum, m_nra->am()); switch (r) { case l_false: - set_conflict1(); + set_conflict(); break; case l_true: m_use_nra_model = true; @@ -2271,7 +2269,7 @@ public: switch(lbl) { case l_false: TRACE("arith", tout << "propagation conflict\n";); - set_conflict(); + get_infeasibility_explanation_and_set_conflict(); break; case l_true: propagate_basic_bounds(); @@ -2298,7 +2296,7 @@ public: (void)new_num_of_p; CTRACE("arith", new_num_of_p > num_of_p, tout << "found " << new_num_of_p << " implied bounds\n";); if (is_infeasible()) { - set_conflict(); + get_infeasibility_explanation_and_set_conflict(); } else { for (unsigned i = 0; !m.canceled() && !ctx().inconsistent() && i < bp.m_ibounds.size(); ++i) { @@ -3237,13 +3235,13 @@ public: } } - void set_conflict() { + void get_infeasibility_explanation_and_set_conflict() { m_explanation.clear(); m_solver->get_infeasibility_explanation(m_explanation); - set_conflict1(); + set_conflict(); } - void set_conflict1() { + void set_conflict() { literal_vector core; set_conflict_or_lemma(core, true); } diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index f9aa371c5..ac7a591c9 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -3521,7 +3521,8 @@ void test_maximize_term() { std::cout<< "v[" << p.first << "] = " << p.second << std::endl; } std::cout << "calling int_solver\n"; - lia_move lm = i_solver.check(); + explanation ex; + lia_move lm = i_solver.check(&ex); VERIFY(lm == lia_move::sat); impq term_max; lp_status st = solver.maximize_term(term_2x_pl_2y, term_max); diff --git a/src/util/lp/gomory.cpp b/src/util/lp/gomory.cpp index b0ae395bd..80a87467a 100644 --- a/src/util/lp/gomory.cpp +++ b/src/util/lp/gomory.cpp @@ -26,7 +26,7 @@ namespace lp { class gomory::imp { lar_term & m_t; // the term to return in the cut mpq & m_k; // the right side of the cut - explanation& m_ex; // the conflict explanation + 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; @@ -58,7 +58,7 @@ class gomory::imp { new_a = m_fj <= m_one_minus_f ? m_fj / m_one_minus_f : ((1 - m_fj) / m_f); lp_assert(new_a.is_pos()); m_k.addmul(new_a, lower_bound(j).x); - m_ex.push_justification(column_lower_bound_constraint(j)); + m_ex->push_justification(column_lower_bound_constraint(j)); } else { lp_assert(at_upper(j)); @@ -66,7 +66,7 @@ class gomory::imp { new_a = - (m_fj <= m_f ? m_fj / m_f : ((1 - m_fj) / m_one_minus_f)); lp_assert(new_a.is_neg()); m_k.addmul(new_a, upper_bound(j).x); - m_ex.push_justification(column_upper_bound_constraint(j)); + m_ex->push_justification(column_upper_bound_constraint(j)); } m_t.add_coeff_var(new_a, j); m_lcm_den = lcm(m_lcm_den, denominator(new_a)); @@ -85,7 +85,7 @@ class gomory::imp { } m_k.addmul(new_a, lower_bound(j).x); // is it a faster operation than // k += lower_bound(j).x * new_a; - m_ex.push_justification(column_lower_bound_constraint(j)); + m_ex->push_justification(column_lower_bound_constraint(j)); } else { lp_assert(at_upper(j)); @@ -96,7 +96,7 @@ class gomory::imp { new_a = a / m_one_minus_f; } m_k.addmul(new_a, upper_bound(j).x); // k += upper_bound(j).x * new_a; - m_ex.push_justification(column_upper_bound_constraint(j)); + m_ex->push_justification(column_upper_bound_constraint(j)); } TRACE("gomory_cut_detail_real", tout << a << "*v" << j << " k: " << m_k << "\n";); m_t.add_coeff_var(new_a, j); @@ -314,7 +314,7 @@ public: return lia_move::cut; } - imp(lar_term & t, mpq & k, explanation& ex, unsigned basic_inf_int_j, const row_strip& row, const int_solver& int_slv ) : + imp(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip& row, const int_solver& int_slv ) : m_t(t), m_k(k), m_ex(ex), @@ -331,7 +331,7 @@ lia_move gomory::create_cut() { return m_imp->create_cut(); } -gomory::gomory(lar_term & t, mpq & k, explanation& ex, unsigned basic_inf_int_j, const row_strip& row, const int_solver& s) { +gomory::gomory(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip& row, const int_solver& s) { m_imp = alloc(imp, t, k, ex, basic_inf_int_j, row, s); } diff --git a/src/util/lp/gomory.h b/src/util/lp/gomory.h index acb5f04fd..7e5e081e1 100644 --- a/src/util/lp/gomory.h +++ b/src/util/lp/gomory.h @@ -27,7 +27,7 @@ class gomory { class imp; imp *m_imp; public : - gomory(lar_term & t, mpq & k, explanation& ex, unsigned basic_inf_int_j, const row_strip& row, const int_solver& s); + gomory(lar_term & t, mpq & k, explanation* ex, unsigned basic_inf_int_j, const row_strip& row, const int_solver& s); lia_move create_cut(); ~gomory(); }; diff --git a/src/util/lp/hnf_cutter.h b/src/util/lp/hnf_cutter.h index 74ee47d35..a96d9ec4c 100644 --- a/src/util/lp/hnf_cutter.h +++ b/src/util/lp/hnf_cutter.h @@ -186,7 +186,7 @@ public: bool overflow() const { return m_overflow; } - lia_move create_cut(lar_term& t, mpq& k, explanation& ex, bool & upper, const vector & x0) { + lia_move create_cut(lar_term& t, mpq& k, explanation* ex, bool & upper, const vector & x0) { // we suppose that x0 has at least one non integer element (void)x0; diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp index 6d5cc5437..1480e0f28 100644 --- a/src/util/lp/int_solver.cpp +++ b/src/util/lp/int_solver.cpp @@ -382,9 +382,9 @@ lia_move int_solver::make_hnf_cut() { ); lp_assert(current_solution_is_inf_on_cut()); settings().st().m_hnf_cuts++; - m_ex.clear(); + m_ex->clear(); for (unsigned i : m_hnf_cutter.constraints_for_explanation()) { - m_ex.push_justification(i); + m_ex->push_justification(i); } } return r; @@ -412,7 +412,8 @@ lia_move int_solver::check() { m_t.clear(); m_k.reset(); - m_ex.clear(); + m_ex = e; + m_ex->clear(); m_upper = false; lia_move r; @@ -596,8 +597,8 @@ bool int_solver::gcd_test_for_row(static_matrix> & A, uns void int_solver::add_to_explanation_from_fixed_or_boxed_column(unsigned j) { constraint_index lc, uc; m_lar_solver->get_bound_constraint_witnesses_for_column(j, lc, uc); - m_ex.push_justification(lc); - m_ex.push_justification(uc); + m_ex->push_justification(lc); + m_ex->push_justification(uc); } void int_solver::fill_explanation_from_fixed_columns(const row_strip & row) { for (const auto & c : row) { diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h index 83a16aed8..fc4a3f5b1 100644 --- a/src/util/lp/int_solver.h +++ b/src/util/lp/int_solver.h @@ -41,7 +41,7 @@ public: unsigned m_number_of_calls; lar_term m_t; // the term to return in the cut mpq m_k; // the right side of the cut - explanation m_ex; // the conflict explanation + explanation *m_ex; // the conflict explanation bool m_upper; // we have a cut m_t*x <= k if m_upper is true nad m_t*x >= k otherwise hnf_cutter m_hnf_cutter; // methods @@ -49,10 +49,9 @@ public: // 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(); + lia_move check(explanation *); lar_term const& get_term() const { return m_t; } mpq const& get_offset() const { return m_k; } - explanation const& get_explanation() const { return m_ex; } bool is_upper() const { return m_upper; } lia_move check_wrapper(lar_term& t, mpq& k, explanation& ex); bool is_base(unsigned j) const; diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 9ceff28fa..f6d256bd8 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -831,12 +831,36 @@ struct solver::imp { m_expl->clear(); m_lemma->clear(); } + + bool order_lemma_on_factor_equiv_and_other_mon_factor(unsigned i_f, + unsigned o_i_mon, unsigned e_j, unsigned i_mon, const factorization& f, unsigned k, const rational& sign) { + return false; + } + bool order_lemma_on_factor_equiv_and_other_mon(unsigned o_i_mon, unsigned e_j, unsigned i_mon, const factorization& f, unsigned k, const rational& sign) { - NOT_IMPLEMENTED_YET(); + if (o_i_mon == i_mon) return false; + const monomial & o_m = m_monomials[o_i_mon]; + svector o_key; + for (unsigned j : o_m) { + if (j != e_j) { + o_key.push_back(j); + } + } + + rational o_sign(1); + o_key = reduce_monomial_to_rooted(o_key, o_sign); + auto it = m_rooted_monomials.find(o_key); + if (it == m_rooted_monomials.end()) + return false; + for (const index_with_sign& i_s : it->second) { + if (order_lemma_on_factor_equiv_and_other_mon_factor(i_s.var(), o_i_mon, e_j, i_mon, f, k, sign * o_sign * i_s.sign())) + return true; + } return false; } - // here e_j is equivalent to f[k], + // f is a factorization of m_monomials[i_mon] + // here e_j is equivalent to f[k], bool order_lemma_on_factor_and_equiv(unsigned e_j, unsigned i_mon, const factorization& f, unsigned k, const rational& sign) { lpvar j = f[k]; for (unsigned i : m_monomials_containing_var[j]) { diff --git a/src/util/lp/vars_equivalence.h b/src/util/lp/vars_equivalence.h index cf8408f68..f63022faf 100644 --- a/src/util/lp/vars_equivalence.h +++ b/src/util/lp/vars_equivalence.h @@ -36,6 +36,8 @@ struct index_with_sign { bool operator==(const index_with_sign& b) { return m_i == b.m_i && m_sign == b.m_sign; } + unsigned var() const { return m_i; } + const rational& sign() const { return m_sign; } }; struct rat_hash {