Fix statistics for quantification runs and transposition sweeps are m…

…isleading

Warning: this is technically a breaking change to the public API. Sorry! But, you didn't
use this part anyway... right...?

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

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<typename Policy::label_type>& 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<Policy>(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<Policy>(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<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<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<Policy>(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<Policy> 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<Policy>::generator_t& lvls)
   {
+#ifdef ADIAR_STATS
+    stats_quantify.runs += 1u;
+#endif
+
     switch (ep.template get<exec_policy::quantify::algorithm>()) {
     case exec_policy::quantify::Singleton: {
       // -------------------------------------------------------------------------------------------
@@ -1769,16 +1786,22 @@ namespace adiar::internal
         // 'next_on_level' to see whether it is the last one.
         optional<typename Policy::label_type> next_on_level = lvls();
         while (next_on_level) {
+          dd = quantify<Policy>(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<Policy>(ep, dd, on_level.value());
           if (dd_isterminal(dd)) { return dd; }
 
           on_level      = next_on_level;
           next_on_level = lvls();
         }
-        return quantify<Policy>(ep, dd, on_level.value());
+        const typename Policy::__dd_type out = quantify<Policy>(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<Policy>(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<Policy>(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<Policy>(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<Policy>(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<Policy>(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<Policy> 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<Policy> inner_impl(lvls);
@@ -1929,6 +1956,11 @@ namespace adiar::internal
         return quantify<Policy>(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<Policy> inner_impl(lvls);
       return nested_sweep<>(ep, std::move(__dd), inner_impl);
     }

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

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.