Simplify parallel SMT code: clean comments and deduplicate stat computation

- Fix tab/space indentation inconsistency in smt_parallel_params.pyg
- Remove double blank line in minimize_unsat_core
- Replace informal comments in backbones retry loop with clear descriptions
- Extract repeated safe-division pattern into a lambda in backbones_worker::collect_statistics

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

src/params/smt_parallel_params.pyg

@@ -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'),

src/smt/smt_parallel.cpp

@@ -481,10 +481,9 @@ namespace smt {
                 }
             }
 
-            // retry loop so thread isn't idle
+            // Retry loop to avoid idle backbone threads.
-            // experiments on my laptop showed this had about a 0% success rate and i'm not sure if this 
+            // Only continue retrying while progress is being made (at least one backbone found per round),
-            // messes with resource scheduling little enough to justify keeping it
+            // since stalling retries are unlikely to succeed.
-            // for now we only retry if we make progress on finding at least 1 backbone in each retry round
             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
+                // Stop retrying if no progress was made on this batch
-                // unlikely to make progress on future runs and idk if this creates any kind of resource stress
                 if (m_stats.m_internal_backbones_found == found_before) 
                     break;
             }
@@ -596,23 +594,13 @@ 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;
+        auto safe_ratio = [](unsigned num, unsigned denom) -> double {
-        if (m_stats.m_candidates_total > 0)
+            return denom > 0 ? (double)num / denom : 0.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;
+        st.update("bb-backbone-yield-pct",                       100.0 * safe_ratio(m_stats.m_internal_backbones_found, m_stats.m_candidates_total));
-        if (m_stats.m_batches_total > 0)
+        st.update("bb-avg-backbones-per-batch",                  safe_ratio(m_stats.m_internal_backbones_found, m_stats.m_batches_total));
-            avg_backbones_per_batch = (double)m_stats.m_internal_backbones_found / (double)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));
-        double core_refinement_cost = 0.0;
+        st.update("bb-core-effectiveness-lit-removed-per-round", safe_ratio(m_stats.m_lits_removed_by_core, m_stats.m_core_refinement_rounds));
-        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;
-
-        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);
     }
 
     void parallel::sls_worker::cancel() {
@@ -656,7 +644,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()) {