mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 10:30:44 +00:00
Code Activity

tesing factorization of monomials in nla_solver

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-09-27 16:22:53 -07:00 • committed by Lev Nachmanson
parent 83dda2f162
commit 012131df73
1 changed files with 10 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1055,18 +1055,22 @@ struct solver::imp {
k = k_vars[0]; k = k_vars[0];
k_sign = 1; k_sign = 1;
k_mon = -1; k_mon = -1;
} else if (!m_binary_factorizations.m_imp.find_monomial_of_vars(k_vars, m, k_sign)) { } else {
return false; if (!m_binary_factorizations.m_imp.find_monomial_of_vars(k_vars, m, k_sign)) {
return false;
}
k = m.var();
} }
k = m.var();
if (j_vars.size() == 1) { if (j_vars.size() == 1) {
j = j_vars[0]; j = j_vars[0];
j_sign = 1; j_sign = 1;
} else if (!m_binary_factorizations.m_imp.find_monomial_of_vars(j_vars, m, j_sign)) { } else {
return false; if (!m_binary_factorizations.m_imp.find_monomial_of_vars(j_vars, m, j_sign)) {
return false;
}
j = m.var();
} }
sign = j_sign * k_sign; sign = j_sign * k_sign;
j = m.var();
return true; return true;
} }