mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-31 16:29:52 +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 fbc7f6c77d
commit 2e810e3aaa
3 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/nlsat/nlsat_explain.cpp
View file

@ -1671,7 +1671,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,
@ -1877,8 +1877,8 @@ namespace nlsat {
m_imp->m_add_zero_disc = 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) {

2
src/nlsat/nlsat_explain.h
View file

@ -64,7 +64,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);
/**

2
src/test/nlsat.cpp
View file

@ -320,7 +320,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);