mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-16 15:15:35 +00:00
Code Activity

Simplify parallel SMT code: clean comments and deduplicate stat computation (#9507)

Browse source 
* Initial plan

* Simplify parallel SMT code: clean comments and deduplicate stat computation

- Normalize tab to spaces on line 7 of smt_parallel_params.pyg
- Remove extraneous blank line after ++m_num_core_minimize_calls
- Replace informal retry-loop comments with professional descriptions
- Extract repeated safe-division pattern into safe_ratio lambda in backbones_worker::collect_statistics

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/e0418d2f-7d4d-4980-897f-98d4057bddc3

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-05-12 14:41:20 -04:00 • committed by GitHub
parent 57e0a12e3a
commit 98153a8f30
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 16 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/params/smt_parallel_params.pyg
View file

@ -4,7 +4,7 @@ def_module_params('smt_parallel',
params=(
('inprocessing', BOOL, False, 'integrate in-processing as a heuristic simplification'),
('sls', BOOL, False, 'add sls-tactic as a separate worker thread outside the search tree parallelism'),
('num_global_bb_fl_threads', UINT, 0, 'run failed-literal backbone worker threads; default is 0 (off), supported values are 1 (negative mode only) or 2 (negative and positive mode)'),
('num_global_bb_fl_threads', UINT, 0, 'run failed-literal backbone worker threads; default is 0 (off), supported values are 1 (negative mode only) or 2 (negative and positive mode)'),
('num_global_bb_batch_threads', UINT, 0, 'run Janota-style chunking backbone worker threads; default is 0 (off), supported values are 1 (negative mode only) or 2 (negative and positive mode)'),
('local_backbones', BOOL, False, 'enable local backbones experiment within the search tree parallelism'),
('core_minimize', BOOL, True, 'minimize unsat cores used for parallel cube backtracking'),

38
src/smt/smt_parallel.cpp
View file

@ -481,10 +481,9 @@ namespace smt {
}
}
// retry loop so thread isn't idle
// experiments on my laptop showed this had about a 0% success rate and i'm not sure if this
// messes with resource scheduling little enough to justify keeping it
// for now we only retry if we make progress on finding at least 1 backbone in each retry round
// Retry loop: keeps the thread active while waiting for new backbone candidates.
// Only retries if at least one new backbone was found in the previous round, to avoid
// spinning indefinitely when progress has stalled.
while (!b.has_new_backbone_candidates(bb_candidate_epoch) && !canceled() && m.inc()) {
collect_shared_clauses();
unsigned found_before = m_stats.m_internal_backbones_found;
@ -506,8 +505,7 @@ namespace smt {
fallback_failed_literal_probe(bb_candidate_lits, bb_candidate_lits, true);
// break if we made no progress on this batch
// unlikely to make progress on future runs and idk if this creates any kind of resource stress
// Break if no progress was made; further retries on this batch are unlikely to succeed.
if (m_stats.m_internal_backbones_found == found_before)
break;
}
@ -596,23 +594,18 @@ namespace smt {
st.update("bb-literals-removed-by-core", m_stats.m_lits_removed_by_core);
st.update("bb-num-chunk-increases", m_stats.m_num_chunk_increases);
double backbone_yield = 0.0;
if (m_stats.m_candidates_total > 0)
backbone_yield = 100.0 * (double)m_stats.m_internal_backbones_found / (double)m_stats.m_candidates_total;
double avg_backbones_per_batch = 0.0;
if (m_stats.m_batches_total > 0)
avg_backbones_per_batch = (double)m_stats.m_internal_backbones_found / (double)m_stats.m_batches_total;
double core_refinement_cost = 0.0;
if (m_stats.m_batches_total > 0)
core_refinement_cost = (double)m_stats.m_core_refinement_rounds / (double)m_stats.m_batches_total;
double core_effectiveness = 0.0;
if (m_stats.m_core_refinement_rounds > 0)
core_effectiveness = (double)m_stats.m_lits_removed_by_core / (double)m_stats.m_core_refinement_rounds;
auto safe_ratio = [](double num, double den) -> double {
return den > 0 ? num / den : 0.0;
};
st.update("bb-backbone-yield-pct", backbone_yield);
st.update("bb-avg-backbones-per-batch", avg_backbones_per_batch);
st.update("bb-core-refinement-rounds-per-batch", core_refinement_cost);
st.update("bb-core-effectiveness-lit-removed-per-round", core_effectiveness);
st.update("bb-backbone-yield-pct",
100.0 * safe_ratio(m_stats.m_internal_backbones_found, m_stats.m_candidates_total));
st.update("bb-avg-backbones-per-batch",
safe_ratio(m_stats.m_internal_backbones_found, m_stats.m_batches_total));
st.update("bb-core-refinement-rounds-per-batch",
safe_ratio(m_stats.m_core_refinement_rounds, m_stats.m_batches_total));
st.update("bb-core-effectiveness-lit-removed-per-round",
safe_ratio(m_stats.m_lits_removed_by_core, m_stats.m_core_refinement_rounds));
}
void parallel::sls_worker::cancel() {
@ -656,7 +649,6 @@ namespace smt {
unsigned original_size = core.size();
++m_num_core_minimize_calls;
// Invariant: F and mus and unknown is UNSAT.
while (!unknown.empty()) {
if (!m.inc()) {