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

fixes to sat-par

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-02-06 12:00:35 -08:00
parent 7aeaf11ee4
commit fe105d94a0
5 changed files with 78 additions and 51 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/opt/maxres.cpp
View file

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

4
src/sat/card_extension.cpp
View file

@ -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;
}
}

49
src/sat/sat_par.cpp
View file

@ -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<bool> _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());
}
}
}

16
src/sat/sat_par.h
View file

@ -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<reslimit> m_limits;
ptr_vector<solver> 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);

57
src/sat/sat_solver.cpp
View file

@ -835,35 +835,21 @@ namespace sat {
lbool solver::check_par(unsigned num_lits, literal const* lits) {
int num_threads = static_cast<int>(m_config.m_num_parallel);
int num_extra_solvers = num_threads - 1;
scoped_limits scoped_rlimit(rlimit());
vector<reslimit> rlims(num_extra_solvers);
ptr_vector<sat::solver> 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;
}