From 2739342abab997e671b6cd8badd56eff76f129f0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Jan 2018 23:41:04 -0800 Subject: [PATCH] fix updates to cce Signed-off-by: Nikolaj Bjorner --- src/sat/ba_solver.cpp | 2 +- src/sat/sat_asymm_branch.cpp | 13 +- src/sat/sat_clause.cpp | 9 + src/sat/sat_clause.h | 2 +- src/sat/sat_cleaner.cpp | 5 +- src/sat/sat_elim_eqs.cpp | 4 +- src/sat/sat_elim_vars.cpp | 4 +- src/sat/sat_iff3_finder.cpp | 2 +- src/sat/sat_integrity_checker.cpp | 10 +- src/sat/sat_lookahead.cpp | 1 + src/sat/sat_simplifier.cpp | 371 ++++++++++++++---------------- src/sat/sat_simplifier.h | 17 +- src/sat/sat_solver.cpp | 32 +-- src/sat/sat_solver.h | 2 + src/sat/sat_watched.cpp | 18 +- src/sat/sat_watched.h | 10 +- 16 files changed, 248 insertions(+), 254 deletions(-) diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index 55a7713ce..42a78b5f1 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -2798,7 +2798,7 @@ namespace sat { } unsigned ba_solver::get_num_unblocked_bin(literal l) { - return s().m_simplifier.get_num_unblocked_bin(l); + return s().m_simplifier.num_nonlearned_bin(l); } /* diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 1b37e4dbc..b05de55e6 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -60,7 +60,7 @@ namespace sat { verbose_stream() << " (sat-asymm-branch :elim-literals " << (num_total - num_learned) << " :elim-learned-literals " << num_learned - << " :hidden-tautologies " << (m_asymm_branch.m_hidden_tautologies - m_hidden_tautologies) + << " :hte " << (m_asymm_branch.m_hidden_tautologies - m_hidden_tautologies) << " :cost " << m_asymm_branch.m_counter << mem_stat() << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";); @@ -124,13 +124,13 @@ namespace sat { break; } SASSERT(s.m_qhead == s.m_trail.size()); - if (m_counter < limit || s.inconsistent()) { + clause & c = *(*it); + if (m_counter < limit || s.inconsistent() || c.was_removed()) { *it2 = *it; ++it2; continue; } - s.checkpoint(); - clause & c = *(*it); + s.checkpoint(); if (big ? !process_sampled(*big, c) : !process(c)) { continue; // clause was removed } @@ -431,7 +431,8 @@ namespace sat { bool asymm_branch::process_sampled(big& big, clause & c) { scoped_detach scoped_d(s, c); sort(big, c); - if ((c.is_learned() || !big.learned()) && uhte(big, c)) { + if (!big.learned() && !c.is_learned() && uhte(big, c)) { + // TBD: mark clause as learned. ++m_hidden_tautologies; scoped_d.del_clause(); return false; @@ -501,7 +502,7 @@ namespace sat { void asymm_branch::collect_statistics(statistics & st) const { st.update("elim literals", m_elim_literals); - st.update("hidden tautologies", m_hidden_tautologies); + st.update("hte", m_hidden_tautologies); } void asymm_branch::reset_statistics() { diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp index 3600ac1a3..f433f884d 100644 --- a/src/sat/sat_clause.cpp +++ b/src/sat/sat_clause.cpp @@ -87,6 +87,15 @@ namespace sat { mark_strengthened(); } + void clause::shrink(unsigned num_lits) { + SASSERT(num_lits <= m_size); + if (num_lits < m_size) { + m_size = num_lits; + mark_strengthened(); + } + } + + bool clause::satisfied_by(model const & m) const { for (literal l : *this) { if (l.sign()) { diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index f9e3bb33f..c7273f57d 100644 --- a/src/sat/sat_clause.h +++ b/src/sat/sat_clause.h @@ -66,7 +66,7 @@ namespace sat { literal const & operator[](unsigned idx) const { SASSERT(idx < m_size); return m_lits[idx]; } bool is_learned() const { return m_learned; } void set_learned(bool l) { SASSERT(is_learned() != l); m_learned = l; } - void shrink(unsigned num_lits) { SASSERT(num_lits <= m_size); if (num_lits < m_size) { m_size = num_lits; mark_strengthened(); } } + void shrink(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 286cc1661..3d0899692 100644 --- a/src/sat/sat_cleaner.cpp +++ b/src/sat/sat_cleaner.cpp @@ -145,10 +145,7 @@ namespace sat { *it2 = *it; it2++; if (!c.frozen()) { - if (new_sz == 3) - s.attach_ter_clause(c); - else - s.attach_nary_clause(c); + s.attach_clause(c); } if (s.m_config.m_drat) { // for optimization, could also report deletion diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp index 270ae9d04..b178c52e2 100644 --- a/src/sat/sat_elim_eqs.cpp +++ b/src/sat/sat_elim_eqs.cpp @@ -95,10 +95,10 @@ namespace sat { m_solver.detach_clause(c); // apply substitution for (i = 0; i < sz; i++) { - literal lit = c[i]; + literal lit = c[i]; c[i] = norm(roots, lit); VERIFY(c[i] == norm(roots, c[i])); - VERIFY(!m_solver.was_eliminated(c[i].var()) || lit == c[i]); + VERIFY(!m_solver.was_eliminated(c[i].var()) || lit == c[i]); } std::sort(c.begin(), c.end()); for (literal l : c) VERIFY(l == norm(roots, l)); diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp index 0adcc95ef..34f871a8f 100644 --- a/src/sat/sat_elim_vars.cpp +++ b/src/sat/sat_elim_vars.cpp @@ -37,9 +37,9 @@ namespace sat{ literal pos_l(v, false); literal neg_l(v, true); - unsigned num_bin_pos = simp.get_num_unblocked_bin(pos_l); + unsigned num_bin_pos = simp.num_nonlearned_bin(pos_l); if (num_bin_pos > m_max_literals) return false; - unsigned num_bin_neg = simp.get_num_unblocked_bin(neg_l); + unsigned num_bin_neg = simp.num_nonlearned_bin(neg_l); if (num_bin_neg > m_max_literals) return false; clause_use_list & pos_occs = simp.m_use_list.get(pos_l); clause_use_list & neg_occs = simp.m_use_list.get(neg_l); diff --git a/src/sat/sat_iff3_finder.cpp b/src/sat/sat_iff3_finder.cpp index 8bbfc0ce0..af7a6f438 100644 --- a/src/sat/sat_iff3_finder.cpp +++ b/src/sat/sat_iff3_finder.cpp @@ -73,7 +73,7 @@ namespace sat { It assumes wlist have been sorted using iff3_lt */ static bool contains(watch_list const & wlist, literal l1, literal l2) { - watched k(l1, l2, false); + watched k(l1, l2); if (wlist.size() < SMALL_WLIST) return wlist.contains(k); iff3_lt lt; diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp index d09fb9581..d581dbd36 100644 --- a/src/sat/sat_integrity_checker.cpp +++ b/src/sat/sat_integrity_checker.cpp @@ -28,8 +28,8 @@ namespace sat { } // for ternary clauses - static bool contains_watched(watch_list const & wlist, literal l1, literal l2, bool learned) { - return wlist.contains(watched(l1, l2, learned)); + static bool contains_watched(watch_list const & wlist, literal l1, literal l2) { + return wlist.contains(watched(l1, l2)); } // for nary clauses @@ -68,9 +68,9 @@ namespace sat { tout << "watch_list:\n"; sat::display_watch_list(tout, s.m_cls_allocator, s.get_wlist(~c[0])); tout << "\n";); - VERIFY(contains_watched(s.get_wlist(~c[0]), c[1], c[2], c.is_learned())); - VERIFY(contains_watched(s.get_wlist(~c[1]), c[0], c[2], c.is_learned())); - VERIFY(contains_watched(s.get_wlist(~c[2]), c[0], c[1], c.is_learned())); + VERIFY(contains_watched(s.get_wlist(~c[0]), c[1], c[2])); + VERIFY(contains_watched(s.get_wlist(~c[1]), c[0], c[2])); + VERIFY(contains_watched(s.get_wlist(~c[2]), c[0], c[1])); } else { if (s.value(c[0]) == l_false || s.value(c[1]) == l_false) { diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 94f73dffc..5bf3a194d 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2306,6 +2306,7 @@ namespace sat { roots[v] = p; VERIFY(get_parent(p) == p); VERIFY(get_parent(~p) == ~p); + IF_VERBOSE(0, verbose_stream() << p << " " << q << "\n";); } } IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :equivalences " << to_elim.size() << ")\n";); diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index c7addcffc..3e7b32eb4 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -148,27 +148,17 @@ namespace sat { m_use_list.erase(c, l); } - inline void simplifier::block_clause(clause & c) { - if (m_retain_blocked_clauses) { - m_need_cleanup = true; - s.set_learned(c, true); - m_use_list.block(c); - } - else { - remove_clause(c); - } - + inline void simplifier::set_learned(clause & c) { + m_need_cleanup = true; + s.set_learned(c, true); + m_use_list.block(c); } - inline void simplifier::unblock_clause(clause & c) { - s.set_learned(c, false); - m_use_list.unblock(c); - } - - inline void simplifier::remove_bin_clause_half(literal l1, literal l2, bool learned) { - get_wlist(~l1).erase(watched(l2, learned)); - m_sub_bin_todo.erase(bin_clause(l1, l2, learned)); - m_sub_bin_todo.erase(bin_clause(l2, l1, learned)); + inline void simplifier::set_learned(literal l1, literal l2) { + m_sub_bin_todo.erase(bin_clause(l1, l2, false)); + m_sub_bin_todo.erase(bin_clause(l2, l1, false)); + m_sub_bin_todo.push_back(bin_clause(l1, l2, true)); + m_sub_bin_todo.push_back(bin_clause(l2, l1, true)); } void simplifier::init_visited() { @@ -308,13 +298,16 @@ namespace sat { clause_vector::iterator it = cs.begin(); clause_vector::iterator it2 = it; clause_vector::iterator end = cs.end(); + unsigned nm = 0; for (; it != end; ++it) { clause & c = *(*it); if (learned && !c.is_learned()) { s.m_clauses.push_back(&c); + ++nm; } else if (!learned && c.is_learned()) { s.m_learned.push_back(&c); + ++nm; } else { *it2 = *it; @@ -322,6 +315,7 @@ namespace sat { } } cs.set_end(it2); + IF_VERBOSE(0, verbose_stream() << "num moved: " << nm << "\n";); } void simplifier::cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists) { @@ -373,19 +367,10 @@ namespace sat { s.del_clause(c); continue; } - // clause became a learned clause - if (!learned && c.is_learned()) { - SASSERT(!c.frozen()); - s.m_learned.push_back(&c); - continue; - } *it2 = *it; it2++; if (!c.frozen()) { - if (sz == 3) - s.attach_ter_clause(c); - else - s.attach_nary_clause(c); + s.attach_clause(c); if (s.m_config.m_drat) { s.m_drat.add(c, true); } @@ -895,6 +880,10 @@ namespace sat { break; clause & c = m_sub_todo.erase(); + if (c.id() == 60127) { + IF_VERBOSE(0, verbose_stream() << "subsume " << c << "\n";); + } + c.unmark_strengthened(); m_sub_counter--; TRACE("subsumption", tout << "next: " << c << "\n";); @@ -904,6 +893,9 @@ namespace sat { continue; } unsigned sz = c.size(); + if (c.id() == 60127) { + IF_VERBOSE(0, verbose_stream() << "subsume " << c << "\n";); + } if (sz == 0) { s.set_conflict(justification()); return; @@ -990,11 +982,11 @@ namespace sat { int m_counter; model_converter & mc; queue m_queue; - clause_vector m_to_remove; literal_vector m_covered_clause; svector m_covered_antecedent; literal_vector m_intersection; + literal_vector m_tautology; literal_vector m_new_intersection; literal_vector m_blocked_binary; svector m_in_intersection; @@ -1084,39 +1076,25 @@ namespace sat { model_converter::entry* new_entry = 0; watch_list & wlist = s.get_wlist(~l); m_counter -= wlist.size(); - watch_list::iterator it = wlist.begin(); - watch_list::iterator it2 = it; - watch_list::iterator end = wlist.end(); - - for (; it != end; ++it) { - if (!it->is_binary_non_learned_clause()) { - *it2 = *it; it2++; + for (watched& w : wlist) { + if (!w.is_binary_non_learned_clause()) { continue; } - literal l2 = it->get_literal(); + literal l2 = w.get_literal(); s.mark_visited(l2); if (all_tautology(l)) { - block_binary(it, l, new_entry); - s.m_num_blocked_clauses++; + block_binary(w, l, new_entry); + w.set_learned(true); + s.s.set_learned1(l2, l, true); + s.m_num_bce++; m_blocked_binary.push_back(l2); } - else { - *it2 = *it; it2++; - } s.unmark_visited(l2); } - wlist.set_end(it2); - if (s.m_retain_blocked_clauses && !m_blocked_binary.empty()) { - IF_VERBOSE(0, verbose_stream() << "retaining " << m_blocked_binary.size() << " binary clauses\n";); - for (literal lit2 : m_blocked_binary) { - s.s.mk_bin_clause(l, lit2, true); - } - } } void process_clauses(literal l) { model_converter::entry* new_entry = 0; - m_to_remove.reset(); clause_use_list & occs = s.m_use_list.get(l); clause_use_list::iterator it = occs.mk_iterator(); for (; !it.at_end(); it.next()) { @@ -1127,12 +1105,11 @@ namespace sat { s.mark_all_but(c, l); if (all_tautology(l)) { block_clause(c, l, new_entry); - s.m_num_blocked_clauses++; + s.m_num_bce++; + s.set_learned(c); } s.unmark_all(c); - } - for (clause* c : m_to_remove) - s.block_clause(*c); + } } void reset_intersection() { @@ -1155,6 +1132,7 @@ namespace sat { if (!process_var(l.var())) return false; bool first = true; reset_intersection(); + m_tautology.reset(); for (watched & w : s.get_wlist(l)) { // when adding a blocked clause, then all non-learned clauses have to be considered for the // resolution intersection. @@ -1162,6 +1140,7 @@ namespace sat { if (process_bin) { literal lit = w.get_literal(); if (s.is_marked(~lit) && lit != ~l) { + m_tautology.push_back(~lit); continue; // tautology } if (!first || s.is_marked(lit)) { @@ -1178,8 +1157,10 @@ namespace sat { bool tautology = false; clause & c = it.curr(); if (c.is_learned() && !adding) continue; + if (c.was_removed()) continue; for (literal lit : c) { if (s.is_marked(~lit) && lit != ~l) { + m_tautology.push_back(~lit); tautology = true; break; } @@ -1204,25 +1185,30 @@ namespace sat { return false; } } + // if (first) IF_VERBOSE(0, verbose_stream() << "taut: " << m_tautology << "\n";); return first; } bool check_abce_tautology(literal l) { + m_tautology.reset(); if (!process_var(l.var())) return false; for (watched & w : s.get_wlist(l)) { if (w.is_binary_non_learned_clause()) { literal lit = w.get_literal(); - if (!s.is_marked(~lit) || lit == ~l) return false; + VERIFY(lit != ~l); + if (!s.is_marked(~lit)) return false; + m_tautology.push_back(~lit); } } clause_use_list & neg_occs = s.m_use_list.get(~l); for (auto it = neg_occs.mk_iterator(); !it.at_end(); it.next()) { clause & c = it.curr(); - if (c.is_learned()) continue; + if (c.is_learned() || c.was_removed()) continue; bool tautology = false; for (literal lit : c) { if (s.is_marked(~lit) && lit != ~l) { tautology = true; + m_tautology.push_back(~lit); break; } } @@ -1251,26 +1237,36 @@ namespace sat { return !m_clause.is_binary() && (m_clause.get_clause() == &c); } + /** + \brief idx is the index of the blocked literal. + m_tautology contains literals that were used to establish that the current members of m_covered_clause is blocked. + This routine removes literals that were not relevant to establishing it was blocked. + */ void minimize_covered_clause(unsigned idx) { - IF_VERBOSE(0, verbose_stream() << "minimize: " << m_covered_clause << " @ " << idx << "\n";); + // IF_VERBOSE(0, verbose_stream() << "minimize: " << m_covered_clause << " @ " << idx << "\n" << "tautology: " << m_tautology << "\n";); + for (literal l : m_tautology) VERIFY(s.is_marked(l)); for (literal l : m_covered_clause) s.unmark_visited(l); + for (literal l : m_tautology) s.mark_visited(l); s.mark_visited(m_covered_clause[idx]); + for (unsigned i = 0; i < m_covered_clause.size(); ++i) { + if (s.is_marked(m_covered_clause[i])) idx = i; + } for (unsigned i = idx; i > 0; --i) { literal lit = m_covered_clause[i]; if (!s.is_marked(lit)) continue; clause_ante const& ante = m_covered_antecedent[i]; if (ante.cls()) { + //IF_VERBOSE(0, verbose_stream() << "clause ante: " << lit << ": " << *ante.cls() << "\n";); for (literal l : *ante.cls()) { - IF_VERBOSE(0, verbose_stream() << "clause ante: " << l << "\n";); if (l != ~lit) s.mark_visited(l); } } if (ante.lit1() != null_literal) { - IF_VERBOSE(0, verbose_stream() << "ante1: " << ante.lit1() << "\n";); + //IF_VERBOSE(0, verbose_stream() << "ante1: " << lit << ": " << ante.lit1() << "\n";); s.mark_visited(ante.lit1()); } if (ante.lit2() != null_literal) { - IF_VERBOSE(0, verbose_stream() << "ante2: " << ante.lit2() << "\n";); + //IF_VERBOSE(0, verbose_stream() << "ante2: " << lit << ": " << ante.lit2() << "\n";); s.mark_visited(ante.lit2()); } } @@ -1282,8 +1278,16 @@ namespace sat { s.unmark_visited(lit); } } + // ensure that rest of literals from original clause are included + for (unsigned i = idx + 1; i < m_covered_clause.size() && m_covered_antecedent[i] == clause_ante(); ++i) { + literal lit = m_covered_clause[i]; + m_covered_clause[j++] = lit; + } + for (literal l : m_covered_clause) VERIFY(!s.is_marked(l)); + unsigned sz0 = m_covered_clause.size(); m_covered_clause.resize(j); - IF_VERBOSE(0, verbose_stream() << "reduced: " << m_covered_clause << "\n";); + VERIFY(j >= m_clause.size()); + // IF_VERBOSE(0, verbose_stream() << "reduced from size " << sz0 << " to " << m_covered_clause << "\n" << m_clause << "\n";); } /* @@ -1303,71 +1307,51 @@ namespace sat { bool add_ala() { for (; m_ala_qhead < m_covered_clause.size(); ++m_ala_qhead) { literal l = m_covered_clause[m_ala_qhead]; + for (watched & w : s.get_wlist(~l)) { if (w.is_binary_non_learned_clause()) { literal lit = w.get_literal(); if (revisit_binary(l, lit)) continue; if (s.is_marked(lit)) { - IF_VERBOSE(0, verbose_stream() << "ATE: " << m_covered_clause << " binary: " << l << " " << lit << "\n";); + //IF_VERBOSE(0, verbose_stream() << "ATE: " << m_covered_clause << " binary: " << l << " " << lit << "\n";); return true; } if (!s.is_marked(~lit)) { - IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " binary " << l << " " << lit << " " << (~lit) << "\n";); + //IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " binary " << l << " " << lit << " " << (~lit) << "\n";); m_covered_clause.push_back(~lit); m_covered_antecedent.push_back(clause_ante(l)); s.mark_visited(~lit); } } - else if (w.is_ternary_clause() && !w.is_learned()) { - literal lit1 = w.get_literal1(); - literal lit2 = w.get_literal2(); - if (revisit_ternary(l, lit1, lit2)) continue; - if (s.is_marked(lit1) && s.is_marked(lit2)) { - IF_VERBOSE(0, verbose_stream() << "ATE: " << m_covered_clause << " ternary: " << l << " " << lit1 << " " << lit2 << "\n";); - return true; + } + clause_use_list & pos_occs = s.m_use_list.get(l); + clause_use_list::iterator it = pos_occs.mk_iterator(); + for (; !it.at_end(); it.next()) { + clause & c = it.curr(); + if (c.is_learned() || c.was_removed()) continue; + if (revisit_clause(c)) continue; + literal lit1 = null_literal; + bool ok = true; + for (literal lit : c) { + if (lit == l) continue; + if (s.is_marked(lit)) continue; + if (!s.is_marked(~lit) && lit1 == null_literal) { + lit1 = lit; } - if (s.is_marked(lit1) && !s.is_marked(~lit2)) { - IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " ternary " << l << " " << lit1 << " " << lit2 << " " << (~lit2) << "\n";); - m_covered_clause.push_back(~lit2); - m_covered_antecedent.push_back(clause_ante(l, lit1)); - s.mark_visited(~lit2); - continue; - } - if (s.is_marked(lit2) && !s.is_marked(~lit1)) { - IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " ternay " << l << " " << lit1 << " " << lit2 << " " << (~lit1) << "\n";); - m_covered_clause.push_back(~lit1); - m_covered_antecedent.push_back(clause_ante(l, lit2)); - s.mark_visited(~lit1); - continue; + else { + ok = false; + break; } } - else if (w.is_clause()) { - clause & c = s.s.get_clause(w.get_clause_offset()); - if (c.is_learned()) continue; - if (revisit_clause(c)) continue; - literal lit1 = null_literal; - bool ok = true; - for (literal lit : c) { - if (lit == l) continue; - if (s.is_marked(lit)) continue; - if (!s.is_marked(~lit) && lit1 == null_literal) { - lit1 = lit; - } - else { - ok = false; - break; - } - } - if (!ok) continue; - if (lit1 == null_literal) { - IF_VERBOSE(0, verbose_stream() << "ATE: " << m_covered_clause << " clause " << c << "\n";); - return true; - } - IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " clause " << c << " " << (~lit1) << "\n";); - m_covered_clause.push_back(~lit1); - m_covered_antecedent.push_back(clause_ante(c)); - s.mark_visited(~lit1); + if (!ok) continue; + if (lit1 == null_literal) { + //IF_VERBOSE(0, verbose_stream() << "ATE: " << m_covered_clause << " clause " << c << "\n";); + return true; } + // IF_VERBOSE(0, verbose_stream() << "ALA: " << m_covered_clause << " clause " << c << " " << (~lit1) << "\n";); + m_covered_clause.push_back(~lit1); + m_covered_antecedent.push_back(clause_ante(c)); + s.mark_visited(~lit1); } } return false; @@ -1430,10 +1414,9 @@ namespace sat { for (literal l : m_covered_clause) s.unmark_visited(l); return at_t; } - for (unsigned i = 0; !is_tautology && i < sz0; ++i) { + for (unsigned i = 0; i < sz0; ++i) { if (check_abce_tautology(m_covered_clause[i])) { blocked = m_covered_clause[i]; - minimize_covered_clause(i); is_tautology = true; break; } @@ -1456,7 +1439,6 @@ namespace sat { is_tautology = add_cla(blocked); } while (m_covered_clause.size() > sz && !is_tautology); - if (above_threshold(sz0)) break; if (et == acce_t && !is_tautology) { sz = m_covered_clause.size(); if (add_ala()) { @@ -1465,9 +1447,9 @@ namespace sat { } k = model_converter::ACCE; } + if (above_threshold(sz0)) break; } while (m_covered_clause.size() > sz && !is_tautology); - // if (is_tautology) std::cout << num_iterations << " " << m_covered_clause.size() << " " << sz0 << " " << is_tautology << " " << m_elim_stack.size() << "\n"; for (literal l : m_covered_clause) s.unmark_visited(l); return (is_tautology && !above_threshold(sz0)) ? bc_t : no_t; } @@ -1484,6 +1466,7 @@ namespace sat { m_covered_clause.push_back(l); m_covered_antecedent.push_back(clause_ante()); } + // shuffle(s.s.m_rand, m_covered_clause); return cla(blocked, k); } @@ -1516,81 +1499,68 @@ namespace sat { template void process_cce_binary(literal l) { - m_blocked_binary.reset(); literal blocked = null_literal; watch_list & wlist = s.get_wlist(~l); m_counter -= wlist.size(); - watch_list::iterator it = wlist.begin(); - watch_list::iterator it2 = it; - watch_list::iterator end = wlist.end(); model_converter::kind k; - for (; it != end; ++it) { - if (!it->is_binary_non_learned_clause()) { - *it2 = *it; - it2++; - continue; - } - literal l2 = it->get_literal(); + for (watched & w : wlist) { + if (!w.is_binary_non_learned_clause()) continue; + literal l2 = w.get_literal(); switch (cce(l, l2, blocked, k)) { case bc_t: - block_covered_binary(it, l, blocked, k); - s.m_num_covered_clauses++; - m_blocked_binary.push_back(l2); + inc_bc(); + block_covered_binary(w, l, blocked, k); + w.set_learned(true); + s.s.set_learned1(l2, l, true); break; case at_t: s.m_num_ate++; - m_blocked_binary.push_back(l2); + w.set_learned(true); + s.s.set_learned1(l2, l, true); break; case no_t: - *it2 = *it; - it2++; break; } } - wlist.set_end(it2); - if (s.m_retain_blocked_clauses && !m_blocked_binary.empty()) { - IF_VERBOSE(0, verbose_stream() << "retaining " << m_blocked_binary.size() << " binary clauses\n";); - for (literal lit2 : m_blocked_binary) { - s.s.mk_bin_clause(l, lit2, true); - } - } } - template void cce_clauses() { - m_to_remove.reset(); literal blocked; model_converter::kind k; for (clause* cp : s.s.m_clauses) { clause& c = *cp; - if (!c.was_removed() && !c.is_learned()) { - switch (cce(c, blocked, k)) { - case bc_t: - block_covered_clause(c, blocked, k); - s.m_num_covered_clauses++; - break; - case at_t: - m_to_remove.push_back(&c); - break; - case no_t: - break; - } + if (c.was_removed() || c.is_learned()) continue; + switch (cce(c, blocked, k)) { + case bc_t: + inc_bc(); + block_covered_clause(c, blocked, k); + s.set_learned(c); + break; + case at_t: + s.m_num_ate++; + s.set_learned(c); + break; + case no_t: + break; } } - for (clause* c : m_to_remove) { - s.block_clause(*c); - } - m_to_remove.reset(); } + template + void inc_bc() { + switch (et) { + case cce_t: s.m_num_cce++; break; + case acce_t: s.m_num_acce++; break; + case abce_t: s.m_num_abce++; break; + } + } void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry, model_converter::kind k) { TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";); VERIFY(!s.is_external(l)); if (new_entry == 0) new_entry = &(mc.mk(k, l.var())); - m_to_remove.push_back(&c); for (literal lit : c) { if (lit != l && process_var(lit.var())) { m_queue.decreased(~lit); @@ -1611,25 +1581,25 @@ namespace sat { mc.insert(*new_entry, m_covered_clause, m_elim_stack); } - void prepare_block_binary(watch_list::iterator it, literal l1, literal blocked, model_converter::entry*& new_entry, model_converter::kind k) { + void prepare_block_binary(watched const& w, literal l1, literal blocked, model_converter::entry*& new_entry, model_converter::kind k) { SASSERT(!s.is_external(blocked)); if (new_entry == 0) new_entry = &(mc.mk(k, blocked.var())); - literal l2 = it->get_literal(); + literal l2 = w.get_literal(); TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l1 << "\n";); - s.remove_bin_clause_half(l2, l1, it->is_learned()); + s.set_learned(l1, l2); m_queue.decreased(~l2); } - void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) { - literal l2 = it->get_literal(); - prepare_block_binary(it, l, l, new_entry, model_converter::BLOCK_LIT); + void block_binary(watched const& w, literal l, model_converter::entry *& new_entry) { + literal l2 = w.get_literal(); + prepare_block_binary(w, l, l, new_entry, model_converter::BLOCK_LIT); mc.insert(*new_entry, l, l2); } - void block_covered_binary(watch_list::iterator it, literal l, literal blocked, model_converter::kind k) { + void block_covered_binary(watched const& w, literal l, literal blocked, model_converter::kind k) { model_converter::entry * new_entry = 0; - prepare_block_binary(it, l, blocked, new_entry, k); + prepare_block_binary(w, l, blocked, new_entry, k); mc.insert(*new_entry, m_covered_clause, m_elim_stack); } @@ -1681,6 +1651,7 @@ namespace sat { for (; !it.at_end(); it.next()) { clause & c = it.curr(); if (c.is_learned()) continue; + if (c.was_removed()) continue; m_counter -= c.size(); unsigned sz = c.size(); unsigned i; @@ -1707,33 +1678,40 @@ namespace sat { struct simplifier::blocked_cls_report { simplifier & m_simplifier; stopwatch m_watch; - unsigned m_num_blocked_clauses; - unsigned m_num_covered_clauses; + unsigned m_num_bce; + unsigned m_num_cce; + unsigned m_num_acce; + unsigned m_num_abce; unsigned m_num_ate; - unsigned m_num_added_clauses; + unsigned m_num_bca; blocked_cls_report(simplifier & s): m_simplifier(s), - m_num_blocked_clauses(s.m_num_blocked_clauses), - m_num_covered_clauses(s.m_num_covered_clauses), + m_num_bce(s.m_num_bce), + m_num_cce(s.m_num_cce), + m_num_acce(s.m_num_acce), + m_num_abce(s.m_num_abce), m_num_ate(s.m_num_ate), - m_num_added_clauses(s.m_num_bca) { + m_num_bca(s.m_num_bca) { m_watch.start(); } ~blocked_cls_report() { m_watch.stop(); IF_VERBOSE(SAT_VB_LVL, - verbose_stream() << " (sat-blocked-clauses :elim-blocked-clauses " - << (m_simplifier.m_num_blocked_clauses - m_num_blocked_clauses) - << " :elim-covered-clauses " - << (m_simplifier.m_num_covered_clauses - m_num_covered_clauses) - << " :added-clauses " - << (m_simplifier.m_num_bca - m_num_added_clauses) - << " :ate " - << (m_simplifier.m_num_ate - m_num_ate) - << mem_stat() + verbose_stream() << " (sat-blocked-clauses"; + report(m_simplifier.m_num_ate, m_num_ate, " :ate "); + report(m_simplifier.m_num_bce, m_num_bce, " :bce "); + report(m_simplifier.m_num_abce, m_num_abce, " :abce "); + report(m_simplifier.m_num_cce, m_num_cce, " :cce "); + report(m_simplifier.m_num_bca, m_num_bca, " :bca "); + report(m_simplifier.m_num_acce, m_num_acce, " :acce "); + verbose_stream() << mem_stat() << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";); } + + void report(unsigned n, unsigned m, char const* s) { + if (n > m) verbose_stream() << s << (n - m); + } }; void simplifier::elim_blocked_clauses() { @@ -1743,7 +1721,7 @@ namespace sat { elim(); } - unsigned simplifier::get_num_unblocked_bin(literal l) const { + unsigned simplifier::num_nonlearned_bin(literal l) const { unsigned r = 0; watch_list const & wlist = get_wlist(~l); for (auto & w : wlist) { @@ -1758,8 +1736,8 @@ namespace sat { literal neg_l(v, true); unsigned num_pos = m_use_list.get(pos_l).size(); unsigned num_neg = m_use_list.get(neg_l).size(); - unsigned num_bin_pos = get_num_unblocked_bin(pos_l); - unsigned num_bin_neg = get_num_unblocked_bin(neg_l); + unsigned num_bin_pos = num_nonlearned_bin(pos_l); + unsigned num_bin_neg = num_nonlearned_bin(neg_l); unsigned cost = 2 * num_pos * num_neg + num_pos * num_bin_neg + num_neg * num_bin_pos; CTRACE("elim_vars_detail", cost == 0, tout << v << " num_pos: " << num_pos << " num_neg: " << num_neg << " num_bin_pos: " << num_bin_pos << " num_bin_neg: " << num_bin_neg << " cost: " << cost << "\n";); @@ -1799,9 +1777,10 @@ namespace sat { void simplifier::collect_clauses(literal l, clause_wrapper_vector & r) { clause_use_list const & cs = m_use_list.get(l); for (auto it = cs.mk_iterator(); !it.at_end(); it.next()) { - if (!it.curr().is_learned()) { - r.push_back(clause_wrapper(it.curr())); - SASSERT(r.back().size() == it.curr().size()); + clause& c = it.curr(); + if (!c.is_learned() && !c.was_removed()) { + r.push_back(clause_wrapper(c)); + SASSERT(r.back().size() == c.size()); } } @@ -1939,8 +1918,8 @@ namespace sat { literal pos_l(v, false); literal neg_l(v, true); - unsigned num_bin_pos = get_num_unblocked_bin(pos_l); - unsigned num_bin_neg = get_num_unblocked_bin(neg_l); + unsigned num_bin_pos = num_nonlearned_bin(pos_l); + unsigned num_bin_neg = num_nonlearned_bin(neg_l); clause_use_list & pos_occs = m_use_list.get(pos_l); clause_use_list & neg_occs = m_use_list.get(neg_l); unsigned num_pos = pos_occs.num_irredundant() + num_bin_pos; @@ -2146,15 +2125,19 @@ namespace sat { st.update("subsumed", m_num_subsumed); st.update("subsumption resolution", m_num_sub_res); st.update("elim literals", m_num_elim_lits); - st.update("elim blocked clauses", m_num_blocked_clauses); - st.update("elim covered clauses", m_num_covered_clauses); - st.update("blocked clauses added", m_num_bca); - st.update("asymmetric tautologies eliminated", m_num_ate); + st.update("bce", m_num_bce); + st.update("cce", m_num_cce); + st.update("acce", m_num_acce); + st.update("abce", m_num_abce); + st.update("bca", m_num_bca); + st.update("ate", m_num_ate); } void simplifier::reset_statistics() { - m_num_blocked_clauses = 0; - m_num_covered_clauses = 0; + m_num_bce = 0; + m_num_cce = 0; + m_num_acce = 0; + m_num_abce = 0; m_num_subsumed = 0; m_num_sub_res = 0; m_num_elim_lits = 0; diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index 69a444954..e0a0e6b67 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -100,14 +100,16 @@ namespace sat { unsigned m_elim_vars_bdd_delay; // stats - unsigned m_num_blocked_clauses; - unsigned m_num_covered_clauses; + unsigned m_num_bce; + unsigned m_num_cce; + unsigned m_num_acce; + unsigned m_num_abce; + unsigned m_num_bca; + unsigned m_num_ate; unsigned m_num_subsumed; unsigned m_num_elim_vars; unsigned m_num_sub_res; unsigned m_num_elim_lits; - unsigned m_num_bca; - unsigned m_num_ate; bool m_learned_in_use_lists; unsigned m_old_num_elim_vars; @@ -132,9 +134,8 @@ namespace sat { void remove_clause_core(clause & c); void remove_clause(clause & c); void remove_clause(clause & c, literal l); - void block_clause(clause & c); - void unblock_clause(clause & c); - void remove_bin_clause_half(literal l1, literal l2, bool learned); + void set_learned(clause & c); + void set_learned(literal l1, literal l2); bool_var get_min_occ_var(clause const & c) const; bool subsumes1(clause const & c1, clause const & c2, literal & l); @@ -183,7 +184,7 @@ namespace sat { bool elim_vars_bdd_enabled() const; bool elim_vars_enabled() const; - unsigned get_num_unblocked_bin(literal l) const; + unsigned num_nonlearned_bin(literal l) const; unsigned get_to_elim_cost(bool_var v) const; void order_vars_for_elim(bool_var_vector & r); void collect_clauses(literal l, clause_wrapper_vector & r); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index d21e773f3..b8850ce95 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -396,9 +396,9 @@ namespace sat { bool solver::attach_ter_clause(clause & c) { bool reinit = false; - m_watches[(~c[0]).index()].push_back(watched(c[1], c[2], c.is_learned())); - m_watches[(~c[1]).index()].push_back(watched(c[0], c[2], c.is_learned())); - m_watches[(~c[2]).index()].push_back(watched(c[0], c[1], c.is_learned())); + m_watches[(~c[0]).index()].push_back(watched(c[1], c[2])); + m_watches[(~c[1]).index()].push_back(watched(c[0], c[2])); + m_watches[(~c[2]).index()].push_back(watched(c[0], c[1])); if (!at_base_lvl()) { if (value(c[1]) == l_false && value(c[2]) == l_false) { m_stats.m_ter_propagate++; @@ -482,17 +482,23 @@ namespace sat { } void solver::set_learned(clause& c, bool learned) { - if (c.is_learned() == learned) - return; - - if (c.size() == 3) { - set_ternary_learned(get_wlist(~c[0]), c[1], c[2], learned); - set_ternary_learned(get_wlist(~c[1]), c[0], c[2], learned); - set_ternary_learned(get_wlist(~c[2]), c[0], c[1], learned); - } - c.set_learned(learned); + if (c.is_learned() != learned) + c.set_learned(learned); } + void solver::set_learned1(literal l1, literal l2, bool learned) { + for (watched& w : get_wlist(~l1)) { + if (w.is_binary_clause() && l2 == w.get_literal() && !w.is_learned()) { + w.set_learned(learned); + break; + } + } + } + + void solver::set_learned(literal l1, literal l2, bool learned) { + set_learned1(l1, l2, learned); + set_learned1(l2, l1, learned); + } /** \brief Select a watch literal starting the search at the given position. @@ -1523,7 +1529,7 @@ namespace sat { m_simplifier(false); CASSERT("sat_simplify_bug", check_invariant()); CASSERT("sat_missed_prop", check_missed_propagation()); - si.check_watches(); + si.check_watches(); if (!m_learned.empty()) { m_simplifier(true); CASSERT("sat_missed_prop", check_missed_propagation()); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 0370d634d..824d728d6 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -234,6 +234,8 @@ namespace sat { void attach_clause(clause & c, bool & reinit); void attach_clause(clause & c) { bool reinit; attach_clause(c, reinit); } void set_learned(clause& c, bool learned); + void set_learned(literal l1, literal l2, bool learned); + void set_learned1(literal l1, literal l2, bool learned); class scoped_disable_checkpoint { solver& s; public: diff --git a/src/sat/sat_watched.cpp b/src/sat/sat_watched.cpp index d7c6520bd..5e86a7a87 100644 --- a/src/sat/sat_watched.cpp +++ b/src/sat/sat_watched.cpp @@ -71,29 +71,23 @@ namespace sat { } void erase_ternary_watch(watch_list& wlist, literal l1, literal l2) { + watched w(l1, l2); watch_list::iterator it = wlist.begin(), end = wlist.end(); watch_list::iterator it2 = it; bool found = false; for (; it != end; ++it) { - if (it->is_ternary_clause() && it->get_literal1() == l1 && it->get_literal2() == l2) { + if (!found && w == *it) { found = true; - continue; } - *it2 = *it; - ++it2; + else { + *it2 = *it; + ++it2; + } } wlist.set_end(it2); VERIFY(found); } - void set_ternary_learned(watch_list& wlist, literal l1, literal l2, bool learned) { - for (watched& w : wlist) { - if (w.is_ternary_clause() && w.get_literal1() == l1 && w.get_literal2() == l2) { - w.set_learned(learned); - } - } - } - void conflict_cleanup(watch_list::iterator it, watch_list::iterator it2, watch_list& wlist) { watch_list::iterator end = wlist.end(); for (; it != end; ++it, ++it2) diff --git a/src/sat/sat_watched.h b/src/sat/sat_watched.h index 8979405ae..acd4ed9c0 100644 --- a/src/sat/sat_watched.h +++ b/src/sat/sat_watched.h @@ -53,12 +53,12 @@ namespace sat { SASSERT(learned || is_binary_non_learned_clause()); } - watched(literal l1, literal l2, bool learned) { + watched(literal l1, literal l2) { SASSERT(l1 != l2); if (l1.index() > l2.index()) std::swap(l1, l2); m_val1 = l1.to_uint(); - m_val2 = static_cast(TERNARY) + (static_cast(learned) << 2) + (l2.to_uint() << 3); + m_val2 = static_cast(TERNARY) + (l2.to_uint() << 2); SASSERT(is_ternary_clause()); SASSERT(get_literal1() == l1); SASSERT(get_literal2() == l2); @@ -87,16 +87,16 @@ namespace sat { bool is_binary_clause() const { return get_kind() == BINARY; } literal get_literal() const { SASSERT(is_binary_clause()); return to_literal(static_cast(m_val1)); } void set_literal(literal l) { SASSERT(is_binary_clause()); m_val1 = l.to_uint(); } - bool is_learned() const { SASSERT(is_binary_clause() || is_ternary_clause()); return ((m_val2 >> 2) & 1) == 1; } + bool is_learned() const { SASSERT(is_binary_clause()); return ((m_val2 >> 2) & 1) == 1; } bool is_binary_learned_clause() const { return is_binary_clause() && is_learned(); } bool is_binary_non_learned_clause() const { return is_binary_clause() && !is_learned(); } - void set_learned(bool l) { SASSERT(is_learned() != l); if (l) m_val2 |= 4; else m_val2 &= 3; SASSERT(is_learned() == l); } + void set_learned(bool l) { if (l) m_val2 |= 4u; else m_val2 &= ~4u; SASSERT(is_learned() == l); } bool is_ternary_clause() const { return get_kind() == TERNARY; } literal get_literal1() const { SASSERT(is_ternary_clause()); return to_literal(static_cast(m_val1)); } - literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 3); } + literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 2); } bool is_clause() const { return get_kind() == CLAUSE; } clause_offset get_clause_offset() const { SASSERT(is_clause()); return static_cast(m_val1); }