mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-26 05:43:33 +00:00
Code Activity

improve logging

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-11-20 10:51:39 -10:00 • committed by Nikolaj Bjorner
parent 82958565ed
commit 8f97785498
6 changed files with 99 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/nlsat/nlsat_explain.cpp
View file

@ -295,14 +295,6 @@ namespace nlsat {
if (maxx == null_var)
return;
SASSERT(m_assignment.is_assigned(maxx));
// Make sure its discriminant does not vanish at the model.
polynomial_ref disc(m_pm);
disc = discriminant(q, maxx);
int const disc_sign = sign(disc);
SASSERT(disc_sign != 0);
if (disc_sign == 0)
NOT_IMPLEMENTED_YET();
undef_var_assignment partial(m_assignment, maxx);
scoped_anum_vector & roots = m_roots_tmp;
@ -319,7 +311,7 @@ namespace nlsat {
}
if (root_idx == 0)
return; // there are no root functions and therefore no constraints aer generated
TRACE(nlsat_explain,
tout << "adding zero-assumption root literal for ";
display_var(tout, maxx); tout << " using root[" << root_idx << "] of " << q << "\n";);

6
src/nlsat/nlsat_solver.cpp
View file

@ -3368,6 +3368,12 @@ namespace nlsat {
m_am.to_rational(m_assignment.value(x), q);
m_am.qm().display_smt2(out, q, false);
}
else if (m_log_lemma_smtrat) {
std::ostringstream var_name;
proc(var_name, x);
std::string name = var_name.str();
m_am.display_root_smtrat(out, m_assignment.value(x), name.c_str());
}
else {
m_am.display_root_smt2(out, m_assignment.value(x));
}