mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-02 07:07:52 +00:00
Code Activity

collect shared clauses inside share units after pop to base level (might help NIA)

Browse source
This commit is contained in:
Ilana Shapiro 2025-12-19 17:15:39 -08:00
parent b4c7764aad
commit e11bf4b9b1
1 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/smt_parallel.cpp
View file

@ -154,6 +154,10 @@ namespace smt {
goto check_cube_start; goto check_cube_start;
b.split(m_l2g, id, node, atom); b.split(m_l2g, id, node, atom);
simplify(); simplify();
if (m_config.m_share_units) {
IF_VERBOSE(1, verbose_stream() << " Sharing units\n");
share_units();
}
break; break;
} }
case l_true: { case l_true: {
@ -203,10 +207,6 @@ namespace smt {
break; break;
} }
} }
if (m_config.m_share_units) {
IF_VERBOSE(1, verbose_stream() << " Sharing units\n");
share_units();
}
} }
} }
@ -236,6 +236,7 @@ namespace smt {
// Collect new units learned locally by this worker and send to batch manager // Collect new units learned locally by this worker and send to batch manager
ctx->pop_to_base_lvl(); ctx->pop_to_base_lvl();
collect_shared_clauses(); // collect shared clauses from other workers while we're ALREADY POPPED TO BASE LEVEL
unsigned sz = ctx->assigned_literals().size(); 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) { // iterate only over new literals since last sync
literal lit = ctx->assigned_literals()[j]; literal lit = ctx->assigned_literals()[j];