mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-11 21:50:52 +00:00
Code Activity

pwatch

Browse source
This commit is contained in:
Jakob Rath 2023-11-06 11:40:48 +01:00
parent 9e90b353e9
commit f49440690d
1 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1664,8 +1664,14 @@ namespace polysat {
out << '@' << s.m_bvars.level(lit); out << '@' << s.m_bvars.level(lit);
out << " idx:" << s.m_search.get_bool_index(lit); out << " idx:" << s.m_search.get_bool_index(lit);
} }
if (c->is_pwatched()) if (c->is_pwatched()) {
out << " pwatched"; out << " pwatched(";
char const* delim = "";
for (pvar v : c->vars())
if (s.m_pwatch[v].contains(c.get()))
out << delim << "v" << v, delim = ",";
out << ")";
}
if (c->is_external()) if (c->is_external())
out << " ext"; out << " ext";
dependency const d = s.m_bvars.dep(lit); dependency const d = s.m_bvars.dep(lit);