mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-25 12:35:59 +00:00
Code Activity

add handling for option to not share or cube non-initial atoms

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-08-17 14:11:45 -07:00
parent 242eaa9ce8
commit 19bc9aa132
1 changed files with 11 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/smt_parallel.cpp
View file

@ -153,6 +153,11 @@ namespace smt {
literal lit = ctx->assigned_literals()[j];
if (!ctx->is_relevant(lit.var()) && m_config.m_relevant_units_only)
continue;
if (m_config.m_share_units_initial_only && lit.var() >= m_num_initial_atoms) {
LOG_WORKER(2, " Skipping non-initial unit: " << lit.var() << "\n");
continue; // skip non-iniial atoms if configured to do so
}
expr_ref e(ctx->bool_var2expr(lit.var()), ctx->m); // turn literal into a Boolean expression
if (m.is_and(e) || m.is_or(e))
@ -491,9 +496,15 @@ namespace smt {
expr_ref_vector top_lits(m);
for (const auto& node: candidates) {
if (ctx->get_assignment(node.key) != l_undef)
continue;
if (m_config.m_cube_initial_only && node.key >= m_num_initial_atoms) {
LOG_WORKER(2, " Skipping non-initial atom from cube: " << node.key << "\n");
continue; // skip non-initial atoms if configured to do so
}
expr* e = ctx->bool_var2expr(node.key);
if (!e)
continue;