diff --git a/CHANGELOG.md b/CHANGELOG.md index 15f59c83e..6453fc091 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -96,6 +96,9 @@ messages when running `bdd_exists(f, ...)` and `bdd_forall(f, ...)` with exclusively external memory data structures. +- Fixed statistics for quantification algorithms are incorrect/misleading. To + do so, the `adiar::statistics` struct has been changed (in a breaking way). + ## Other Changes - The maximum number of BDD variables has been decreased to *2097149* (21 bytes diff --git a/src/adiar/internal/algorithms/quantify.h b/src/adiar/internal/algorithms/quantify.h index a09f1585e..ecd0bc823 100644 --- a/src/adiar/internal/algorithms/quantify.h +++ b/src/adiar/internal/algorithms/quantify.h @@ -968,6 +968,10 @@ namespace adiar::internal const typename Policy::dd_type& in, const typename Policy::label_type label) { +#ifdef ADIAR_STATS + stats_quantify.runs += 1u; +#endif + // ------------------------------------------------------------------------- // Case: Terminal / Disjunct Levels if (dd_isterminal(in) || !has_level(in, label)) { @@ -1502,6 +1506,10 @@ namespace adiar::internal typename Policy::dd_type dd, const predicate& pred) { +#ifdef ADIAR_STATS + stats_quantify.runs += 1u; +#endif + using unreduced_t = typename Policy::__dd_type; // TODO: check for missing std::move(...) @@ -1525,13 +1533,14 @@ namespace adiar::internal case exec_policy::quantify::Singleton: { // ------------------------------------------------------------------------------------------- // Case: Repeated single variable quantification -#ifdef ADIAR_STATS - stats_quantify.singleton_sweeps += 1u; -#endif typename Policy::label_type label = pred_profile.deepest_var.level; while (label <= Policy::max_label) { dd = quantify(ep, dd, label); +#ifdef ADIAR_STATS + // HACK: Undo the += 1 in the nested call + stats_quantify.runs -= 1u; +#endif if (dd_isterminal(dd)) { return dd; } label = __quantify__get_deepest(dd, pred); @@ -1561,21 +1570,21 @@ namespace adiar::internal if (transposition__max_iterations == 0) { // Singleton Quantification of bottom-most level #ifdef ADIAR_STATS - stats_quantify.singleton_sweeps += 1u; + stats_quantify.nested_transposition.pruning += 1u; #endif pruning_quantify_policy pruning_impl(pred); transposed = select(ep, std::move(dd), pruning_impl); } else { // Partial Quantification #ifdef ADIAR_STATS - stats_quantify.partial_sweeps += 1u; + stats_quantify.nested_transposition.partial += 1u; #endif partial_quantify_policy partial_impl(pred); transposed = __quantify(ep, std::move(dd), partial_impl); if (partial_impl.remaining_nodes == 0) { #ifdef ADIAR_STATS - stats_quantify.partial_termination += 1u; + stats_quantify.nested_transposition.partial_terminations += 1u; #endif return transposed; } @@ -1587,15 +1596,14 @@ namespace adiar::internal partial_impl.reset(); #ifdef ADIAR_STATS - stats_quantify.partial_sweeps += 1u; - stats_quantify.partial_repetitions += 1u; + stats_quantify.nested_transposition.partial_repetitions += 1u; #endif transposed = __quantify(ep, transposed, partial_impl); // Reduce result, if no work is left to be done. if (partial_impl.remaining_nodes == 0) { #ifdef ADIAR_STATS - stats_quantify.partial_termination += 1u; + stats_quantify.nested_transposition.partial_terminations += 1u; #endif return transposed; } @@ -1641,6 +1649,11 @@ namespace adiar::internal return quantify(ep, typename Policy::dd_type(std::move(__dd)), pred); } +#ifdef ADIAR_STATS + stats_quantify.runs += 1u; + stats_quantify.nested_transposition.none += 1u; + stats_quantify.nested_sweeps += 1u; +#endif multi_quantify_policy__pred inner_impl(pred); return nested_sweep<>(ep, std::move(__dd), inner_impl); } @@ -1750,6 +1763,10 @@ namespace adiar::internal typename Policy::dd_type dd, const typename multi_quantify_policy__generator::generator_t& lvls) { +#ifdef ADIAR_STATS + stats_quantify.runs += 1u; +#endif + switch (ep.template get()) { case exec_policy::quantify::Singleton: { // ------------------------------------------------------------------------------------------- @@ -1769,16 +1786,22 @@ namespace adiar::internal // 'next_on_level' to see whether it is the last one. optional next_on_level = lvls(); while (next_on_level) { + dd = quantify(ep, dd, on_level.value()); #ifdef ADIAR_STATS - stats_quantify.singleton_sweeps += 1u; + // HACK: Undo the += 1 in the nested call + stats_quantify.runs -= 1u; #endif - dd = quantify(ep, dd, on_level.value()); if (dd_isterminal(dd)) { return dd; } on_level = next_on_level; next_on_level = lvls(); } - return quantify(ep, dd, on_level.value()); + const typename Policy::__dd_type out = quantify(ep, dd, on_level.value()); +#ifdef ADIAR_STATS + // HACK: Undo the += 1 in the nested call + stats_quantify.runs -= 1u; +#endif + return std::move(out); } else { // !Policy::quantify_onset // TODO: only designed for 'OR' at this point in time if (!on_level) { return typename Policy::dd_type(dd->number_of_terminals[true] > 0); } @@ -1790,10 +1813,11 @@ namespace adiar::internal if (Policy::max_label < off_level) { break; } + dd = quantify(ep, dd, off_level); #ifdef ADIAR_STATS - stats_quantify.singleton_sweeps += 1u; + // HACK: Undo the += 1 in the nested call + stats_quantify.runs -= 1u; #endif - dd = quantify(ep, dd, off_level); if (dd_isterminal(dd)) { return dd; } } @@ -1808,10 +1832,11 @@ namespace adiar::internal if (Policy::max_label < off_level) { break; } + dd = quantify(ep, dd, off_level); #ifdef ADIAR_STATS - stats_quantify.singleton_sweeps += 1u; + // HACK: Undo the += 1 in the nested call + stats_quantify.runs -= 1u; #endif - dd = quantify(ep, dd, off_level); if (dd_isterminal(dd)) { return dd; } } @@ -1882,19 +1907,21 @@ namespace adiar::internal adiar_assert(transposition_level.has_value()); // Quantify the 'transposition_level' as part of the initial transposition step -#ifdef ADIAR_STATS - stats_quantify.singleton_sweeps += 1u; -#endif typename Policy::__dd_type transposed = quantify(ep, dd, transposition_level.value()); #ifdef ADIAR_STATS + stats_quantify.nested_transposition.singleton += 1u; stats_quantify.nested_sweeps += 1u; + // HACK: Undo the two += 1 in the nested call + stats_quantify.runs -= 1u; + stats_quantify.singleton_sweeps -= 1u; #endif multi_quantify_policy__generator inner_impl(lvls); return nested_sweep<>(ep, std::move(transposed), inner_impl); } else { // !Policy::quantify_onset #ifdef ADIAR_STATS + stats_quantify.nested_transposition.simple += 1u; stats_quantify.nested_sweeps += 1u; #endif multi_quantify_policy__generator inner_impl(lvls); @@ -1929,6 +1956,11 @@ namespace adiar::internal return quantify(ep, typename Policy::dd_type(std::move(__dd)), lvls); } +#ifdef ADIAR_STATS + stats_quantify.runs += 1u; + stats_quantify.nested_transposition.none += 1u; + stats_quantify.nested_sweeps += 1u; +#endif multi_quantify_policy__generator inner_impl(lvls); return nested_sweep<>(ep, std::move(__dd), inner_impl); } diff --git a/src/adiar/statistics.cpp b/src/adiar/statistics.cpp index 93b1099ed..9616799ef 100644 --- a/src/adiar/statistics.cpp +++ b/src/adiar/statistics.cpp @@ -492,9 +492,7 @@ namespace adiar void __printstat_quantify(std::ostream& o) { - const uintwide total_runs = internal::stats_quantify.skipped - + internal::stats_quantify.singleton_sweeps - + (internal::stats_quantify.partial_sweeps - internal::stats_quantify.partial_repetitions); + const uintwide total_runs = internal::stats_quantify.runs; o << indent << bold_on << label << "Quantification" << bold_off << total_runs << endl; @@ -521,33 +519,52 @@ namespace adiar { o << indent << endl; - o << indent << bold_on << label << "case [partial sweep]" << bold_off - << internal::stats_quantify.partial_sweeps << endl; + o << indent << bold_on << label << "case [nested sweep]" << bold_off + << internal::stats_quantify.nested_sweeps << " = " + << internal::percent_frac(internal::stats_quantify.nested_sweeps, total_runs) << percent + << endl; indent_level++; - o << indent << label << "repeated transpositions" - << internal::stats_quantify.partial_repetitions << " = " - << internal::percent_frac(internal::stats_quantify.partial_repetitions, - internal::stats_quantify.partial_sweeps) - << percent << endl; - o << indent << label << "termination" << internal::stats_quantify.partial_termination << " = " - << internal::percent_frac(internal::stats_quantify.partial_termination, - internal::stats_quantify.partial_sweeps) - << percent << endl; + { + o << indent << bold_on << label << "transposition" << bold_off << endl; - indent_level--; - } + indent_level++; + o << indent << label << "none" << internal::stats_quantify.nested_transposition.none + << endl; - { - o << indent << endl; + o << indent << label << "simple" << internal::stats_quantify.nested_transposition.simple + << endl; - o << indent << bold_on << label << "case [nested sweep]" << bold_off - << internal::stats_quantify.nested_sweeps << " = " - << internal::percent_frac(internal::stats_quantify.nested_sweeps, total_runs) << percent - << endl; + o << indent << label << "singleton quantification" + << internal::stats_quantify.nested_transposition.singleton << endl; - indent_level++; + o << indent << label << "pruning" << internal::stats_quantify.nested_transposition.pruning + << endl; + + o << indent << label << "partial quantification" << bold_off + << internal::stats_quantify.nested_transposition.partial << endl; + + indent_level++; + + o << indent << label << "repetitions" + << internal::stats_quantify.nested_transposition.partial_repetitions << " = " + << internal::percent_frac( + internal::stats_quantify.nested_transposition.partial_repetitions, + internal::stats_quantify.nested_transposition.partial) + << percent << endl; + o << indent << label << "terminations" + << internal::stats_quantify.nested_transposition.partial_terminations << " = " + << internal::percent_frac( + internal::stats_quantify.nested_transposition.partial_terminations, + internal::stats_quantify.nested_transposition.partial) + << percent << endl; + + indent_level--; + + indent_level--; + } + o << indent << endl; const uintwide total_roots = internal::stats_quantify.nested_policy.shortcut_terminal + internal::stats_quantify.nested_policy.shortcut_node diff --git a/src/adiar/statistics.h b/src/adiar/statistics.h index 207d3bcce..599dbbb0d 100644 --- a/src/adiar/statistics.h +++ b/src/adiar/statistics.h @@ -401,6 +401,11 @@ namespace adiar //////////////////////////////////////////////////////////////////////////////////////////////// struct quantify_t : public __alg_base { + ////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Number of calls to quantification operation. + ////////////////////////////////////////////////////////////////////////////////////////////// + uintwide runs = 0; + ////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Number of bailed-out quantifications for non-existent labels. ////////////////////////////////////////////////////////////////////////////////////////////// @@ -412,24 +417,51 @@ namespace adiar uintwide singleton_sweeps = 0; ////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Number of *partial* multi-variable sweeps. + /// \brief Number of *nested* multi-variable sweeps. ////////////////////////////////////////////////////////////////////////////////////////////// - uintwide partial_sweeps = 0; + uintwide nested_sweeps = 0; ////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Number of early-termination during *partial* sweeps. + /// \brief Transposition algorithms prior to nested multi-variable sweeping. ////////////////////////////////////////////////////////////////////////////////////////////// - uintwide partial_termination = 0; + struct nested_transposition_t + { + ////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Number of skipped transpositions (already transposed). + ////////////////////////////////////////////////////////////////////////////////////////////// + uintwide none = 0; - ////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Number of *partial* multi-variable sweeps that are repeated partial transposition. - ////////////////////////////////////////////////////////////////////////////////////////////// - uintwide partial_repetitions = 0; + ////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Number of simple transposition sweeps. + ////////////////////////////////////////////////////////////////////////////////////////////// + uintwide simple = 0; - ////////////////////////////////////////////////////////////////////////////////////////////// - /// \brief Number of *nested* multi-variable sweeps. - ////////////////////////////////////////////////////////////////////////////////////////////// - uintwide nested_sweeps = 0; + ////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Number of single-variable transposition sweeps. + ////////////////////////////////////////////////////////////////////////////////////////////// + uintwide singleton = 0; + + ////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Number of *pruning* multi-variable transposition sweeps. + ////////////////////////////////////////////////////////////////////////////////////////////// + uintwide pruning = 0; + + ////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Number of *partial* multi-variable transposition sweeps. + ////////////////////////////////////////////////////////////////////////////////////////////// + uintwide partial = 0; + + ////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Number of early-termination during *partial* transposition sweeps. + ////////////////////////////////////////////////////////////////////////////////////////////// + uintwide partial_terminations = 0; + + ////////////////////////////////////////////////////////////////////////////////////////////// + /// \brief Number of *partial* multi-variable sweeps that are repeated partial + /// transposition. + ////////////////////////////////////////////////////////////////////////////////////////////// + uintwide partial_repetitions = 0; + } nested_transposition; ////////////////////////////////////////////////////////////////////////////////////////////// /// \brief Nested multi-variable sweeping.