diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index dea03f54c..c776e3432 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -845,34 +845,13 @@ struct solver::imp { - void register_rooted_monomial_containing_vars(unsigned i_rm) { - TRACE("nla_solver", print_rooted_monomial(m_rm_table.vec()[i_rm], tout);); - for (lpvar j_var : m_rm_table.vec()[i_rm].vars()) { - TRACE("nla_solver", print_var(j_var, tout);); - auto it = m_rm_table.var_map().find(j_var); - if (it == m_rm_table.var_map().end()) { - std::unordered_set s; - s.insert(i_rm); - m_rm_table.var_map()[j_var] = s; - } else { - it->second.insert(i_rm); - } - } - } - - void fill_rooted_monomials_containing_var() { - for (unsigned i = 0; i < m_rm_table.vec().size(); i++) { - register_rooted_monomial_containing_vars(i); - } - - } void register_monomials_in_tables() { m_vars_equivalence.clear_monomials_by_abs_vals(); for (unsigned i = 0; i < m_monomials.size(); i++) register_monomial_in_tables(i); - fill_rooted_monomials_containing_var(); + m_rm_table.fill_rooted_monomials_containing_var(); m_rm_table.fill_rooted_factor_to_product(); } diff --git a/src/util/lp/rooted_mons.h b/src/util/lp/rooted_mons.h index d5b7cc308..d6b20421b 100644 --- a/src/util/lp/rooted_mons.h +++ b/src/util/lp/rooted_mons.h @@ -136,5 +136,26 @@ struct rooted_mon_table { find_rooted_monomials_containing_rm(i); } } + + void register_rooted_monomial_containing_vars(unsigned i_rm) { + for (lpvar j_var : vec()[i_rm].vars()) { + auto it = var_map().find(j_var); + if (it == var_map().end()) { + std::unordered_set s; + s.insert(i_rm); + var_map()[j_var] = s; + } else { + it->second.insert(i_rm); + } + } + } + + void fill_rooted_monomials_containing_var() { + for (unsigned i = 0; i < vec().size(); i++) { + register_rooted_monomial_containing_vars(i); + } + + } + }; }