From 1921260c424036b40f4fad1eb9a3f171590cdfd3 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 14 Oct 2025 17:43:48 -0700 Subject: [PATCH] restore single cell Signed-off-by: Lev Nachmanson --- src/nlsat/nlsat_explain.cpp | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 83c5f31b6..3d124864b 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1226,6 +1226,7 @@ namespace nlsat { * https://arxiv.org/abs/2003.00409 */ void project_cdcac(polynomial_ref_vector & ps, var max_x) { + bool first = true; if (ps.empty()) return; @@ -1256,9 +1257,17 @@ namespace nlsat { } TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n"; display(tout, ps); tout << "\n";); - add_lcs(ps, x); - psc_discriminant(ps, x); - psc_resultant(ps, x); + if (first) { + add_lcs(ps, x); + psc_discriminant(ps, x); + psc_resultant(ps, x); + first = false; + } + else { + add_lcs(ps, x); + psc_discriminant(ps, x); + psc_resultant_sample(ps, x, samples); + } if (m_todo.empty()) break;