mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
refine parsat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
dadcc6e8ff
commit
76bc4f0b38
|
@ -72,9 +72,9 @@ namespace sat {
|
|||
}
|
||||
|
||||
void solver::copy(solver const & src) {
|
||||
pop_to_base_level();
|
||||
SASSERT(m_mc.empty() && src.m_mc.empty());
|
||||
SASSERT(scope_lvl() == 0);
|
||||
SASSERT(src.scope_lvl() == 0);
|
||||
// create new vars
|
||||
if (num_vars() < src.num_vars()) {
|
||||
for (bool_var v = num_vars(); v < src.num_vars(); v++) {
|
||||
|
@ -120,6 +120,9 @@ namespace sat {
|
|||
mk_clause_core(buffer);
|
||||
}
|
||||
}
|
||||
|
||||
m_user_scope_literals.reset();
|
||||
m_user_scope_literals.append(src.m_user_scope_literals);
|
||||
}
|
||||
|
||||
// -----------------------
|
||||
|
@ -800,6 +803,9 @@ namespace sat {
|
|||
sat::par par;
|
||||
for (int i = 0; i < num_threads; ++i) {
|
||||
m_params.set_uint("random_seed", i);
|
||||
if (i < 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);
|
||||
|
@ -869,17 +875,18 @@ namespace sat {
|
|||
*/
|
||||
void solver::exchange_par() {
|
||||
if (m_par && scope_lvl() == 0) {
|
||||
unsigned sz = scope_lvl() == 0 ? m_trail.size() : m_scopes[0].m_trail_lim;
|
||||
unsigned num_in = 0, num_out = 0;
|
||||
SASSERT(scope_lvl() == 0); // parallel with assumptions is TBD
|
||||
literal_vector in, out;
|
||||
for (unsigned i = m_par_limit_out; i < m_trail.size(); ++i) {
|
||||
for (unsigned i = m_par_limit_out; i < sz; ++i) {
|
||||
literal lit = m_trail[i];
|
||||
if (lit.var() < m_par_num_vars) {
|
||||
++num_out;
|
||||
out.push_back(lit);
|
||||
}
|
||||
}
|
||||
m_par_limit_out = m_trail.size();
|
||||
m_par_limit_out = sz;
|
||||
m_par->exchange(out, m_par_limit_in, in);
|
||||
for (unsigned i = 0; !inconsistent() && i < in.size(); ++i) {
|
||||
literal lit = in[i];
|
||||
|
|
Loading…
Reference in a new issue