mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-31 06:07:46 +00:00
Code Activity

fix nlsat_explain.cpp that the regression tests would pass with lws=false

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-02-08 08:40:49 -10:00
parent 72564da251
commit 56db8d5e98
1 changed files with 19 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

27
src/nlsat/nlsat_explain.cpp
View file

@ -100,8 +100,8 @@ namespace nlsat {
m_simplify_cores = false; m_simplify_cores = false;
m_full_dimensional = false; m_full_dimensional = false;
m_minimize_cores = false; m_minimize_cores = false;
m_add_all_coeffs = true; m_add_all_coeffs = false;
m_add_zero_disc = true; m_add_zero_disc = false;
} }
// display helpers moved to free functions in nlsat_common.h // display helpers moved to free functions in nlsat_common.h
@ -901,11 +901,11 @@ namespace nlsat {
yy = m_pm.mk_polynomial(y); yy = m_pm.mk_polynomial(y);
p_diff = 2*A*yy + B; p_diff = 2*A*yy + B;
p_diff = m_pm.normalize(p_diff); p_diff = m_pm.normalize(p_diff);
int sq = ensure_sign(q); int sq = ensure_sign_quad(q);
if (sq < 0) { if (sq < 0) {
return false; return false;
} }
int sa = ensure_sign(A); int sa = ensure_sign_quad(A);
if (sa == 0) { if (sa == 0) {
q = B*yy + C; q = B*yy + C;
return mk_plinear_root(k, y, i, q); return mk_plinear_root(k, y, i, q);
@ -918,12 +918,23 @@ namespace nlsat {
return true; return true;
} }
int ensure_sign(polynomial_ref & p) { void ensure_sign(polynomial_ref & p) {
if (is_const(p) || m_processed.contains(p))
return;
int s = sign(p); int s = sign(p);
if (!is_const(p)) { TRACE(nlsat_explain, tout << p << "\n";);
add_assumption(s == 0 ? atom::EQ : (s < 0 ? atom::LT : atom::GT), p);
// Also add p to the projection to ensure proper cell construction
insert_fresh_factors_in_todo(p);
}
// Specialized version for quadratic root handling.
// Returns the sign value (-1, 0, or 1).
int ensure_sign_quad(polynomial_ref & p) {
int s = sign(p);
if (!is_const(p) && !m_processed.contains(p)) {
TRACE(nlsat_explain, tout << p << "\n";); TRACE(nlsat_explain, tout << p << "\n";);
add_assumption(s == 0 ? atom::EQ : (s < 0 ? atom::LT : atom::GT), p); add_assumption(s == 0 ? atom::EQ : (s < 0 ? atom::LT : atom::GT), p);
// Also add p to the projection to ensure proper cell construction
insert_fresh_factors_in_todo(p); insert_fresh_factors_in_todo(p);
} }
return s; return s;
@ -1101,7 +1112,6 @@ namespace nlsat {
use_all_coeffs = true; use_all_coeffs = true;
} }
// Set m_add_all_coeffs for the rest of the projection, restore on function exit // Set m_add_all_coeffs for the rest of the projection, restore on function exit
flet<bool> _set_all_coeffs(m_add_all_coeffs, use_all_coeffs || m_add_all_coeffs);
var x = m_todo.extract_max_polys(ps); var x = m_todo.extract_max_polys(ps);
collect_to_processed(ps); collect_to_processed(ps);
@ -1665,6 +1675,7 @@ namespace nlsat {
void compute_conflict_explanation(unsigned num, literal const * ls, scoped_literal_vector & result) { void compute_conflict_explanation(unsigned num, literal const * ls, scoped_literal_vector & result) {
SASSERT(check_already_added()); SASSERT(check_already_added());
SASSERT(num > 0); SASSERT(num > 0);
flet<bool> _restore_add_all_coeffs(m_add_all_coeffs, false);
TRACE(nlsat_explain, TRACE(nlsat_explain,
tout << "the infeasible clause:\n"; tout << "the infeasible clause:\n";
display(tout, m_solver, num, ls) << "\n"; display(tout, m_solver, num, ls) << "\n";