mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-25 15:09:32 +00:00
Code Activity

add coefficients from the elim_vanishing to m_todo

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-11-18 10:28:25 -10:00
parent 5d77885339
commit 43465accc6
1 changed files with 5 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/nlsat/nlsat_explain.cpp
View file

@ -350,20 +350,12 @@ namespace nlsat {
}
lc = m_pm.coeff(p, x, k, reduct);
TRACE(nlsat_explain, tout << "lc: " << lc << " reduct: " << reduct << "\n";);
if (!is_zero(lc)) {
if (!::is_zero(sign(lc))) {
TRACE(nlsat_explain, tout << "lc does no vaninsh\n";);
return;
}
TRACE(nlsat_explain, tout << "got a zero sign on lc\n";);
// lc is not the zero polynomial, but it vanished in the current interpretation.
// so we keep searching...
TRACE(nlsat_explain, tout << "adding zero assumption for var:"; m_solver.display_var(tout, x); tout << ", degree k:" << k << ", p:" ; display(tout, p) << "\n";);
add_zero_assumption(lc);
insert_fresh_factors_in_todo(lc);
if (!is_zero(lc) && sign(lc)) {
TRACE(nlsat_explain, tout << "lc does no vaninsh\n";);
return;
}
add_zero_assumption(lc);
if (k == 0) {
// all coefficients of p vanished in the current interpretation,
// and were added as assumptions.