diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 6c8d5af3a..7e9381e1d 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -352,9 +352,6 @@ public: while (is_sat == l_false) { core.reset(); s().get_unsat_core(core); - expr_ref_vector core1(m); - core1.append(core.size(), core.c_ptr()); - std::cout << core1 << "\n"; // verify_core(core); model_ref mdl; get_mus_model(mdl); diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp index c051ded15..351c487bd 100644 --- a/src/sat/card_extension.cpp +++ b/src/sat/card_extension.cpp @@ -378,7 +378,7 @@ namespace sat { if (offset > m_bound) { m_coeffs[v] = (get_coeff(v) < 0) ? -m_bound : m_bound; offset = m_bound; - // TBD: also adjust coefficient in m_A. + DEBUG_CODE(active2pb(m_A);); } SASSERT(value(consequent) == l_true); @@ -424,7 +424,7 @@ namespace sat { m_lemma.push_back(~lit); if (lvl(lit) == m_conflict_lvl) { TRACE("sat", tout << "Bail out on no progress " << lit << "\n";); - IF_VERBOSE(1, verbose_stream() << "bail cardinality lemma\n";); + IF_VERBOSE(3, verbose_stream() << "(sat.card bail resolve)\n";); return false; } } diff --git a/src/sat/sat_par.cpp b/src/sat/sat_par.cpp index 585bd8bcc..8b8c8e309 100644 --- a/src/sat/sat_par.cpp +++ b/src/sat/sat_par.cpp @@ -50,10 +50,12 @@ namespace sat { if (m_tail >= m_size) { // move tail to the front. for (unsigned i = 0; i < m_heads.size(); ++i) { + // the tail could potentially loop around full circle before one of the heads picks up anything. + // in this case the we miss the newly inserted record. while (m_heads[i] < capacity) { next(m_heads[i]); } - IF_VERBOSE(3, verbose_stream() << owner << ": head: " << m_heads[i] << "\n";); + IF_VERBOSE(3, verbose_stream() << owner << ": head: " << m_heads[i] << "\n";); } m_tail = 0; } @@ -75,8 +77,8 @@ namespace sat { bool par::vector_pool::get_vector(unsigned owner, unsigned& n, unsigned const*& ptr) { unsigned head = m_heads[owner]; - SASSERT(head < m_size); while (head != m_tail) { + SASSERT(head < m_size); IF_VERBOSE(3, verbose_stream() << owner << ": head: " << head << " tail: " << m_tail << "\n";); bool is_self = owner == get_owner(head); next(m_heads[owner]); @@ -86,11 +88,40 @@ namespace sat { return true; } head = m_heads[owner]; + if (head == 0 && m_tail >= m_size) { + break; + } } return false; } - par::par() {} + par::par(solver& s): m_scoped_rlimit(s.rlimit()) {} + + par::~par() { + for (unsigned i = 0; i < m_solvers.size(); ++i) { + dealloc(m_solvers[i]); + } + } + + void par::init_solvers(solver& s, unsigned num_extra_solvers) { + unsigned num_threads = num_extra_solvers + 1; + m_solvers.resize(num_extra_solvers, 0); + symbol saved_phase = s.m_params.get_sym("phase", symbol("caching")); + for (unsigned i = 0; i < num_extra_solvers; ++i) { + m_limits.push_back(reslimit()); + s.m_params.set_uint("random_seed", s.m_rand()); + if (i == 1 + num_threads/2) { + s.m_params.set_sym("phase", symbol("random")); + } + m_solvers[i] = alloc(sat::solver, s.m_params, m_limits[i], 0); + m_solvers[i]->copy(s); + m_solvers[i]->set_par(this, i); + m_scoped_rlimit.push_child(&m_solvers[i]->rlimit()); + } + s.set_par(this, num_extra_solvers); + s.m_params.set_sym("phase", saved_phase); + } + void par::exchange(solver& s, literal_vector const& in, unsigned& limit, literal_vector& out) { if (s.m_par_syncing_clauses) return; @@ -125,18 +156,16 @@ namespace sat { } void par::share_clause(solver& s, clause const& c) { - if (s.m_par_syncing_clauses) return; + if (!enable_add(c) || s.m_par_syncing_clauses) return; flet _disable_sync_clause(s.m_par_syncing_clauses, true); unsigned n = c.size(); unsigned owner = s.m_par_id; #pragma omp critical (par_solver) { - if (enable_add(c)) { - IF_VERBOSE(3, verbose_stream() << owner << ": share " << c << "\n";); - m_pool.begin_add_vector(owner, n); - for (unsigned i = 0; i < n; ++i) { - m_pool.add_vector_elem(c[i].index()); - } + IF_VERBOSE(3, verbose_stream() << owner << ": share " << c << "\n";); + m_pool.begin_add_vector(owner, n); + for (unsigned i = 0; i < n; ++i) { + m_pool.add_vector_elem(c[i].index()); } } } diff --git a/src/sat/sat_par.h b/src/sat/sat_par.h index f76b47536..dd2e93f95 100644 --- a/src/sat/sat_par.h +++ b/src/sat/sat_par.h @@ -22,6 +22,7 @@ Revision History: #include"sat_types.h" #include"hashtable.h" #include"map.h" +#include"rlimit.h" namespace sat { @@ -53,13 +54,26 @@ namespace sat { index_set m_unit_set; literal_vector m_lits; vector_pool m_pool; + + scoped_limits m_scoped_rlimit; + vector m_limits; + ptr_vector m_solvers; + public: - par(); + par(solver& s); + + ~par(); + + void init_solvers(solver& s, unsigned num_extra_solvers); // reserve space void reserve(unsigned num_owners, unsigned sz) { m_pool.reserve(num_owners, sz); } + solver& get_solver(unsigned i) { return *m_solvers[i]; } + + void cancel_solver(unsigned i) { m_limits[i].cancel(); } + // exchange unit literals void exchange(solver& s, literal_vector const& in, unsigned& limit, literal_vector& out); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index beb53fd93..2dcbf7cbb 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -835,35 +835,21 @@ namespace sat { lbool solver::check_par(unsigned num_lits, literal const* lits) { int num_threads = static_cast(m_config.m_num_parallel); int num_extra_solvers = num_threads - 1; - scoped_limits scoped_rlimit(rlimit()); - vector rlims(num_extra_solvers); - ptr_vector solvers(num_extra_solvers); - sat::par par; - par.reserve(num_threads, 1 << 9); - symbol saved_phase = m_params.get_sym("phase", symbol("caching")); - for (int i = 0; i < num_extra_solvers; ++i) { - m_params.set_uint("random_seed", m_rand()); - if (i == 1 + num_threads/2) { - m_params.set_sym("phase", symbol("random")); - } - solvers[i] = alloc(sat::solver, m_params, rlims[i], 0); - solvers[i]->copy(*this); - solvers[i]->set_par(&par, i); - scoped_rlimit.push_child(&solvers[i]->rlimit()); - } - set_par(&par, num_extra_solvers); - m_params.set_sym("phase", saved_phase); + sat::par par(*this); + par.reserve(num_threads, 1 << 16); + par.init_solvers(*this, num_extra_solvers); int finished_id = -1; std::string ex_msg; par_exception_kind ex_kind; unsigned error_code = 0; lbool result = l_undef; + bool canceled = false; #pragma omp parallel for for (int i = 0; i < num_threads; ++i) { try { lbool r = l_undef; if (i < num_extra_solvers) { - r = solvers[i]->check(num_lits, lits); + r = par.get_solver(i).check(num_lits, lits); } else { r = check(num_lits, lits); @@ -879,40 +865,40 @@ namespace sat { } if (first) { if (r == l_true && i < num_extra_solvers) { - set_model(solvers[i]->get_model()); + set_model(par.get_solver(i).get_model()); } else if (r == l_false && i < num_extra_solvers) { m_core.reset(); - m_core.append(solvers[i]->get_core()); + m_core.append(par.get_solver(i).get_core()); } for (int j = 0; j < num_extra_solvers; ++j) { if (i != j) { - rlims[j].cancel(); + par.cancel_solver(j); } } + if (i != num_extra_solvers) { + canceled = rlimit().inc(); + rlimit().cancel(); + } } } catch (z3_error & err) { - if (i == 0) { - error_code = err.error_code(); - ex_kind = ERROR_EX; - } + error_code = err.error_code(); + ex_kind = ERROR_EX; } catch (z3_exception & ex) { - if (i == 0) { - ex_msg = ex.msg(); - ex_kind = DEFAULT_EX; - } + ex_msg = ex.msg(); + ex_kind = DEFAULT_EX; } } set_par(0, 0); if (finished_id != -1 && finished_id < num_extra_solvers) { - m_stats = solvers[finished_id]->m_stats; + m_stats = par.get_solver(finished_id).m_stats; + } + if (!canceled) { + rlimit().reset_cancel(); } - for (int i = 0; i < num_extra_solvers; ++i) { - dealloc(solvers[i]); - } if (finished_id == -1) { switch (ex_kind) { case ERROR_EX: throw z3_error(error_code); @@ -1728,10 +1714,10 @@ namespace sat { bool solver::resolve_conflict_core() { - m_stats.m_conflict++; m_conflicts++; m_conflicts_since_restart++; m_conflicts_since_gc++; + m_stats.m_conflict++; m_conflict_lvl = get_max_lvl(m_not_l, m_conflict); TRACE("sat", tout << "conflict detected at level " << m_conflict_lvl << " for "; @@ -1751,6 +1737,7 @@ namespace sat { if (m_ext && m_ext->resolve_conflict()) { learn_lemma_and_backjump(); + m_stats.m_conflict--; return true; }