mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-05 17:47:41 +00:00
Code Activity

rename explain::main_operator to compute_conflict_explanation

Browse source
This commit is contained in:
Lev Nachmanson 2025-08-27 10:05:31 -10:00
parent 5654f149e7
commit c87e7c312a
4 changed files with 10 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/nlsat/nlsat_explain.cpp
View file

@ -1220,8 +1220,8 @@ namespace nlsat {
// Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore // Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore
polynomial_ref_vector samples(m_pm); polynomial_ref_vector samples(m_pm);
levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am); // levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am);
auto cell = lws.single_cell(); //auto cell = lws.single_cell();
if (x < max_x) if (x < max_x)
cac_add_cell_lits(ps, x, samples); 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(check_already_added());
SASSERT(num > 0); SASSERT(num > 0);
TRACE(nlsat_explain, TRACE(nlsat_explain,
@ -2104,11 +2104,11 @@ namespace nlsat {
} }
void explain::set_signed_project(bool f) { 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) { void explain::compute_conflict_explanation(unsigned n, literal const * ls, scoped_literal_vector & result) {
(*m_imp)(n, ls, result); m_imp->compute_conflict_explanation(n, ls, result);
} }
void explain::project(var x, unsigned n, literal const * ls, scoped_literal_vector & result) { void explain::project(var x, unsigned n, literal const * ls, scoped_literal_vector & result) {

2
src/nlsat/nlsat_explain.h
View file

@ -63,7 +63,7 @@ namespace nlsat {
- s_1, ..., s_m do not contain variable x. - s_1, ..., s_m do not contain variable x.
- s_1, ..., s_m are false in the current interpretation - 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);
/** /**

3
src/nlsat/nlsat_solver.cpp
View file

@ -2215,12 +2215,13 @@ namespace nlsat {
m_lazy_clause.reset(); 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++) for (unsigned i = 0; i < sz; i++)
m_lazy_clause.push_back(~jst.lit(i)); m_lazy_clause.push_back(~jst.lit(i));
// lazy clause is a valid clause // lazy clause is a valid clause
TRACE(nlsat_mathematica, display_mathematica_lemma(tout, m_lazy_clause.size(), m_lazy_clause.data());); TRACE(nlsat_mathematica, display_mathematica_lemma(tout, m_lazy_clause.size(), m_lazy_clause.data()););
exit(0);
if (m_dump_mathematica) { if (m_dump_mathematica) {
// verbose_stream() << "lazy clause\n"; // verbose_stream() << "lazy clause\n";
display_mathematica_lemma(verbose_stream(), m_lazy_clause.size(), m_lazy_clause.data()) << std::endl; display_mathematica_lemma(verbose_stream(), m_lazy_clause.size(), m_lazy_clause.data()) << std::endl;

2
src/test/nlsat.cpp
View file

@ -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) { static void project_fa(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsigned num, nlsat::literal const* lits) {
std::cout << "Project "; std::cout << "Project ";
nlsat::scoped_literal_vector result(s); nlsat::scoped_literal_vector result(s);
ex.main_operator(num, lits, result); ex.compute_conflict_explanation(num, lits, result);
std::cout << "(or"; std::cout << "(or";
for (auto l : result) { for (auto l : result) {
s.display(std::cout << " ", l); s.display(std::cout << " ", l);