mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

isolate init_to_refine()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-01-09 21:23:06 +05:30
parent ceac1dc4f7
commit bd1be96e0f
1 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1330,7 +1330,6 @@ struct solver::imp {
}
void clear() {
m_to_refine.clear();
m_var_to_its_monomial.clear();
m_vars_equivalence.clear();
m_rm_table.clear();
@ -1344,10 +1343,10 @@ struct solver::imp {
map_vars_to_monomials();
init_vars_equivalence();
register_monomials_in_tables();
init_to_refine();
}
void init_to_refine() {
m_to_refine.clear();
for (unsigned i = 0; i < m_monomials.size(); i++) {
if (!check_monomial(m_monomials[i]))
m_to_refine.push_back(i);
@ -1917,11 +1916,11 @@ struct solver::imp {
return l_undef;
}
init_search();
init_to_refine();
if (m_to_refine.empty()) {
return l_true;
}
init_search();
lbool ret = l_undef;
for (int search_level = 0; search_level < 3 && ret == l_undef; search_level++) {
TRACE("nla_solver", tout << "search_level = " << search_level << "\n";);