mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-01 08:53:18 +00:00
Code Activity

Avoid duplicates

Browse source
This commit is contained in:
Jakob Rath 2023-02-06 16:50:34 +01:00
parent a37536e0ae
commit 984e98c88f
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -503,7 +503,7 @@ namespace polysat {
void conflict::find_deps(dependency_vector& out_deps) const { void conflict::find_deps(dependency_vector& out_deps) const {
sat::literal_vector todo_lits; sat::literal_vector todo_lits;
sat::literal_set done_lits; sat::bool_var_set done_lits;
unsigned_vector todo_vars; unsigned_vector todo_vars;
uint_set done_vars; uint_set done_vars;
indexed_uint_set deps; indexed_uint_set deps;
@ -512,13 +512,13 @@ namespace polysat {
SASSERT(s.at_base_level()); SASSERT(s.at_base_level());
auto const enqueue_lit = [&](sat::literal lit) { auto const enqueue_lit = [&](sat::literal lit) {
if (done_lits.contains(lit)) if (done_lits.contains(lit.var()))
return; return;
if (!s.m_bvars.is_assigned(lit)) if (!s.m_bvars.is_assigned(lit))
return; return;
// verbose_stream() << "enqueue " << lit_pp(s, lit) << "\n"; // verbose_stream() << "enqueue " << lit_pp(s, lit) << "\n";
todo_lits.push_back(lit); todo_lits.push_back(lit);
done_lits.insert(lit); done_lits.insert(lit.var());
}; };
auto const enqueue_constraint = [&](signed_constraint c) { auto const enqueue_constraint = [&](signed_constraint c) {
@ -586,7 +586,7 @@ namespace polysat {
for (unsigned d : deps) for (unsigned d : deps)
out_deps.push_back(dependency(d)); out_deps.push_back(dependency(d));
if (!m_dep.is_null()) if (!m_dep.is_null() && !deps.contains(m_dep.val()))
out_deps.push_back(m_dep); out_deps.push_back(m_dep);
} }