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

fix #5068

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-08 12:39:23 -07:00
parent 9ef7cf1e81
commit 6b1642e272
1 changed files with 19 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

37
src/sat/sat_big.cpp
View file

@ -166,13 +166,14 @@ namespace sat {
bool big::in_del(literal u, literal v) const { bool big::in_del(literal u, literal v) const {
if (u.index() > v.index()) std::swap(u, v); if (u.index() > v.index())
std::swap(u, v);
return m_del_bin[u.index()].contains(v); return m_del_bin[u.index()].contains(v);
} }
void big::add_del(literal u, literal v) { void big::add_del(literal u, literal v) {
if (u.index() > v.index()) std::swap(u, v); if (u.index() > v.index())
std::swap(u, v);
m_del_bin[u.index()].push_back(v); m_del_bin[u.index()].push_back(v);
} }
@ -182,19 +183,19 @@ namespace sat {
m_del_bin.reset(); m_del_bin.reset();
m_del_bin.reserve(s.m_watches.size()); m_del_bin.reserve(s.m_watches.size());
for (watch_list & wlist : s.m_watches) { for (watch_list & wlist : s.m_watches) {
if (s.inconsistent()) break; if (s.inconsistent())
break;
literal u = to_literal(idx++); literal u = to_literal(idx++);
watch_list::iterator it = wlist.begin(); unsigned j = 0, sz = wlist.size();
watch_list::iterator itprev = it; for (unsigned i = 0; i < sz; ++i) {
watch_list::iterator end = wlist.end(); watched& w = wlist[i];
for (; it != end; ++it) {
watched& w = *it;
if (learned() ? w.is_binary_learned_clause() : w.is_binary_clause()) { if (learned() ? w.is_binary_learned_clause() : w.is_binary_clause()) {
literal v = w.get_literal(); literal v = w.get_literal();
if (u != get_parent(v) && ~u != get_parent(v) && safe_reach(u, v)) { if (u != get_parent(v) && ~u != get_parent(v) && safe_reach(u, v)) {
++elim; ++elim;
add_del(~u, v); add_del(~u, v);
if (s.get_config().m_drat) s.m_drat.del(~u, v); if (s.get_config().m_drat)
s.m_drat.del(~u, v);
s.m_mc.stackv().reset(); // TBD: brittle code s.m_mc.stackv().reset(); // TBD: brittle code
s.add_ate(~u, v); s.add_ate(~u, v);
if (find_binary_watch(wlist, ~v)) { if (find_binary_watch(wlist, ~v)) {
@ -206,22 +207,24 @@ namespace sat {
continue; continue;
} }
} }
*itprev = *it; wlist[j++] = wlist[i];
itprev++;
} }
wlist.set_end(itprev); wlist.shrink(j);
} }
s.propagate(false); s.propagate(false);
return elim; return elim;
} }
bool big::safe_reach(literal u, literal v) { bool big::safe_reach(literal u, literal v) {
if (!reaches(u, v)) return false; if (!reaches(u, v))
return false;
while (u != v) { while (u != v) {
literal w = next(u, v); literal w = next(u, v);
if (in_del(~u, w)) { if (in_del(~u, w))
return false;
// ~u is a unit. removing binary clause destroy's property
if (w == ~v)
return false; return false;
}
u = w; u = w;
} }
return true; return true;
@ -267,12 +270,10 @@ namespace sat {
for (auto& next : m_dag) { for (auto& next : m_dag) {
if (!next.empty()) { if (!next.empty()) {
out << to_literal(idx) << " : " << m_left[idx] << ":" << m_right[idx] << " -> " << next << "\n"; out << to_literal(idx) << " : " << m_left[idx] << ":" << m_right[idx] << " -> " << next << "\n";
#if 1
for (literal n : next) { for (literal n : next) {
out << n << "[" << m_left[n.index()] << ":" << m_right[n.index()] << "] "; out << n << "[" << m_left[n.index()] << ":" << m_right[n.index()] << "] ";
} }
out << "\n"; out << "\n";
#endif
} }
++idx; ++idx;
} }