mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

mark

Browse source
This commit is contained in:
Jakob Rath 2023-10-24 11:22:04 +02:00
parent ebeb1296fd
commit 045b5ed683
1 changed files with 14 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/math/polysat/slicing.cpp
View file

@ -802,17 +802,26 @@ namespace polysat {
dep_t const d = dep_t::decode(dp); dep_t const d = dep_t::decode(dp);
if (d.is_null()) if (d.is_null())
continue; continue;
if (d.is_lit()) if (d.is_lit()) {
on_lit(d.lit()); sat::literal const lit = d.lit();
if (!m_marked_lits.contains(lit)) {
on_lit(lit);
m_marked_lits.insert(lit);
}
}
else { else {
SASSERT(d.is_value()); SASSERT(d.is_value());
if (get_dep_lit(d) == sat::null_literal) sat::literal const lit = get_dep_lit(d);
if (lit == sat::null_literal)
on_var(get_dep_var(d)); on_var(get_dep_var(d));
else else if (!m_marked_lits.contains(lit)) {
on_lit(get_dep_lit(d)); on_lit(lit);
m_marked_lits.insert(lit);
}
} }
} }
m_tmp_deps.reset(); m_tmp_deps.reset();
m_marked_lits.reset();
} }
void slicing::explain_value(pvar v, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var) { void slicing::explain_value(pvar v, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var) {