From c87e7c312a1d68c28f4ba4b6f8d4df4ec53441ce Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 27 Aug 2025 10:05:31 -1000 Subject: [PATCH] rename explain::main_operator to compute_conflict_explanation --- src/nlsat/nlsat_explain.cpp | 12 ++++++------ src/nlsat/nlsat_explain.h | 2 +- src/nlsat/nlsat_solver.cpp | 3 ++- src/test/nlsat.cpp | 2 +- 4 files changed, 10 insertions(+), 9 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index ef86c1ffe..576cc5751 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1220,8 +1220,8 @@ namespace nlsat { // Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore polynomial_ref_vector samples(m_pm); - levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am); - auto cell = lws.single_cell(); + // levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am); + //auto cell = lws.single_cell(); if (x < max_x) cac_add_cell_lits(ps, x, samples); @@ -1716,7 +1716,7 @@ namespace nlsat { } } - void operator()(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(num > 0); TRACE(nlsat_explain, @@ -2104,11 +2104,11 @@ namespace nlsat { } void explain::set_signed_project(bool f) { - m_imp->m_signed_project = f; + m_imp->m_signed_project = f;; } - void explain::main_operator(unsigned n, literal const * ls, scoped_literal_vector & result) { - (*m_imp)(n, ls, result); + void explain::compute_conflict_explanation(unsigned n, literal const * ls, scoped_literal_vector & result) { + m_imp->compute_conflict_explanation(n, ls, result); } void explain::project(var x, unsigned n, literal const * ls, scoped_literal_vector & result) { diff --git a/src/nlsat/nlsat_explain.h b/src/nlsat/nlsat_explain.h index 6e1cf091b..95939ae03 100644 --- a/src/nlsat/nlsat_explain.h +++ b/src/nlsat/nlsat_explain.h @@ -63,7 +63,7 @@ namespace nlsat { - s_1, ..., s_m do not contain variable x. - s_1, ..., s_m are false in the current interpretation */ - void main_operator(unsigned n, literal const * ls, scoped_literal_vector & result); + void compute_conflict_explanation(unsigned n, literal const * ls, scoped_literal_vector & result); /** diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 4ca16dd23..55e713e1d 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -2215,12 +2215,13 @@ namespace nlsat { m_lazy_clause.reset(); - m_explain.main_operator(jst.num_lits(), jst.lits(), m_lazy_clause); + m_explain.compute_conflict_explanation(jst.num_lits(), jst.lits(), m_lazy_clause); for (unsigned i = 0; i < sz; i++) m_lazy_clause.push_back(~jst.lit(i)); // lazy clause is a valid clause TRACE(nlsat_mathematica, display_mathematica_lemma(tout, m_lazy_clause.size(), m_lazy_clause.data());); + exit(0); if (m_dump_mathematica) { // verbose_stream() << "lazy clause\n"; display_mathematica_lemma(verbose_stream(), m_lazy_clause.size(), m_lazy_clause.data()) << std::endl; diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 8b283247d..06e6fb58b 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -319,7 +319,7 @@ static void project(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsigned static void project_fa(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsigned num, nlsat::literal const* lits) { std::cout << "Project "; nlsat::scoped_literal_vector result(s); - ex.main_operator(num, lits, result); + ex.compute_conflict_explanation(num, lits, result); std::cout << "(or"; for (auto l : result) { s.display(std::cout << " ", l);