mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

format

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-04-22 17:25:24 +01:00
parent 81189d6fdd
commit 5a2c92f4af
1 changed files with 7 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/util/max_cliques.h
View file

@ -38,9 +38,8 @@ class max_cliques : public T {
m_todo.push_back(p); m_todo.push_back(p);
for (unsigned i = 0; i < m_todo.size(); ++i) { for (unsigned i = 0; i < m_todo.size(); ++i) {
p = m_todo[i]; p = m_todo[i];
if (m_seen1.contains(p)) { if (m_seen1.contains(p))
continue; continue;
}
m_seen1.insert(p); m_seen1.insert(p);
if (m_seen2.contains(p)) { if (m_seen2.contains(p)) {
unsigned_vector const& tc = m_tc[p]; unsigned_vector const& tc = m_tc[p];
@ -50,14 +49,12 @@ class max_cliques : public T {
} }
else { else {
unsigned np = negate(p); unsigned np = negate(p);
if (goal.contains(np)) { if (goal.contains(np))
reachable.insert(np); reachable.insert(np);
}
m_todo.append(next(np)); m_todo.append(next(np));
} }
} }
for (unsigned i = m_todo.size(); i > 0; ) { for (unsigned i = m_todo.size(); i-- > 0; ) {
--i;
p = m_todo[i]; p = m_todo[i];
if (m_seen2.contains(p)) if (m_seen2.contains(p))
continue; continue;
@ -209,9 +206,8 @@ public:
unsigned_vector mux; unsigned_vector mux;
for (unsigned x : am1) for (unsigned x : am1)
mux.push_back(x); mux.push_back(x);
if (mux.size() == 2 && mux[0] == negate(mux[1])) { if (mux.size() == 2 && mux[0] == negate(mux[1]))
continue; continue;
}
cliques.push_back(mux); cliques.push_back(mux);
} }
} }