mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-30 15:59:52 +00:00
Code Activity

dont pop to base level when sharing units, manual filter

Browse source
This commit is contained in:
Ilana Shapiro 2025-12-21 14:39:19 -08:00
parent c36cb2f516
commit 5bc60ce055
1 changed files with 16 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/smt/smt_parallel.cpp
View file

@ -233,28 +233,37 @@ namespace smt {
}
void parallel::worker::share_units() {
// Collect new units learned locally by this worker and send to batch manager
ctx->pop_to_base_lvl();
// Collect new base-level units learned locally by this worker and send to batch manager
unsigned sz = ctx->assigned_literals().size();
for (unsigned j = m_num_shared_units; j < sz; ++j) { // iterate only over new literals since last sync
for (unsigned j = m_num_shared_units; j < sz; ++j) {
literal lit = ctx->assigned_literals()[j];
// NEW: only share base-level assignments
if (ctx->get_assign_level(lit) > ctx->m_base_lvl)
continue;
if (!ctx->is_relevant(lit.var()) && m_config.m_share_units_relevant_only)
continue;
if (m_config.m_share_units_initial_only && lit.var() >= m_num_initial_atoms) {
LOG_WORKER(4, " Skipping non-initial unit: " << lit.var() << "\n");
continue; // skip non-iniial atoms if configured to do so
continue;
}
expr_ref e(ctx->bool_var2expr(lit.var()), ctx->m); // turn literal into a Boolean expression
expr_ref e(ctx->bool_var2expr(lit.var()), ctx->m);
if (!e)
continue;
if (m.is_and(e) || m.is_or(e))
continue;
if (lit.sign())
e = m.mk_not(e); // negate if literal is negative
e = m.mk_not(e);
b.collect_clause(m_l2g, id, e);
}
m_num_shared_units = sz;
}