diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp index 31a4bba72..d27820e71 100644 --- a/src/sat/sat_clause.cpp +++ b/src/sat/sat_clause.cpp @@ -94,6 +94,11 @@ namespace sat { mark_strengthened(); } } + + void clause::restore(unsigned num_lits) { + SASSERT(num_lits <= m_capacity); + m_size = num_lits; + } bool clause::satisfied_by(model const & m) const { for (literal l : *this) { diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index f95696b3d..ca46063ac 100644 --- a/src/sat/sat_clause.h +++ b/src/sat/sat_clause.h @@ -68,6 +68,7 @@ namespace sat { bool is_learned() const { return m_learned; } void set_learned(bool l) { SASSERT(is_learned() != l); m_learned = l; } void shrink(unsigned num_lits); + void restore(unsigned num_lits); bool strengthened() const { return m_strengthened; } void mark_strengthened() { m_strengthened = true; update_approx(); } void unmark_strengthened() { m_strengthened = false; } diff --git a/src/sat/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp index 4a3fb82b4..f0c76b466 100644 --- a/src/sat/sat_cleaner.cpp +++ b/src/sat/sat_cleaner.cpp @@ -135,7 +135,7 @@ namespace sat { break; default: SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef); - if (s.m_config.m_drat && new_sz < i) { + if (s.m_config.m_drat && new_sz < sz) { tmp.set(c.size(), c.begin(), c.is_learned()); } c.shrink(new_sz); @@ -144,7 +144,7 @@ namespace sat { if (!c.frozen()) { s.attach_clause(c); } - if (s.m_config.m_drat && new_sz < i) { + if (s.m_config.m_drat && new_sz < sz) { // for optimization, could also report deletion // of previous version of clause. s.m_drat.add(c, true); diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 4707fa0ac..ca45bd971 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -68,7 +68,7 @@ namespace sat { case status::asserted: return; case status::external: return; // requires extension to drat format. case status::learned: break; - case status::deleted: (*m_out) << "d "; break; + case status::deleted: return; (*m_out) << "d "; break; } for (unsigned i = 0; i < n; ++i) (*m_out) << c[i] << " "; (*m_out) << "0\n"; @@ -215,18 +215,12 @@ namespace sat { if (!m_inconsistent) { DEBUG_CODE(validate_propagation();); } - for (unsigned i = 0; i < m_units.size(); ++i) { - SASSERT(m_assignment[m_units[i].var()] != l_undef); - } + DEBUG_CODE( + for (literal u : m_units) { + SASSERT(m_assignment[u.var()] != l_undef); + }); - for (unsigned i = num_units; i < m_units.size(); ++i) { - m_assignment[m_units[i].var()] = l_undef; - } - m_units.resize(num_units); - bool ok = m_inconsistent; - m_inconsistent = false; - - if (!ok) { + if (!m_inconsistent) { literal_vector lits(n, c); IF_VERBOSE(0, verbose_stream() << "not drup " << lits << "\n"); for (unsigned v = 0; v < m_assignment.size(); ++v) { @@ -274,6 +268,13 @@ namespace sat { IF_VERBOSE(0, s.display(verbose_stream())); exit(0); } + for (unsigned i = num_units; i < m_units.size(); ++i) { + m_assignment[m_units[i].var()] = l_undef; + } + m_units.resize(num_units); + bool ok = m_inconsistent; + m_inconsistent = false; + return ok; } @@ -344,6 +345,7 @@ namespace sat { } bool drat::contains(unsigned n, literal const* lits) { + if (!m_check) return true; for (unsigned i = m_proof.size(); i-- > 0; ) { clause& c = *m_proof[i]; status st = m_status[i]; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 4feeb4b05..34f89c3aa 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -125,8 +125,9 @@ namespace sat { } inline void simplifier::remove_clause_core(clause & c) { - for (literal l : c) + for (literal l : c) { insert_elim_todo(l.var()); + } m_sub_todo.erase(c); c.set_removed(true); TRACE("resolution_bug", tout << "del_clause: " << c << "\n";); @@ -330,35 +331,40 @@ namespace sat { } } + unsigned sz0 = c.size(); if (cleanup_clause(c, in_use_lists)) { s.del_clause(c); continue; } unsigned sz = c.size(); - if (sz == 0) { + switch(sz) { + case 0: s.set_conflict(justification()); for (; it != end; ++it, ++it2) { *it2 = *it; } - break; - } - if (sz == 1) { + cs.set_end(it2); + return; + case 1: s.assign(c[0], justification()); + c.restore(sz0); s.del_clause(c); - continue; - } - if (sz == 2) { + break; + case 2: s.mk_bin_clause(c[0], c[1], c.is_learned()); - s.del_clause(c, false); - continue; - } - *it2 = *it; - it2++; - if (!c.frozen()) { - s.attach_clause(c); - if (s.m_config.m_drat) { - s.m_drat.add(c, true); + c.restore(sz0); + s.del_clause(c, true); + break; + default: + *it2 = *it; + it2++; + if (!c.frozen()) { + s.attach_clause(c); + if (sz != sz0 && s.m_config.m_drat) { + s.m_drat.add(c, true); + } } + break; } } cs.set_end(it2); @@ -679,9 +685,15 @@ namespace sat { m_need_cleanup = true; m_num_elim_lits++; insert_elim_todo(l.var()); - c.elim(l); - if (s.m_config.m_drat) s.m_drat.add(c, true); - // if (s.m_config.m_drat) s.m_drat.del(c0); // can delete previous version + if (s.m_config.m_drat && c.contains(l)) { + m_dummy.set(c.size(), c.begin(), c.is_learned()); + c.elim(l); + s.m_drat.add(c, true); + s.m_drat.del(*m_dummy.get()); + } + else { + c.elim(l); + } clause_use_list & occurs = m_use_list.get(l); occurs.erase_not_removed(c); m_sub_counter -= occurs.size()/2; @@ -695,23 +707,23 @@ namespace sat { case 0: TRACE("elim_lit", tout << "clause is empty\n";); s.set_conflict(justification()); - return; + break; case 1: TRACE("elim_lit", tout << "clause became unit: " << c[0] << "\n";); propagate_unit(c[0]); // propagate_unit will delete c. // remove_clause(c); - return; + break; case 2: TRACE("elim_lit", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";); s.mk_bin_clause(c[0], c[1], c.is_learned()); m_sub_bin_todo.push_back(bin_clause(c[0], c[1], c.is_learned())); remove_clause(c); - return; + break; default: TRACE("elim_lit", tout << "result: " << c << "\n";); m_sub_todo.insert(c); - return; + break; } } @@ -876,27 +888,30 @@ namespace sat { m_sub_counter--; TRACE("subsumption", tout << "next: " << c << "\n";); if (s.m_trail.size() > m_last_sub_trail_sz) { + unsigned sz0 = c.size(); if (cleanup_clause(c, true /* clause is in the use_lists */)) { remove_clause(c); continue; } unsigned sz = c.size(); - if (sz == 0) { + switch (sz) { + case 0: s.set_conflict(justification()); return; - } - if (sz == 1) { + case 1: propagate_unit(c[0]); // propagate_unit will delete c. // remove_clause(c); continue; - } - if (sz == 2) { + case 2: TRACE("subsumption", tout << "clause became binary: " << c << "\n";); s.mk_bin_clause(c[0], c[1], c.is_learned()); m_sub_bin_todo.push_back(bin_clause(c[0], c[1], c.is_learned())); + c.restore(sz0); remove_clause(c); continue; + default: + break; } } TRACE("subsumption", tout << "using: " << c << "\n";); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 6731adc92..6f181dcc9 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -344,11 +344,11 @@ namespace sat { void solver::mk_bin_clause(literal l1, literal l2, bool learned) { if (find_binary_watch(get_wlist(~l1), ~l2)) { - assign(l1, justification()); + assign_core(l1, 0, justification(l2)); return; } if (find_binary_watch(get_wlist(~l2), ~l1)) { - assign(l2, justification()); + assign_core(l2, 0, justification(l1)); return; } watched* w0 = find_binary_watch(get_wlist(~l1), l2); @@ -759,17 +759,20 @@ namespace sat { m_not_l = not_l; } - void solver::assign_core(literal l, unsigned lvl, justification j) { + void solver::assign_core(literal l, unsigned _lvl, justification j) { SASSERT(value(l) == l_undef); TRACE("sat_assign_core", tout << l << " " << j << " level: " << lvl << "\n";); + if (_lvl == 0 && m_config.m_drat) { + m_drat.add(l, !j.is_none()); + } + if (at_base_lvl()) { - if (m_config.m_drat) m_drat.add(l, !j.is_none()); j = justification(); // erase justification for level 0 } m_assignment[l.index()] = l_true; m_assignment[(~l).index()] = l_false; bool_var v = l.var(); - m_level[v] = lvl; + m_level[v] = scope_lvl(); m_justification[v] = j; m_phase[v] = static_cast(l.sign()); m_assigned_since_gc[v] = true; @@ -2263,6 +2266,7 @@ namespace sat { bool solver::resolve_conflict_core() { + m_conflicts_since_init++; m_conflicts_since_restart++; m_conflicts_since_gc++; @@ -2378,6 +2382,7 @@ namespace sat { while (num_marks > 0); m_lemma[0] = ~consequent; + m_drat.verify(m_lemma.size(), m_lemma.c_ptr()); learn_lemma_and_backjump(); return true; } @@ -2409,7 +2414,6 @@ namespace sat { unsigned glue = num_diff_levels(m_lemma.size(), m_lemma.c_ptr()); m_fast_glue_avg.update(glue); m_slow_glue_avg.update(glue); - pop_reinit(m_scope_lvl - new_scope_lvl); TRACE("sat_conflict_detail", tout << new_scope_lvl << "\n"; display(tout);); // unsound: m_asymm_branch.minimize(m_scc, m_lemma); @@ -2879,20 +2883,16 @@ namespace sat { void solver::minimize_lemma() { SASSERT(!m_lemma.empty()); SASSERT(m_unmark.empty()); - //m_unmark.reset(); updt_lemma_lvl_set(); unsigned sz = m_lemma.size(); unsigned i = 1; // the first literal is the FUIP unsigned j = 1; - //bool drop = false; - //unsigned bound = sz/5+10; for (; i < sz; i++) { literal l = m_lemma[i]; if (implied_by_marked(l)) { TRACE("sat", tout << "drop: " << l << "\n";); m_unmark.push_back(l.var()); - //drop = true; } else { if (j != i) { @@ -2900,12 +2900,6 @@ namespace sat { } j++; } -#if 0 - if (!drop && i >= bound) { - j = sz; - break; - } -#endif } reset_unmark(0);