From b98c864d760c141a0e622f9af18f6db204d04974 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 1 Dec 2017 18:06:26 -0800 Subject: [PATCH] fixes to inprocessing code Signed-off-by: Nikolaj Bjorner --- src/sat/sat_asymm_branch.cpp | 21 ++++++++++----------- src/sat/sat_asymm_branch.h | 3 ++- src/sat/sat_elim_eqs.cpp | 7 ++++--- src/sat/sat_lookahead.cpp | 3 +++ src/sat/sat_scc.cpp | 12 ++++++------ src/sat/sat_solver.cpp | 21 +++------------------ src/sat/sat_solver.h | 1 - 7 files changed, 28 insertions(+), 40 deletions(-) diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 869b4ac4c..8e5e556e3 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -59,7 +59,7 @@ namespace sat { } }; - void asymm_branch::process(scc& scc, clause_vector& clauses) { + void asymm_branch::process(scc* scc, clause_vector& clauses) { int64 limit = -m_asymm_branch_limit; std::stable_sort(clauses.begin(), clauses.end(), clause_size_lt()); m_counter -= clauses.size(); @@ -83,7 +83,7 @@ namespace sat { } s.checkpoint(); clause & c = *(*it); - if (m_asymm_branch_sampled ? !process_sampled(scc, c) : !process(c)) { + if (scc ? !process_sampled(*scc, c) : !process(c)) { continue; // clause was removed } *it2 = *it; @@ -106,7 +106,7 @@ namespace sat { ++m_calls; if (m_calls <= m_asymm_branch_delay) return; - if (!m_asymm_branch && !m_asymm_branch_all) + if (!m_asymm_branch && !m_asymm_branch_all && !m_asymm_branch_sampled) return; s.propagate(false); // must propagate, since it uses s.push() if (s.m_inconsistent) @@ -119,13 +119,18 @@ namespace sat { TRACE("asymm_branch_detail", s.display(tout);); report rpt(*this); svector saved_phase(s.m_phase); + if (m_asymm_branch) { + m_counter = 0; + process(nullptr, s.m_clauses); + m_counter = -m_counter; + } if (m_asymm_branch_sampled) { scc scc(s, m_params); while (true) { unsigned elim = m_elim_literals; scc.init_big(true); - process(scc, s.m_clauses); - process(scc, s.m_learned); + process(&scc, s.m_clauses); + process(&scc, s.m_learned); s.propagate(false); if (s.m_inconsistent) break; @@ -134,12 +139,6 @@ namespace sat { break; } } - else { - scc scc(s, m_params); - m_counter = 0; - process(scc, s.m_clauses); - m_counter = -m_counter; - } s.m_phase = saved_phase; m_asymm_branch_limit *= 2; if (m_asymm_branch_limit > UINT_MAX) diff --git a/src/sat/sat_asymm_branch.h b/src/sat/sat_asymm_branch.h index b7e2b0218..4510aaddf 100644 --- a/src/sat/sat_asymm_branch.h +++ b/src/sat/sat_asymm_branch.h @@ -41,6 +41,7 @@ namespace sat { bool m_asymm_branch; unsigned m_asymm_branch_delay; bool m_asymm_branch_sampled; + bool m_asymm_branch_propagate; bool m_asymm_branch_all; int64 m_asymm_branch_limit; @@ -64,7 +65,7 @@ namespace sat { bool process_sampled(scc& scc, clause & c); - void process(scc& scc, clause_vector & c); + void process(scc* scc, clause_vector & c); bool process_all(clause & c); diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp index ea44c870d..d0166b64e 100644 --- a/src/sat/sat_elim_eqs.cpp +++ b/src/sat/sat_elim_eqs.cpp @@ -94,10 +94,11 @@ namespace sat { if (!c.frozen()) m_solver.detach_clause(c); // apply substitution - for (i = 0; i < sz; i++) { - c[i] = norm(roots, c[i]); + for (i = 0; i < sz; 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())); + 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_lookahead.cpp b/src/sat/sat_lookahead.cpp index 2a2da1c90..843c70fd8 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2081,6 +2081,7 @@ namespace sat { if (inconsistent()) { TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";); m_cube_state.m_freevars_threshold = prev_nfreevars; + m_cube_state.inc_conflict(); if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false; continue; } @@ -2375,6 +2376,8 @@ namespace sat { ++disconnected1; uf.merge(u.index(), v.index()); uf.merge((~u).index(), (~v).index()); + VERIFY(!m_s.was_eliminated(u.var())); + VERIFY(!m_s.was_eliminated(v.var())); m_s.mk_clause(~u, v, true); } else { diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp index 7615a19a3..59c53304d 100644 --- a/src/sat/sat_scc.cpp +++ b/src/sat/sat_scc.cpp @@ -303,16 +303,16 @@ namespace sat { else { SASSERT(m_left[u.index()] == 0); m_left[u.index()] = ++dfs_num; - for (literal v : m_dag[u.index()]) { - if (m_left[v.index()] == 0) { - todo.push_back(pframe(u, v)); - } - } literal p = todo.back().parent(); if (p != null_literal) { m_root[u.index()] = m_root[p.index()]; m_parent[u.index()] = p; } + for (literal v : m_dag[u.index()]) { + if (m_left[v.index()] == 0) { + todo.push_back(pframe(u, v)); + } + } } } for (unsigned i = 0; i < num_lits; ++i) { @@ -339,7 +339,7 @@ namespace sat { watch_list::iterator end = wlist.end(); for (; it != end; ++it) { watched& w = *it; - if (learned ? w.is_binary_learned_clause() : w.is_binary_unblocked_clause()) { + if (learned ? w.is_binary_learned_clause() : w.is_binary_clause()) { literal v = w.get_literal(); if (reaches(u, v) && u != get_parent(v)) { ++m_num_elim_bin; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 5a7e234e9..f8425b9bc 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -159,17 +159,20 @@ namespace sat { } } // copy high quality lemmas + unsigned num_learned = 0; for (clause* c : src.m_learned) { if (c->glue() <= 2 || (c->size() <= 40 && c->glue() <= 8)) { buffer.reset(); for (literal l : *c) buffer.push_back(l); clause* c1 = mk_clause_core(buffer.size(), buffer.c_ptr(), true); if (c1) { + ++num_learned; c1->set_glue(c->glue()); c1->set_psm(c->psm()); } } } + IF_VERBOSE(1, verbose_stream() << "(sat.copy :learned " << num_learned << ")\n";); } m_user_scope_literals.reset(); @@ -879,9 +882,6 @@ namespace sat { m_stats.m_units = init_trail_size(); IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";); SASSERT(at_base_lvl()); - if (m_config.m_lookahead_search && num_lits == 0) { - return lookahead_search(); - } if (m_config.m_local_search) { return do_local_search(num_lits, lits); @@ -984,21 +984,6 @@ namespace sat { return r; } - lbool solver::lookahead_search() { - lookahead lh(*this); - lbool r = l_undef; - try { - r = lh.check(); - m_model = lh.get_model(); - } - catch (z3_exception&) { - lh.collect_statistics(m_aux_stats); - throw; - } - lh.collect_statistics(m_aux_stats); - return r; - } - lbool solver::check_par(unsigned num_lits, literal const* lits) { scoped_ptr_vector ls; int num_threads = static_cast(m_config.m_num_threads + m_config.m_local_search_threads); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 602850487..135d9e067 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -394,7 +394,6 @@ namespace sat { void sort_watch_lits(); void exchange_par(); lbool check_par(unsigned num_lits, literal const* lits); - lbool lookahead_search(); lbool do_local_search(unsigned num_lits, literal const* lits); // -----------------------