From b2bd4dd3b4ce591aab630adb25ddf2df30e8fc5f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 5 Feb 2018 18:54:14 -0800 Subject: [PATCH] fix #1471 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_integrity_checker.cpp | 30 ++++++++++++++---------------- src/sat/sat_solver.cpp | 26 ++++++++++++++++---------- src/sat/sat_solver.h | 2 +- 3 files changed, 31 insertions(+), 27 deletions(-) diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp index 08a6072b6..027cd8a6f 100644 --- a/src/sat/sat_integrity_checker.cpp +++ b/src/sat/sat_integrity_checker.cpp @@ -153,7 +153,7 @@ namespace sat { } bool integrity_checker::check_watches() const { - DEBUG_CODE( + DEBUG_CODE( vector::const_iterator it = s.m_watches.begin(); vector::const_iterator end = s.m_watches.end(); for (unsigned l_idx = 0; it != end; ++it, ++l_idx) { @@ -165,30 +165,28 @@ namespace sat { s.display_watches(tout); s.display(tout);); SASSERT(!s.was_eliminated(l.var()) || wlist.empty()); - watch_list::const_iterator it2 = wlist.begin(); - watch_list::const_iterator end2 = wlist.end(); - for (; it2 != end2; ++it2) { - switch (it2->get_kind()) { + for (watched const& w : wlist) { + switch (w.get_kind()) { case watched::BINARY: - SASSERT(!s.was_eliminated(it2->get_literal().var())); - CTRACE("sat_watched_bug", !s.get_wlist(~(it2->get_literal())).contains(watched(l, it2->is_learned())), - tout << "l: " << l << " l2: " << it2->get_literal() << "\n"; + SASSERT(!s.was_eliminated(w.get_literal().var())); + CTRACE("sat_watched_bug", !s.get_wlist(~(w.get_literal())).contains(watched(l, w.is_learned())), + tout << "l: " << l << " l2: " << w.get_literal() << "\n"; tout << "was_eliminated1: " << s.was_eliminated(l.var()); - tout << " was_eliminated2: " << s.was_eliminated(it2->get_literal().var()); - tout << " learned: " << it2->is_learned() << "\n"; + tout << " was_eliminated2: " << s.was_eliminated(w.get_literal().var()); + tout << " learned: " << w.is_learned() << "\n"; sat::display(tout, s.m_cls_allocator, wlist); tout << "\n"; - sat::display(tout, s.m_cls_allocator, s.get_wlist(~(it2->get_literal()))); + sat::display(tout, s.m_cls_allocator, s.get_wlist(~(w.get_literal()))); tout << "\n";); - SASSERT(s.get_wlist(~(it2->get_literal())).contains(watched(l, it2->is_learned()))); + SASSERT(s.get_wlist(~(w.get_literal())).contains(watched(l, w.is_learned()))); break; case watched::TERNARY: - SASSERT(!s.was_eliminated(it2->get_literal1().var())); - SASSERT(!s.was_eliminated(it2->get_literal2().var())); - SASSERT(it2->get_literal1().index() < it2->get_literal2().index()); + SASSERT(!s.was_eliminated(w.get_literal1().var())); + SASSERT(!s.was_eliminated(w.get_literal2().var())); + SASSERT(w.get_literal1().index() < w.get_literal2().index()); break; case watched::CLAUSE: - SASSERT(!s.m_cls_allocator.get_clause(it2->get_clause_offset())->was_removed()); + SASSERT(!s.m_cls_allocator.get_clause(w.get_clause_offset())->was_removed()); break; default: break; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 4cb7339d1..f0c23e087 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -2641,15 +2641,22 @@ namespace sat { clauses.shrink(j); } - void solver::gc_bin(bool learned, literal nlit) { - m_user_bin_clauses.reset(); - collect_bin_clauses(m_user_bin_clauses, learned); - for (unsigned i = 0; i < m_user_bin_clauses.size(); ++i) { - literal l1 = m_user_bin_clauses[i].first; - literal l2 = m_user_bin_clauses[i].second; - if (nlit == l1 || nlit == l2) { - detach_bin_clause(l1, l2, learned); + void solver::gc_bin(literal lit) { + bool_var v = lit.var(); + for (watch_list& wlist : m_watches) { + watch_list::iterator it = wlist.begin(); + watch_list::iterator it2 = wlist.begin(); + watch_list::iterator end = wlist.end(); + for (; it != end; ++it) { + if (it->is_binary_clause() && it->get_literal().var() == v) { + // skip + } + else { + *it2 = *it; + ++it2; + } } + wlist.set_end(it2); } } @@ -2724,8 +2731,7 @@ namespace sat { gc_lit(m_learned, lit); gc_lit(m_clauses, lit); - gc_bin(true, lit); - gc_bin(false, lit); + gc_bin(lit); TRACE("sat", tout << "gc: " << lit << "\n"; display(tout);); --num_scopes; for (unsigned i = 0; i < m_trail.size(); ++i) { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index c011eb46d..c275b8ee2 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -444,7 +444,7 @@ namespace sat { literal_vector m_aux_literals; svector m_user_bin_clauses; void gc_lit(clause_vector& clauses, literal lit); - void gc_bin(bool learned, literal nlit); + void gc_bin(literal lit); void gc_var(bool_var v); bool_var max_var(clause_vector& clauses, bool_var v);