mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-08 10:07:59 +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 a3d0bc049c
commit 5da5bed466
3 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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);