From 5db46c1d81b1678dd582abb9cd285dd7a9391736 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 4 Sep 2024 10:57:41 -0700 Subject: [PATCH] use u_dependency in eprime_pair Signed-off-by: Lev Nachmanson --- src/math/lp/bound_analyzer_on_row.h | 2 +- src/math/lp/dioph_eq.cpp | 57 ++++++++++++++++++++--------- src/math/lp/gomory.cpp | 2 +- src/math/lp/lar_solver.h | 2 +- 4 files changed, 43 insertions(+), 20 deletions(-) diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h index 20e45a218..791e64327 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -300,7 +300,7 @@ private: int a_sign = is_pos(a) ? 1 : -1; int sign = j_sign * a_sign; u_dependency* witness = sign > 0 ? lar->get_column_upper_bound_witness(j) : lar->get_column_lower_bound_witness(j); - ret = lar->join_deps(ret, witness); + ret = lar->mk_join(ret, witness); } return ret; }; diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 363c3c6ca..6a22e88d4 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -57,7 +57,7 @@ namespace lp { } }; - std::ostream& print_S(std::ostream & out) const { + std::ostream& print_S(std::ostream & out) { out << "S:\n"; for (unsigned i : m_s) { out << "x" << m_eprime[i].m_e.j() << " ->\n"; @@ -117,7 +117,7 @@ namespace lp { */ struct eprime_pair { term_o m_e; - lar_term m_l; // this term keeps the history of m_e : originally m_l is i, the index of row m_e was constructed from + u_dependency *m_l; // this term keeps the history of m_e : originally m_l is i, the index of row m_e was constructed from }; vector m_eprime; @@ -179,7 +179,8 @@ namespace lp { SASSERT(t.c().is_zero()); continue; } - eprime_pair pair = {t, lar_term(i)}; +// eprime_pair pair = {t, lar_term(i)}; + eprime_pair pair = {t, get_dep_from_row(row)}; m_f.push_back(static_cast(m_f.size())); m_eprime.push_back(pair); TRACE("dioph_eq", print_eprime_entry(static_cast(m_f.size()) - 1, tout);); @@ -187,6 +188,17 @@ namespace lp { } + // look only at the fixed columns + u_dependency * get_dep_from_row(const row_strip& row) { + u_dependency* dep = nullptr; + for (const auto & p: row) { + if (!lia.is_fixed(p.var())) continue; + u_dependency * bound_dep = lra.get_bound_constraint_witnesses_for_column(p.var()); + dep = lra.mk_join(dep, bound_dep); + } + return dep; + } + mpq gcd_of_coeffs(const term_o& t) { mpq g(0); for (const auto & p : t) { @@ -198,10 +210,14 @@ namespace lp { } return g; } + std::ostream & print_dep(std::ostream& out, u_dependency* dep) { + explanation ex(lra.flatten(dep)); + return lra.print_expl(out, ex); + } // returns true if no conflict is found and false otherwise bool normalize_e_by_gcd(eprime_pair& ep) { TRACE("dioph_eq", print_term_o(ep.m_e, tout << "m_e:") << std::endl; - print_lar_term_L(ep.m_l, tout << "m_l:") << std::endl; + print_dep(tout << "m_l:", ep.m_l) << std::endl; ); mpq g = gcd_of_coeffs(ep.m_e); if (g.is_zero()) { @@ -216,11 +232,8 @@ namespace lp { TRACE("dioph_eq", print_term_o(ep.m_e, tout << "conflict m_e:") << std::endl; tout << "g:" << g << std::endl; - print_lar_term_L(ep.m_l, tout << "m_l:") << std::endl; - for (const auto & p: ep.m_l) { - tout << p.coeff() << "("; print_term_o(m_eprime[p.j()].m_e, tout) << ")"<< std::endl; - } - tout << "S:\n"; + print_dep(tout << "m_l:", ep.m_l) << std::endl; + tout << "S:\n"; for (const auto& t : m_sigma) { tout << "x" << t.m_key << " -> "; print_term_o(t.m_value, tout) << std::endl; @@ -232,11 +245,11 @@ namespace lp { p.m_value /= g; } ep.m_e.c() = new_c; - ep.m_l *= (1/g); +// ep.m_l *= (1/g); TRACE("dioph_eq", tout << "ep_m_e:"; print_term_o(ep.m_e, tout) << std::endl; tout << "ep.ml:"; - print_lar_term_L(ep.m_l, tout ) << std::endl;); + print_dep(tout, ep.m_l) << std::endl;); } return true; @@ -358,8 +371,8 @@ namespace lp { } } - void substitute_var_on_f(unsigned k, int k_sign, const term_o& k_subst, const lar_term& l_term, unsigned index_to_avoid) { - TRACE("dioph_eq", print_term_o(k_subst, tout<< "x" << k<< " -> ") << std::endl; tout << "l_term:"; print_lar_term_L(l_term, tout) << std::endl;); + void substitute_var_on_f(unsigned k, int k_sign, const term_o& k_subst, u_dependency * dep, unsigned index_to_avoid) { + TRACE("dioph_eq", print_term_o(k_subst, tout<< "x" << k<< " -> ") << std::endl; tout << "dep:"; print_dep(tout, dep) << std::endl;); for (unsigned e_index: m_f) { if (e_index == index_to_avoid) continue; term_o& e = m_eprime[e_index].m_e; @@ -368,12 +381,16 @@ namespace lp { const mpq& k_coeff = e.get_coeff(k); TRACE("dioph_eq", print_eprime_entry(e_index, tout << "before:") << std::endl; tout << "k_coeff:" << k_coeff << std::endl;); + +/* if (!l_term.is_empty()) { if (k_sign == 1) add_operator(m_eprime[e_index].m_l, -k_coeff, l_term); else add_operator(m_eprime[e_index].m_l, k_coeff, l_term); } +*/ + dep = lra.mk_join(dep, m_eprime[e_index].m_l); e.substitute(k_subst, k); TRACE("dioph_eq", print_eprime_entry(e_index, tout << "after :") << std::endl;); } @@ -451,7 +468,8 @@ namespace lp { et.add_monomial(r, p.j()); } m_eprime[e_index].m_e = et; - eprime_pair xt_entry = {xt_term, lar_term()}; // 0 for m_l field + // eprime_pair xt_entry = {xt_term, lar_term()}; // 0 for m_l field + eprime_pair xt_entry = {xt_term, nullptr}; // 0 for m_l field m_eprime.push_back(xt_entry); TRACE("dioph_eq", tout << "xt_term:"; print_term_o(xt_term, tout) << std::endl; tout << "k_subs:"; print_term_o(k_subs, tout) << std::endl; @@ -464,10 +482,10 @@ namespace lp { TRACE("dioph_eq", tout << "xt_subs: x~"<< fresh_index(xt) << " -> "; print_term_o(xt_subs, tout) << std::endl;); m_sigma.insert(xt, xt_subs); } - std::ostream& print_eprime_entry(unsigned i, std::ostream& out) const { + std::ostream& print_eprime_entry(unsigned i, std::ostream& out) { out << "m_eprime[" << i << "]:{\n"; print_term_o(m_eprime[i].m_e, out << "\tm_e:") << "," << std::endl; - print_lar_term_L(m_eprime[i].m_l, out<< "\tm_l:") << "\n}"<< std::endl; + print_dep(out<< "\tm_l:", m_eprime[i].m_l) << "\n}"<< std::endl; return out; } @@ -501,11 +519,16 @@ namespace lp { TRACE("dioph_eq", tout << "conflict:"; print_eprime_entry(m_conflict_index, tout) << std::endl;); auto & ep = m_eprime[m_conflict_index]; u_dependency* dep = nullptr; - for (const auto & pl : ep.m_l) { + /* + for (const auto & pl : ep.m_l) { unsigned row_index = pl.j(); for (const auto & p : lra.get_row(row_index)) if (lra.column_is_fixed(p.var())) lra.explain_fixed_column(p.var(), ex); + } + */ + for (auto ci: lra.flatten(ep.m_l)) { + ex.push_back(ci); } TRACE("dioph_eq", lra.print_expl(tout, ex);); } diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index c0119f7f1..442231558 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -323,7 +323,7 @@ public: m_dep = nullptr; for (auto c : *m_ex) - m_dep = lia.lra.join_deps(lia.lra.dep_manager().mk_leaf(c.ci()), m_dep); + m_dep = lia.lra.mk_join(lia.lra.dep_manager().mk_leaf(c.ci()), m_dep); TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout); lia.lra.display(tout)); diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 00a4f9c06..2c68116aa 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -600,7 +600,7 @@ public: } void explain_fixed_column(unsigned j, explanation& ex); - u_dependency* join_deps(u_dependency* a, u_dependency *b) { return m_dependencies.mk_join(a, b); } + u_dependency* mk_join(u_dependency* a, u_dependency *b) { return m_dependencies.mk_join(a, b); } inline constraint_set const& constraints() const { return m_constraints; } void push(); void pop();