From 254a40535eddf100b956535ffb375d81b9a38c78 Mon Sep 17 00:00:00 2001 From: Lev Date: Sun, 2 Dec 2018 15:24:49 -0800 Subject: [PATCH] call order_lemma_on_ac_and_bd Signed-off-by: Lev --- src/util/lp/nla_solver.cpp | 74 +++++++++++++++++++++++++------------- 1 file changed, 50 insertions(+), 24 deletions(-) diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 4d4fb8982..14593e80d 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -189,6 +189,7 @@ struct solver::imp { svector r; r.push_back(f.index()); return r; } + TRACE("nla_solver", tout << "nv";); return m_vector_of_rooted_monomials[f.index()].vars(); } @@ -285,6 +286,15 @@ struct solver::imp { return out; } + std::ostream & print_factor_with_vars(const factor& f, std::ostream& out) const { + if (f.is_var()) { + print_var(f.index(), out); + } else { + print_product_with_vars(m_vector_of_rooted_monomials[f.index()].vars(), out); + } + return out; + } + std::ostream& print_monomial(const monomial& m, std::ostream& out) const { out << m_lar_solver.get_variable_name(m.var()) << " = "; return print_product(m.vars(), out); @@ -316,14 +326,12 @@ struct solver::imp { std::ostream& print_rooted_monomial(const rooted_mon& rm, std::ostream& out) const { out << "vars = "; - print_product_with_vars(rm.vars(), out); - out << "\n orig = "; print_monomial_with_vars(m_monomials[rm.orig_index()], out); + print_product(rm.vars(), out); + out << "\n orig = "; print_monomial(m_monomials[rm.orig_index()], out); out << ", orig sign = " << rm.orig_sign() << "\n"; return out; } - - std::ostream& print_explanation(std::ostream& out) const { for (auto &p : *m_expl) { m_lar_solver.print_constraint(p.second, out); @@ -418,7 +426,7 @@ struct solver::imp { // Replaces definition m_v = v1* .. * vn by // m_v = coeff * w1 * ... * wn, where w1, .., wn are canonical - // representatives, that is the roots of the equivalence tree, under current equations. + // representatives, which are the roots of the equivalence tree, under current equations. // monomial_coeff canonize_monomial(monomial const& m) const { rational sign = rational(1); @@ -607,8 +615,6 @@ struct solver::imp { i = it->second.m_mons.begin()->m_i; return true; } - - }; @@ -657,6 +663,7 @@ struct solver::imp { out << "value: " << vvr(rm) << "\n"; print_factorization(f, out << "fact: ") << "\n"; } + // x = 0 or y = 0 -> xy = 0 bool basic_lemma_for_mon_non_zero(const rooted_mon& rm, const factorization& f) { TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout);); @@ -681,8 +688,6 @@ struct solver::imp { return true; } - - // use the fact that // |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 bool basic_lemma_for_mon_neutral_monomial_to_factor(const rooted_mon& rm, const factorization& f) { @@ -937,8 +942,6 @@ struct solver::imp { } } - - void reduce_set_by_checking_actual_containment(std::unordered_set& p, const rooted_mon & rm ) { for (auto it = p.begin(); it != p.end();) { @@ -956,11 +959,19 @@ struct solver::imp { // here i is the index of a monomial in m_vector_of_rooted_monomials void find_containing_rooted_monomials(unsigned i) { const auto & rm = m_vector_of_rooted_monomials[i]; + TRACE("nla_solver", tout << "i = " << i << ", rm = "; print_rooted_monomial(rm, tout);); + std::unordered_set p = m_rooted_monomials_containing_var[rm[0]]; for (unsigned k = 1; k < rm.size(); k++) { intersect_set(p, m_rooted_monomials_containing_var[rm[k]]); } reduce_set_by_checking_actual_containment(p, rm); + TRACE("nla_solver", + tout << "p = " << p.size(); + for (auto j : p) + TRACE("nla_solver", tout << "j = " << j << ", rm = "; print_rooted_monomial(m_vector_of_rooted_monomials[j], tout);); + ); + m_rooted_factor_to_product[i] = p; } @@ -1015,31 +1026,34 @@ struct solver::imp { print_product(c_vars, tout); tout << "\nbc_vars = "; print_product(bc.vars(), tout);); - auto b_vars = vector_div(bc.vars(), sorted_vars(c)); + if (!is_factor(c_vars, bc.vars())) + return false; + + auto b_vars = vector_div(bc.vars(), c_vars); TRACE("nla_solver", tout << "b_vars = "; print_product(b_vars, tout);); - return false; + return true; } - // a > b && c > 0 && d = c => ac > bd + // a > b && c > 0 && d = |c => ac > bd // ac is a factorization of m_monomials[i_mon] // ac[k] plays the role of c bool order_lemma_on_ac_and_bd(const rooted_mon& rm_ac, const factorization& ac_f, unsigned k, - const rooted_mon& rm_bc, + const rooted_mon& rm_bd, const factor& d) { TRACE("nla_solver", - tout << "rm = "; + tout << "rm_ac = "; print_rooted_monomial(rm_ac, tout); - tout << "factor, c = "; print_factor(ac_f[k], tout); - tout << "\nrm_bc = "; - print_rooted_monomial(rm_bc, tout);); + tout << "\nrm_bd = "; + print_rooted_monomial(rm_bd, tout); + tout << ", d = "; print_factor(d, tout);); factor b; - if (!divide(rm_bc, ac_f[k], b)) + if (!divide(rm_bd, d, b)) return false; rational ac_v = vvr(rm_ac); - rational bc_v = vvr(rm_bc); + rational bc_v = vvr(rm_bd); TRACE("nla_solver", tout << "ac_v = " << ac_v << ", bc_v = " << bc_v;); NOT_IMPLEMENTED_YET(); return false; @@ -1051,7 +1065,7 @@ struct solver::imp { vector r; std::unordered_set found_vars; std::unordered_set found_rm; - + TRACE("nla_solver", tout << "c = "; print_factor_with_vars(c, tout);); for (lpvar i : m_vars_equivalence.get_vars_with_the_same_abs_val(vvr(c))) { auto it = m_var_to_its_monomial.find(i); if (it == m_var_to_its_monomial.end()) { @@ -1063,6 +1077,15 @@ struct solver::imp { } else { const monomial& m = m_monomials[it->second]; monomial_coeff mc = canonize_monomial(m); + auto it = m_rooted_monomials_map.find(mc.vars()); + SASSERT(it != m_rooted_monomials_map.end()); + i = it->second.m_i; + if (!contains(found_rm, i)) { + found_rm.insert(i); + r.push_back(factor(i, factor_type::RM)); + TRACE("nla_solver", tout << "ins "; print_factor(factor(i, factor_type::RM), tout); ); + } + } } return r; @@ -1076,15 +1099,18 @@ struct solver::imp { TRACE("nla_solver", tout << "k = " << k << ", c = "; print_factor(c, tout); ); for (const factor & d : primitive_factors_with_the_same_abs_val(c)) { + TRACE("nla_solver", tout << "d = "; print_factor(d, tout); ); if (d.is_var()) { - for (unsigned rm_bd : m_rooted_monomials_containing_var[var(d)]) { + TRACE("nla_solver", tout << "var(d) = " << var(d);); + for (unsigned rm_bd : m_rooted_monomials_containing_var[d.index()]) { TRACE("nla_solver", ); if (order_lemma_on_ac_and_bd(rm , ac, k, m_vector_of_rooted_monomials[rm_bd], d)) { return true; } } } else { - for (unsigned rm_bd : m_rooted_factor_to_product[var(d)]) { + TRACE("nla_solver", tout << "size = " << m_rooted_factor_to_product[d.index()].size() ;); + for (unsigned rm_bd : m_rooted_factor_to_product[d.index()]) { TRACE("nla_solver", ); if (order_lemma_on_ac_and_bd(rm , ac, k, m_vector_of_rooted_monomials[rm_bd], d)) { return true;