From 7c074dc65c0eecec655fd6e150889d25a7b7ce35 Mon Sep 17 00:00:00 2001 From: Lev Date: Tue, 29 Jan 2019 11:29:24 -0800 Subject: [PATCH] access by indeq from regular monomials to rooted Signed-off-by: Lev --- src/util/lp/nla_solver.cpp | 27 +++------------------------ src/util/lp/rooted_mons.h | 14 +++++++++++++- 2 files changed, 16 insertions(+), 25 deletions(-) diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 682cdaf0c..ce2a2c91f 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -652,22 +652,6 @@ struct solver::imp { return false; } - const rooted_mon& mon_to_rooted_mon(const svector& vars) const { - auto rit = m_rm_table.map().find(vars); - SASSERT(rit != m_rm_table.map().end()); - unsigned rm_i = rit->second; - return m_rm_table.vec()[rm_i]; - } - - - const rooted_mon& mon_to_rooted_mon(const monomial& m) const { - 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);); - - return mon_to_rooted_mon(mc.vars()); - } - /** * \brief second]; SASSERT(m.var() == i); SASSERT(abs(vvr(m)) == abs(vvr(c))); - 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; + const index_with_sign & i_s = m_rm_table.get_rooted_mon(it->second); + i = i_s.index(); // SASSERT(abs(vvr(m_rm_table.vec()[i])) == abs(vvr(c))); if (!contains(found_rm, i)) { found_rm.insert(i); @@ -2436,7 +2415,7 @@ void solver::test_basic_lemma_for_mon_zero_from_monomial_to_factors() { s.set_column_value(lp_a, rational(1)); s.set_column_value(lp_b, rational(1)); s.set_column_value(lp_c, rational(1)); - s.set_column_value(lp_e, rational(1)); + s.set_column_value(lp_d, rational(1)); s.set_column_value(lp_e, rational(1)); s.set_column_value(lp_abcde, rational(1)); s.set_column_value(lp_ac, rational(1)); diff --git a/src/util/lp/rooted_mons.h b/src/util/lp/rooted_mons.h index 9e00b17c1..69a9f304d 100644 --- a/src/util/lp/rooted_mons.h +++ b/src/util/lp/rooted_mons.h @@ -70,7 +70,10 @@ struct rooted_mon_table { // such that for every i and every h in m_proper_factors[i] we have m_vector[i] as a proper factor of m_vector[h] std::unordered_map> m_proper_factors; // points to m_vector - svector m_to_refine; + svector m_to_refine; + // maps the indices of the regular monomials to the rooted monomial indices + std::unordered_map m_reg_to_rm; + const svector& to_refine() { return m_to_refine; } @@ -105,6 +108,7 @@ struct rooted_mon_table { m_mons_containing_var.clear(); m_proper_factors.clear(); m_to_refine.clear(); + m_reg_to_rm.clear(); } const vector& vec() const { return m_vector; } @@ -200,16 +204,24 @@ struct rooted_mon_table { void register_key_mono_in_rooted_monomials(monomial_coeff const& mc, unsigned i_mon) { index_with_sign ms(i_mon, mc.coeff()); + SASSERT(abs(mc.coeff()) == rational(1)); auto it = map().find(mc.vars()); if (it == map().end()) { TRACE("nla_solver", tout << "size = " << vec().size();); map().emplace(mc.vars(), vec().size()); + m_reg_to_rm.emplace(i_mon, index_with_sign(vec().size(), mc.coeff())); vec().push_back(rooted_mon(mc.vars(), i_mon, mc.coeff())); } else { vec()[it->second].push_back(ms); TRACE("nla_solver", tout << "add ms.m_i = " << ms.m_i;); + m_reg_to_rm.emplace(i_mon, index_with_sign(it->second, mc.coeff())); } } + + const index_with_sign& get_rooted_mon(unsigned i_mon) const { + return m_reg_to_rm.find(i_mon)->second; + } + }; }