mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

move some functionality from nla_solver to rooted_mons

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-12-06 12:02:08 -10:00 committed by Lev Nachmanson
parent 64a7231079
commit 00acf408bf
2 changed files with 22 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/util/lp/nla_solver.cpp
View file

@ -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<unsigned> 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();
}

21
src/util/lp/rooted_mons.h
View file

@ -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<unsigned> 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);
}
}
};
}