mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

fix #1471

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-02-05 18:54:14 -08:00
parent b8680f8a46
commit b2bd4dd3b4
3 changed files with 31 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/sat/sat_integrity_checker.cpp
View file

@ -153,7 +153,7 @@ namespace sat {
}
bool integrity_checker::check_watches() const {
DEBUG_CODE(
DEBUG_CODE(
vector<watch_list>::const_iterator it = s.m_watches.begin();
vector<watch_list>::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;

26
src/sat/sat_solver.cpp
View file

@ -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) {

2
src/sat/sat_solver.h
View file

@ -444,7 +444,7 @@ namespace sat {
literal_vector m_aux_literals;
svector<bin_clause> 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);