mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

avoid cleaning m_var_to_its_monomial

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-12-11 17:04:10 -10:00 • committed by Lev Nachmanson
parent 09f5ae7521
commit 5b786c428d
1 changed files with 11 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -95,6 +95,7 @@ struct solver::imp {
// returns the monomial index // returns the monomial index
unsigned add(lpvar v, unsigned sz, lpvar const* vs) { unsigned add(lpvar v, unsigned sz, lpvar const* vs) {
SASSERT(m_var_to_its_monomial.find(v) == m_var_to_its_monomial.end());
unsigned ret = m_var_to_its_monomial[v] = m_monomials.size(); unsigned ret = m_var_to_its_monomial[v] = m_monomials.size();
m_monomials.push_back(monomial(v, sz, vs)); m_monomials.push_back(monomial(v, sz, vs));
TRACE("nla_solver", print_monomial(m_monomials.back(), tout);); TRACE("nla_solver", print_monomial(m_monomials.back(), tout););
@ -331,7 +332,7 @@ struct solver::imp {
for (lpvar v : vars) { for (lpvar v : vars) {
unsigned root = m_vars_equivalence.map_to_root(v, sign); unsigned root = m_vars_equivalence.map_to_root(v, sign);
SASSERT(m_vars_equivalence.is_root(root)); SASSERT(m_vars_equivalence.is_root(root));
TRACE("nla_solver", TRACE("nla_solver_eq",
print_var(v,tout); print_var(v,tout);
tout << " mapped to "; tout << " mapped to ";
@ -534,6 +535,7 @@ struct solver::imp {
} }
i = it->second.m_mons.begin()->m_i; i = it->second.m_mons.begin()->m_i;
TRACE("nla_solver",);
return true; return true;
} }
}; };
@ -835,12 +837,19 @@ struct solver::imp {
for (lpvar j = 0; j < m_lar_solver.number_of_vars(); j++) { for (lpvar j = 0; j < m_lar_solver.number_of_vars(); j++) {
auto it = m_var_to_its_monomial.find(j); auto it = m_var_to_its_monomial.find(j);
if (it != m_var_to_its_monomial.end() if (it != m_var_to_its_monomial.end()
&& m_vars_equivalence.is_root(j)) { && m_monomials[it->second].var() != j) {
TRACE("nla_solver", tout << "j = "; TRACE("nla_solver", tout << "j = ";
print_var(j, tout);); print_var(j, tout););
return false; return false;
} }
} }
for (unsigned i = 0; i < m_monomials.size(); i++){
const monomial& m = m_monomials[i];
lpvar j = m.var();
if (m_var_to_its_monomial.find(j) == m_var_to_its_monomial.end()){
return false;
}
}
return true; return true;
} }
@ -910,7 +919,6 @@ struct solver::imp {
m_vars_equivalence.clear(); m_vars_equivalence.clear();
m_rm_table.clear(); m_rm_table.clear();
m_monomials_containing_var.clear(); m_monomials_containing_var.clear();
m_var_to_its_monomial.clear();
m_expl->clear(); m_expl->clear();
m_lemma->clear(); m_lemma->clear();
} }