mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

nicer output

Browse source
This commit is contained in:
Jakob Rath 2023-03-23 13:39:01 +01:00
parent f0ac81a149
commit 50814c952a
2 changed files with 10 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/math/polysat/search_state.cpp
View file

@ -38,24 +38,12 @@ namespace polysat {
}
case search_item_k::boolean: {
sat::literal const lit = item.lit();
out << rpad(4, lit);
out << ": " << rpad(32, s.lit2cnstr(lit));
out << " @" << s.m_bvars.level(lit);
if (s.m_bvars.is_assumption(lit))
out << " assumption";
else if (s.m_bvars.is_bool_propagation(lit)) {
out << lit_pp(s, lit);
if (s.m_bvars.is_bool_propagation(lit)) {
clause* reason = s.m_bvars.reason(lit);
out << " bool propagation " << show_deref(reason);
for (auto l2 : *reason) {
out << "\n\t" << rpad(4, l2) << ": " << rpad(16, s.lit2cnstr(l2)) << " " << bool_justification_pp(s.m_bvars, l2);
}
}
else if (s.m_bvars.is_evaluation(lit)) {
out << " evaluated";
}
else {
SASSERT(s.m_bvars.is_decision(lit));
out << " decision";
out << "\n\treason " << show_deref(reason);
for (auto l2 : *reason)
out << "\n\t" << lit_pp(s, l2);
}
return out;
}

8
src/math/polysat/solver.cpp
View file

@ -1529,15 +1529,17 @@ namespace polysat {
}
);
#if ENABLE_LEMMA_VALIDITY_CHECK
clause_builder clauseBuilder(*this);
clause_builder cb(*this, "unsat core check");
for (auto d : deps) {
for (sat::bool_var b = 0; b < m_bvars.size(); ++b) {
if (m_bvars.dep(b) != d)
continue;
clauseBuilder.insert(sat::literal(b, m_bvars.value(b) != l_false));
sat::literal lit(b, m_bvars.value(b) == l_false);
VERIFY(m_bvars.is_true(lit));
cb.insert(~lit);
}
}
log_lemma_smt2(*clauseBuilder.build()); // check the unsat-core
log_lemma_smt2(*cb.build()); // check the unsat core
#endif
}