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

lipstick

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-14 22:38:40 -07:00
parent 26f7ce23b6
commit e95f9757c9
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/solver/parallel_tactical2.cpp
View file

@ -1656,13 +1656,13 @@ class parallel_solver {
return den > 0 ? num / den : 0.0; return den > 0 ? num / den : 0.0;
}; };
st.update("bb-backbone-yield-pct", st.update("parallel-bb-backbone-yield-pct",
100.0 * safe_ratio(m_stats.m_internal_backbones_found, m_stats.m_candidates_total)); 100.0 * safe_ratio(m_stats.m_internal_backbones_found, m_stats.m_candidates_total));
st.update("bb-avg-backbones-per-batch", st.update("parallel-bb-avg-backbones-per-batch",
safe_ratio(m_stats.m_internal_backbones_found, m_stats.m_batches_total)); safe_ratio(m_stats.m_internal_backbones_found, m_stats.m_batches_total));
st.update("bb-core-refinement-rounds-per-batch", st.update("parallel-bb-core-refinement-rounds-per-batch",
safe_ratio(m_stats.m_core_refinement_rounds, m_stats.m_batches_total)); safe_ratio(m_stats.m_core_refinement_rounds, m_stats.m_batches_total));
st.update("bb-core-effectiveness-lit-removed-per-round", st.update("parallel-bb-core-effectiveness-lit-removed-per-round",
safe_ratio(m_stats.m_lits_removed_by_core, m_stats.m_core_refinement_rounds)); safe_ratio(m_stats.m_lits_removed_by_core, m_stats.m_core_refinement_rounds));
} }