From 52653e6e433a9cf36e256c80fd086c3c70354a88 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 21 Aug 2024 17:40:32 -1000 Subject: [PATCH] a version with less pointers: got a conflict Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 196 ++++++++++++++++++++---------- src/math/lp/dioph_eq.h | 1 + src/math/lp/int_solver.cpp | 9 +- src/math/lp/lar_solver.cpp | 7 ++ src/math/lp/lar_solver.h | 1 + src/math/lp/lar_term.h | 33 +++++ src/math/lp/lp_bound_propagator.h | 8 +- 7 files changed, 181 insertions(+), 74 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index addddafae..0dbe7c5c8 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -12,6 +12,14 @@ namespace lp { class term_o:public lar_term { mpq m_c; public: + term_o clone() const { + term_o ret; + for (const auto & p: *this) { + ret.add_monomial(p.coeff(), p.j()); + } + ret.c() = c(); + return ret; + } const mpq& c() const { return m_c; } mpq& c() { return m_c; } term_o():m_c(0) {} @@ -32,7 +40,11 @@ namespace lp { } }; - std::ostream& print_term(term_o const& term, std::ostream& out, const std::string & var_prefix) const { + std::ostream& print_lar_term_L(lar_term & t, std::ostream & out) const { + return print_linear_combination_customized(t.coeffs_as_vector(), [](int j)->std::string {return "y"+std::to_string(j);}, out ); + } + + std::ostream& print_term_o(term_o const& term, std::ostream& out, const std::string & var_prefix) const { if (term.size() == 0) { out << "0"; return out; @@ -57,8 +69,13 @@ namespace lp { out << var_prefix << p.j(); } - if (!term.c().is_zero()) - out << " + " << term.c(); + if (!term.c().is_zero()) { + if (term.c().is_pos()) + out << " + " << term.c(); + else + out << " - " << -term.c(); + + } return out; } @@ -67,19 +84,19 @@ namespace lp { e is an equation and ℓ is a linear combination of variables from L */ struct eprime_pair { - term_o * m_e; - lar_term * m_l; + term_o m_e; + lar_term m_l; }; vector m_eprime; /* Let L be a set of variables disjoint from X, and let λ be a mapping from variables in L to linear combinations of variables in X and of integer constants */ - u_map m_lambda; // maps to the index of the term in m_eprime + u_map m_lambda; // maps to the index of the eprime_pair in m_eprime /* let σ be a partial mapping from variables in L united with X to linear combinations of variables in X and of integer constants showing the substitutions */ - u_map m_sigma; + u_map m_sigma; public: int_solver& lia; @@ -90,20 +107,13 @@ namespace lp { std::list m_f; // F = {λ(t):t in m_f} // set S std::list m_s; // S = {λ(t): t in m_s} + + unsigned m_conflict_index = -1; // m_eprime[m_conflict_index] gives the conflict imp(int_solver& lia, lar_solver& lra): lia(lia), lra(lra) { m_last_fresh_x_var = -1; } - bool belongs_to_list(term_o* t, std::list l) { - for (auto& item : l) { - if (item == t) { - return true; - } - } - return false; - } - void init() { unsigned n_of_rows = static_cast(lra.r_basis().size()); unsigned skipped = 0; @@ -122,31 +132,32 @@ namespace lp { } if (all_vars_are_int) { - term_o* t = new term_o(); + term_o t; const auto lcm = get_denominators_lcm(row); for (const auto & p: row) { - t->add_monomial(lcm * p.coeff(), p.var()); + t.add_monomial(lcm * p.coeff(), p.var()); if(lia.is_fixed(p.var())) { - t->c() += lia.lower_bound(p.var()).x; + t.c() += lia.lower_bound(p.var()).x; } } unsigned lvar = static_cast(m_f.size()); - lar_term* lt = new lar_term(); - lt->add_var(lvar); + lar_term lt = lar_term(lvar); eprime_pair pair = {t, lt}; m_eprime.push_back(pair); m_lambda.insert(lvar, lvar); m_f.push_back(lvar); - } } } // returns true if no conflict is found and false otherwise - bool normalize_e_by_gcd(term_o& e) { + bool normalize_e_by_gcd(eprime_pair& ep) { mpq g(0); - for (auto & p : e) { + TRACE("dioph_eq", print_term_o(ep.m_e, tout << "m_e:", "x") << std::endl; + print_lar_term_L(ep.m_l, tout << "m_l:") << std::endl; + ); + for (auto & p : ep.m_e) { if (g.is_zero()) { g = abs(p.coeff()); } else { @@ -158,20 +169,38 @@ namespace lp { } if (g.is_one()) return true; - std::cout << "reached\n"; - e.c() *= (1/g); - if (!e.c().is_int()) { + mpq new_c = ep.m_e.c() / g; + if (new_c.is_int() == false) { // conlict: todo - collect the conflict - NOT_IMPLEMENTED_YET(); + TRACE("dioph_eq", + print_term_o(ep.m_e, tout << "conflict m_e:", "x") << 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, "x") << ")"<< std::endl; + } + tout << "S:\n"; + for (const auto& t : m_sigma) { + tout << "x" << t.m_key << " -> "; + print_term_o(t.m_value, tout, "x") << std::endl; + } + ); return false; + } else { + for (auto& p: ep.m_e.coeffs()) { + p.m_value /= g; + } + ep.m_e.c() = new_c; + ep.m_l *= (1/g); + } return true; } // returns true if no conflict is found and false otherwise bool normalize_by_gcd() { for (unsigned l: m_f) { - term_o* e = m_eprime[l].m_e; - if (!normalize_e_by_gcd(*e)) { + if (!normalize_e_by_gcd(m_eprime[l])) { + m_conflict_index = l; return false; } } @@ -191,50 +220,69 @@ namespace lp { return m_f.begin(); // TODO: make a smarter joice } - void substitute(unsigned k, term_o* s) { - print_term(*s, std::cout<< k<< "->", "x") << std::endl; + void substitute_var_on_f(unsigned k, int k_sign, const term_o& k_subst, const lar_term& l_term) { + TRACE("dioph_eq", print_term_o(k_subst, tout<< k<< "->", "x") << std::endl;); for (unsigned e_index: m_f) { - term_o* e = m_eprime[e_index].m_e; - if (!e->contains(k)) continue; - print_term(*e, std::cout << "before:", "x") << std::endl; - e->substitute(*s, k); - print_term(*e, std::cout << "after :", "x") << std::endl; + term_o& e = m_eprime[e_index].m_e; + if (!e.contains(k)) continue; + const mpq& k_coeff = e.get_coeff(k); + TRACE("dioph_eq", print_term_o(e, tout << "before:", "x") << std::endl; + tout << "k_coeff:" << k_coeff << std::endl;); + m_eprime[e_index].m_l = k_sign*k_coeff*l_term + lar_term(e_index); // m_l is set to k_sign*e + e_sub + e.substitute(k_subst, k); + TRACE("dioph_eq", print_term_o(e, tout << "after :", "x") << std::endl; + print_lar_term_L(m_eprime[e_index].m_l, tout) << std::endl;); } } + + std::tuple find_minimal_abs_coeff(const term_o& eh) const { + bool first = true; + mpq ahk; + unsigned k; + int k_sign; + mpq t; + for (auto& p : eh) { + t = abs(p.coeff()); + if (first || t < ahk) { + ahk = t; + k_sign = p.coeff().is_pos() ? 1 : -1; + k = p.j(); + if (ahk.is_one()) + break; + first = false; + } + } + return std::make_tuple(ahk, k, k_sign); + } + + term_o get_term_to_subst(const term_o& eh, unsigned k, int k_sign) { + term_o t; + for (const auto & p: eh) { + if (p.j() == k) continue; + t.add_monomial(-k_sign*p.coeff(), p.j()); + } + t.c() = eh.c(); + TRACE("dioph_eq", tout << "subst_term:"; print_term_o(t, tout, "x") << std::endl;); + return t; + } // this is the step 6 or 7 of the algorithm void rewrite_eqs() { auto eh_it = pick_eh(); auto eprime_entry = m_eprime[*eh_it]; - std - term_o* eh = m_eprime[*eh_it].m_e; - - // looking for minimal in absolute value coefficient - bool first = true; - mpq ahk; - unsigned k; - int k_sign; - for (auto& p: *eh) { - if (first || abs(p.coeff()) < ahk) { - ahk = abs(p.coeff()); - k_sign = p.coeff().is_pos()? 1:-1; - k = p.j(); - if (ahk.is_one()) - break; - first = false; - } - } + TRACE("dioph_eq", tout << "eprime_entry[" << *eh_it << "]{\n"; + print_term_o(m_eprime[*eh_it].m_e, tout << "\tm_e:", "x") << "," << std::endl; + print_lar_term_L(m_eprime[*eh_it].m_l, tout<< "\tm_l:") << "\n}"<< std::endl;); + + term_o& eh = m_eprime[*eh_it].m_e; + auto [ahk, k, k_sign] = find_minimal_abs_coeff(eh); + if (ahk.is_one()) { // step 6 - term_o *s_term = new term_o(); - s_term->j() = k; // keep the assigned variable in m_j of the term - for (auto& p:*eh) { - if (p.j() == k) continue; - s_term->add_monomial(-k_sign*p.coeff(), p.j()); - } m_s.push_back(*eh_it); m_f.erase(eh_it); - m_sigma.insert(k, s_term); - substitute(k, s_term); + term_o t = get_term_to_subst(eh, k, k_sign); + m_sigma.insert(k, t); + substitute_var_on_f(k, k_sign, t, eprime_entry.m_l) ; } else { // step 7 // the fresh variable @@ -244,7 +292,21 @@ namespace lp { } } - + void explain(lp::explanation& ex) { + auto & ep = m_eprime[m_conflict_index]; + for (const auto & p : ep.m_l) { + remove_fresh_variables(m_eprime[p.j()].m_e); + } + u_dependency* dep = nullptr; + for (const auto & p : ep.m_l) { + if (lra.column_is_fixed(p.j())) { + lra.explain_fixed_column(p.j(), ex); + } + } + } + void remove_fresh_variables(term_o& t) { + // TODO implement + } }; // Constructor definition dioph_eq::dioph_eq(int_solver& lia): lia(lia) { @@ -255,8 +317,10 @@ namespace lp { } lia_move dioph_eq::check() { - return m_imp->check(); - + return m_imp->check(); + } + void dioph_eq::explain(lp::explanation& ex) { + m_imp->explain(ex); } } diff --git a/src/math/lp/dioph_eq.h b/src/math/lp/dioph_eq.h index 36d45844e..628453d60 100644 --- a/src/math/lp/dioph_eq.h +++ b/src/math/lp/dioph_eq.h @@ -29,5 +29,6 @@ namespace lp { dioph_eq(int_solver& lia); ~dioph_eq(); lia_move check(); + void explain(lp::explanation&); }; } diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index fc9572fa7..7ebda83cb 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -166,7 +166,14 @@ namespace lp { lia_move solve_dioph_eq() { dioph_eq de(lia); - de.check(); + lia_move r = de.check(); + + if (r == lia_move::unsat) { + de.explain(*this->m_ex); + } else if (r == lia_move::sat) { + NOT_IMPLEMENTED_YET(); + } + return lia_move::undef; } diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 0c458dbfa..9cdee183d 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -760,6 +760,13 @@ namespace lp { } + void lar_solver::explain_fixed_column(unsigned j, explanation& ex) { + SASSERT(column_is_fixed(j)); + auto* deps = get_bound_constraint_witnesses_for_column(j); + for (auto ci : flatten(deps)) + ex.push_back(ci); + } + void lar_solver::remove_fixed_vars_from_base() { // this will allow to disable and restore the tracking of the touched rows flet f(m_mpq_lar_core_solver.m_r_solver.m_touched_rows, nullptr); diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index c3935d24d..625839c92 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -591,6 +591,7 @@ public: } return dep; } + 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); } inline constraint_set const& constraints() const { return m_constraints; } void push(); diff --git a/src/math/lp/lar_term.h b/src/math/lp/lar_term.h index 659158b96..5f5cdc2d2 100644 --- a/src/math/lp/lar_term.h +++ b/src/math/lp/lar_term.h @@ -118,6 +118,12 @@ public: m_coeffs.erase(j); } + + const mpq & get_coeff(unsigned j) const { + auto* it = m_coeffs.find_core(j); + SASSERT(it != nullptr); + return it->get_data().m_value; + } // the monomial ax[j] is substituted by ax[k] void subst_index(unsigned j, unsigned k) { auto* it = m_coeffs.find_core(j); @@ -145,6 +151,33 @@ public: return ret; } + + lar_term clone() const { + lar_term ret; + for (const auto& p : *this) { + ret.add_monomial(p.coeff(), p.j()); + } + return ret; + } + + + lar_term operator+(const lar_term& other) const { + lar_term ret = other.clone(); + for (const auto& p : *this) { + ret.add_monomial(p.coeff(), p.j()); + } + return ret; + } + + + friend lar_term operator*(const mpq& k, const lar_term& term) { + lar_term result; + for (const auto& p : term) { + result.add_monomial(p.coeff()*k, p.j()); + } + return result; + } + lar_term& operator*=(mpq const& k) { for (auto & t : m_coeffs) t.m_value *= k; diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index e2ebbfbed..d45d4cc7c 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -273,13 +273,7 @@ public: } return base; } - - void explain_fixed_column(unsigned j, explanation& ex) { - SASSERT(column_is_fixed(j)); - auto* deps = lp().get_bound_constraint_witnesses_for_column(j); - for (auto ci : lp().flatten(deps)) - ex.push_back(ci); - } + #ifdef Z3DEBUG bool all_fixed_in_row(unsigned row) const { for (const auto& c : lp().get_row(row))