mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

debug output

Browse source
This commit is contained in:
Jakob Rath 2023-03-16 16:13:13 +01:00
parent ce04d9c73b
commit 9af86f2d68
1 changed files with 7 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1577,8 +1577,12 @@ namespace polysat {
out << "Clauses:\n"; out << "Clauses:\n";
for (clause const& cl : m_constraints.clauses()) { for (clause const& cl : m_constraints.clauses()) {
out << "\t" << cl << "\n"; out << "\t" << cl << "\n";
for (sat::literal lit : cl) for (sat::literal lit : cl) {
out << "\t\t" << lit_pp(*this, lit) << "\n"; out << "\t\t" << lit_pp(*this, lit);
if (count(m_bvars.watch(lit), &cl) != 0)
out << " (bool-watched)";
out << "\n";
}
} }
return out; return out;
} }
@ -1612,6 +1616,7 @@ namespace polysat {
else if (s.m_bvars.is_decision(lit)) else if (s.m_bvars.is_decision(lit))
out << "decide"; out << "decide";
out << '@' << s.m_bvars.level(lit); out << '@' << s.m_bvars.level(lit);
out << " idx:" << s.m_search.get_bool_index(lit);
} }
if (c->is_pwatched()) if (c->is_pwatched())
out << " pwatched"; out << " pwatched";