From 14a86127791aa9d966d1be6d925b442404ac09ae Mon Sep 17 00:00:00 2001 From: Lev Date: Thu, 27 Dec 2018 21:50:58 -0800 Subject: [PATCH] fix a bug in order lemma Signed-off-by: Lev --- src/util/lp/nla_solver.cpp | 94 ++++++++++++++++++++++++++++---------- src/util/lp/rooted_mons.h | 18 ++++---- 2 files changed, 80 insertions(+), 32 deletions(-) diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 32e4fdaea..991650f90 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -224,8 +224,10 @@ struct solver::imp { std::ostream & print_factor(const factor& f, std::ostream& out) const { if (f.is_var()) { + out << "VAR, "; print_var(f.index(), out); } else { + out << "PROD, "; print_product(m_rm_table.vec()[f.index()].vars(), out); } out << "\n"; @@ -236,9 +238,9 @@ struct solver::imp { if (f.is_var()) { print_var(f.index(), out); } else { - print_product_with_vars(m_rm_table.vec()[f.index()].vars(), out); + out << " rm = "; print_rooted_monomial_with_vars(m_rm_table.vec()[f.index()], out); + out << "\n orig mon = "; print_monomial_with_vars(m_monomials[m_rm_table.vec()[f.index()].orig_index()], out); } - out << "vvr(f) = " << vvr(f) << "\n"; return out; } @@ -584,12 +586,51 @@ struct solver::imp { } return false; } - + + bool basic_sign_lemma_on_a_var_bucket_of_abs_vals(const rational& v, const unsigned_vector& vars ) { + for(unsigned j : vars) { + auto it = m_var_to_its_monomial.find(j); + if (it == m_var_to_its_monomial.end()) { + continue; + } + unsigned i = it->second; + const monomial& m = m_monomials[i]; + monomial_coeff mc = canonize_monomial(m); + TRACE("nla_solver", tout << "m = "; print_monomial_with_vars(m, tout); + tout << "mc = "; print_product_with_vars(mc.vars(), tout);); + + auto rit = m_rm_table.map().find(mc.vars()); + SASSERT(rit != m_rm_table.map().end()); + unsigned rm_i = rit->second.m_i; + const rooted_mon& rm = m_rm_table.vec()[rm_i]; + unsigned rm_j = var(rm); + if (rm_j == j) continue; + if (abs(vvr(rm_j)) != v) { + explain(m); + explain(rm); + generate_bsm(j, rm_j); + return true; + } + } + return false; + } + + void generate_bsm(unsigned j, unsigned k) { + auto jv = vvr(j); + auto kv = vvr(k); + auto js = rational(rat_sign(jv)); + auto ks = rational(rat_sign(kv)); + mk_ineq(js, j, -ks, k, llc::EQ); + } /** * \brief & vars, unsigned & i) const { + SASSERT(vars_are_roots(vars)); + auto it = m_rm_table.map().find(vars); + if (it == m_rm_table.map().end()) { + return false; + } + + i = it->second.m_i; + TRACE("nla_solver",); + + SASSERT(lp::vectors_are_equal_(vars, m_rm_table.vec()[i].vars())); + return true; + } + struct factorization_factory_imp: factorization_factory { const imp& m_imp; @@ -676,17 +731,7 @@ struct solver::imp { m_imp(s) { } bool find_rm_monomial_of_vars(const svector& vars, unsigned & i) const { - SASSERT(m_imp.vars_are_roots(vars)); - auto it = m_imp.m_rm_table.map().find(vars); - if (it == m_imp.m_rm_table.map().end()) { - return false; - } - - i = it->second.m_i; - TRACE("nla_solver",); - - SASSERT(lp::vectors_are_equal_(vars, m_imp.m_rm_table.vec()[i].vars())); - return true; + return m_imp.find_rm_monomial_of_vars(vars, i); } }; @@ -1135,7 +1180,7 @@ struct solver::imp { register_monomial_in_tables(i); m_rm_table.fill_rooted_monomials_containing_var(); - m_rm_table.fill_rooted_factor_to_product(); + m_rm_table.fill_proper_factors(); } void clear() { @@ -1312,7 +1357,8 @@ struct solver::imp { print_rooted_monomial(rm_bd, tout); tout << "\nac_f[k] = "; print_factor_with_vars(ac_f[k], tout); - tout << "\nd = "; print_factor(d, tout);); + tout << "\nd = "; + print_factor_with_vars(d, tout);); SASSERT(abs(vvr(ac_f[k])) == abs(vvr(d))); factor b; if (!divide(rm_bd, d, b)){ @@ -1341,6 +1387,9 @@ struct solver::imp { } else { const monomial& m = m_monomials[it->second]; monomial_coeff mc = canonize_monomial(m); + TRACE("nla_solver", tout << "m = "; print_monomial_with_vars(m, tout); + tout << "mc = "; print_product_with_vars(mc.vars(), tout);); + auto it = m_rm_table.map().find(mc.vars()); SASSERT(it != m_rm_table.map().end()); i = it->second.m_i; @@ -1356,14 +1405,15 @@ struct solver::imp { } // a > b && c > 0 => ac > bc - // ac is a factorization of m_monomials[i_mon] + // ac is a factorization of rm.vars() // ac[k] plays the role of c bool order_lemma_on_factor(const rooted_mon& rm, const factorization& ac, unsigned k) { auto c = ac[k]; TRACE("nla_solver", tout << "k = " << k << ", c = "; print_factor(c, tout); ); for (const factor & d : factors_with_the_same_abs_val(c)) { - TRACE("nla_solver", tout << "d = "; print_factor(d, tout); ); + TRACE("nla_solver", tout << "d = "; print_factor_with_vars(d, tout); ); + SASSERT(abs(vvr(d)) == abs(vvr(c))); if (d.is_var()) { TRACE("nla_solver", tout << "var(d) = " << var(d);); for (unsigned rm_bd : m_rm_table.var_map()[d.index()]) { @@ -1373,10 +1423,8 @@ struct solver::imp { } } } else { - TRACE("nla_solver", tout << "not a var = " << m_rm_table.factor_to_product()[d.index()].size() ;); - for (unsigned rm_bd : m_rm_table.factor_to_product()[d.index()]) { - TRACE("nla_solver", ); - if (order_lemma_on_ac_and_bd(rm , ac, k, m_rm_table.vec()[rm_bd], d)) { + for (unsigned rm_b : m_rm_table.proper_factors()[d.index()]) { + if (order_lemma_on_ac_and_bd(rm , ac, k, m_rm_table.vec()[rm_b], d)) { return true; } } @@ -1386,7 +1434,7 @@ struct solver::imp { } // a > b && c == d => ac > bd - // ac is a factorization of m_monomials[i_mon] + // ac is a factorization of rm.vars() bool order_lemma_on_factorization(const rooted_mon& rm, const factorization& ac) { SASSERT(ac.size() == 2); CTRACE("nla_solver", diff --git a/src/util/lp/rooted_mons.h b/src/util/lp/rooted_mons.h index cd238af2c..40a6aa99a 100644 --- a/src/util/lp/rooted_mons.h +++ b/src/util/lp/rooted_mons.h @@ -58,15 +58,15 @@ struct rooted_mon_table { // A map from m_vector_of_rooted_monomials to a set // of sets of m_vector_of_rooted_monomials, - // such that for every i and every h in m_vector_of_rooted_monomials[i] + // such that for every i and every h in m_proper_factors[i] // m_vector_of_rooted_monomials[i] is a proper factor of m_vector_of_rooted_monomials[h] - std::unordered_map> m_rooted_factor_to_product; + std::unordered_map> m_proper_factors; void clear() { m_rooted_monomials_map.clear(); m_vector_of_rooted_monomials.clear(); m_rooted_monomials_containing_var.clear(); - m_rooted_factor_to_product.clear(); + m_proper_factors.clear(); } const vector& vec() const { return m_vector_of_rooted_monomials; } @@ -92,12 +92,12 @@ struct rooted_mon_table { return m_rooted_monomials_containing_var; } - std::unordered_map>& factor_to_product() { - return m_rooted_factor_to_product; + std::unordered_map>& proper_factors() { + return m_proper_factors; } - const std::unordered_map>& factor_to_product() const { - return m_rooted_factor_to_product; + const std::unordered_map>& proper_factors() const { + return m_proper_factors; } void reduce_set_by_checking_proper_containment(std::unordered_set& p, @@ -135,10 +135,10 @@ struct rooted_mon_table { // TRACE("nla_solver", trace_print_rms(p, tout);); reduce_set_by_checking_proper_containment(p, rm); // TRACE("nla_solver", trace_print_rms(p, tout);); - factor_to_product()[i_rm] = p; + proper_factors()[i_rm] = p; } - void fill_rooted_factor_to_product() { + void fill_proper_factors() { for (unsigned i = 0; i < vec().size(); i++) { find_rooted_monomials_containing_rm(i); }