mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

fix #6143

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-07-11 12:09:15 -07:00
parent 8b29f40152
commit 5c54d6564b
1 changed files with 16 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/sat/sat_simplifier.cpp
View file

@ -1787,6 +1787,7 @@ namespace sat {
clause& c = it.curr(); clause& c = it.curr();
if (!c.is_learned() && !c.was_removed()) { if (!c.is_learned() && !c.was_removed()) {
r.push_back(clause_wrapper(c)); r.push_back(clause_wrapper(c));
SASSERT(r.back().contains(l));
SASSERT(r.back().size() == c.size()); SASSERT(r.back().size() == c.size());
} }
} }
@ -1808,9 +1809,13 @@ namespace sat {
Return false if the result is a tautology Return false if the result is a tautology
*/ */
bool simplifier::resolve(clause_wrapper const & c1, clause_wrapper const & c2, literal l, literal_vector & r) { bool simplifier::resolve(clause_wrapper const & c1, clause_wrapper const & c2, literal l, literal_vector & r) {
CTRACE("resolve_bug", !c1.contains(l), tout << c1 << "\n" << c2 << "\nl: " << l << "\n";); CTRACE("resolve_bug", !c1.contains(l) || !c2.contains(~l), tout << c1 << "\n" << c2 << "\nl: " << l << "\n";);
if (m_visited.size() <= 2*s.num_vars()) if (m_visited.size() <= 2*s.num_vars())
m_visited.resize(2*s.num_vars(), false); m_visited.resize(2*s.num_vars(), false);
if (c1.was_removed())
return false;
if (c2.was_removed())
return false;
SASSERT(c1.contains(l)); SASSERT(c1.contains(l));
SASSERT(c2.contains(~l)); SASSERT(c2.contains(~l));
bool res = true; bool res = true;
@ -1973,7 +1978,14 @@ namespace sat {
} }
} }
} }
TRACE("sat_simplifier", tout << "eliminate " << v << ", before: " << before_clauses << " after: " << after_clauses << "\n";); TRACE("sat_simplifier", tout << "eliminate " << v << ", before: " << before_clauses << " after: " << after_clauses << "\n";
tout << "pos\n";
for (auto & c : m_pos_cls)
tout << c << "\n";
tout << "neg\n";
for (auto & c : m_neg_cls)
tout << c << "\n";
);
m_elim_counter -= num_pos * num_neg + before_lits; m_elim_counter -= num_pos * num_neg + before_lits;
m_elim_counter -= num_pos * num_neg + before_lits; m_elim_counter -= num_pos * num_neg + before_lits;
@ -1988,6 +2000,8 @@ namespace sat {
m_elim_counter -= num_pos * num_neg + before_lits; m_elim_counter -= num_pos * num_neg + before_lits;
for (auto & c1 : m_pos_cls) { for (auto & c1 : m_pos_cls) {
if (c1.was_removed())
continue;
for (auto & c2 : m_neg_cls) { for (auto & c2 : m_neg_cls) {
m_new_cls.reset(); m_new_cls.reset();
if (!resolve(c1, c2, pos_l, m_new_cls)) if (!resolve(c1, c2, pos_l, m_new_cls))