From 00acf408bfa85e0c20afc3073f04df4d7cce1eb3 Mon Sep 17 00:00:00 2001 From: Lev Date: Thu, 6 Dec 2018 12:02:08 -1000 Subject: [PATCH] move some functionality from nla_solver to rooted_mons Signed-off-by: Lev --- src/util/lp/nla_solver.cpp | 23 +---------------------- src/util/lp/rooted_mons.h | 21 +++++++++++++++++++++ 2 files changed, 22 insertions(+), 22 deletions(-) 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); + } + + } + }; }