Add 'quantify pred-profile' to have more information for heuristics

.github/workflows/mac.yml

@@ -36,14 +36,14 @@ jobs:
         os: [macos-latest]
         cc:
           # GNU Compiler
-          - { cc: gcc,   v: 10, cxx: g++, xcode: latest }
+          - { cc: gcc,   v: 11, cxx: g++, xcode: latest } # oldest supported on Apple Silicon
           - { cc: gcc,   v: 12, cxx: g++, xcode: latest }
+          - { cc: gcc,   v: 13, cxx: g++, xcode: latest }
 
           # Clang Compiler
-          - { cc: clang, cxx: clang++, xcode: 13.1 } # oldest
-          - { cc: clang, cxx: clang++, xcode: 13.4 }
-          - { cc: clang, cxx: clang++, xcode: 14.0 }
-          - { cc: clang, cxx: clang++, xcode: 14.2 } # newest
+          - { cc: clang, cxx: clang++, xcode: 14.3 } # oldest supported
+          - { cc: clang, cxx: clang++, xcode: 15.0 }
+          - { cc: clang, cxx: clang++, xcode: latest }
 
     steps:
     # Git repo set up
@@ -68,7 +68,7 @@ jobs:
       run: |
         if [ "${{matrix.cc.cc}}" = "gcc" ]; then
           echo "================================"
-          echo "Compiler"
+          echo GCC "Compiler"
           brew install ${{matrix.cc.cc}}@${{matrix.cc.v}}
         fi
 

src/adiar/bdd/restrict.cpp

@@ -1,6 +1,5 @@
 #include <adiar/bdd.h>
 #include <adiar/bdd/bdd_policy.h>
-
 #include <adiar/types.h>
 
 #include <adiar/internal/algorithms/select.h>
@@ -13,11 +12,13 @@ namespace adiar
 {
   //////////////////////////////////////////////////////////////////////////////
   template <typename AssignmentPolicy>
-  class bdd_restrict_policy : public bdd_policy, public AssignmentPolicy
+  class bdd_restrict_policy
+    : public bdd_policy
+    , public AssignmentPolicy
   {
   public:
     template <typename Arg>
-    bdd_restrict_policy(const Arg &a)
+    bdd_restrict_policy(const Arg& a)
       : AssignmentPolicy(a)
     {}
 

src/adiar/internal/algorithms/quantify.h

@@ -1232,29 +1232,19 @@ namespace adiar::internal
     {
       // -------------------------------------------------------------------------------------------
       // CASE: Not to-be quantified node.
-      if (!_pred_result) {
-        return n;
-      }
+      if (!_pred_result) { return n; }
 
       // -------------------------------------------------------------------------------------------
       // CASE: Prune low()
       //
       // TODO (ZDD): Remove 'Policy::keep_terminal' depending on semantics in Policy
-      if (Policy::collapse_to_terminal(n.low())) {
-        return n.low();
-      }
-      if (n.low().is_terminal() && !Policy::keep_terminal(n.low())) {
-        return n.high();
-      }
+      if (Policy::collapse_to_terminal(n.low())) { return n.low(); }
+      if (n.low().is_terminal() && !Policy::keep_terminal(n.low())) { return n.high(); }
 
       // -------------------------------------------------------------------------------------------
       // CASE: Prune high()
-      if (Policy::collapse_to_terminal(n.high())) {
-        return n.high();
-      }
-      if (n.high().is_terminal() && !Policy::keep_terminal(n.high())) {
-        return n.low();
-      }
+      if (Policy::collapse_to_terminal(n.high())) { return n.high(); }
+      if (n.high().is_terminal() && !Policy::keep_terminal(n.high())) { return n.low(); }
 
       // -------------------------------------------------------------------------------------------
       // No pruning possible. Do nothing.
@@ -1359,72 +1349,139 @@ namespace adiar::internal
   };
 
   //////////////////////////////////////////////////////////////////////////////////////////////////
-  /// \brief Obtain the deepest level that satisfies (or not) the requested level.
-  //////////////////////////////////////////////////////////////////////////////////////////////////
-  // TODO: optimisations
-  //       - initial cheap check on is_terminal.
-  //       - initial '__quantify__get_deepest' should not terminate early but
-  //         determine whether any variable may "survive".
   template <typename Policy>
-  inline typename Policy::label_type
-  __quantify__get_deepest(const typename Policy::dd_type& dd,
-                          const predicate<typename Policy::label_type>& pred)
+  struct quantify__pred_profile
   {
-    level_info_stream<true /* bottom-up */> lis(dd);
+  private:
+  public:
+    /// \brief Total number of nodes in the diagram.
+    size_t dd_size;
 
-    while (lis.can_pull()) {
-      const typename Policy::label_type l = lis.pull().label();
-      if (pred(l) == Policy::quantify_onset) { return l; }
-    }
-    return Policy::max_label + 1;
-  }
+    /// \brief Width of the diagram.
+    size_t dd_width;
+
+    /// \brief Total number of variables in the diagram.
+    size_t dd_vars;
+
+    /// \brief Number of nodes of *all* to-be quantified levels.
+    size_t quant_all_size = 0u;
+
+    /// \brief Number of *all* to-be quantified levels.
+    size_t quant_all_vars = 0u;
+
+    /// \brief Number of *deep* to-be quantified levels, i.e. the last N/3 nodes.
+    size_t quant_deep_vars = 0u;
+
+    /// \brief Number of *shallow* to-be quantified levels, i.e. the first N/3 nodes.
+    size_t quant_shallow_vars = 0u;
+
+    struct var_data
+    {
+      /// \brief The to-be quantified variable.
+      typename Policy::label_type level;
+
+      /// \brief Number of nodes below this level (not inclusive)
+      size_t nodes_below;
+
+      /// \brief Number of nodes on said level
+      typename Policy::id_type width;
+    };
+
+    /// \brief The *deepest* to-be quantified level.
+    var_data deepest_var{ 0, std::numeric_limits<size_t>::max(), Policy::max_id + 1 };
+
+    /// \brief The *shallowest* to-be quantified level.
+    var_data shallowest_var{ Policy::max_label + 1,
+                             std::numeric_limits<size_t>::max(),
+                             Policy::max_id + 1 };
+
+    /// \brief The *widest* to-be quantified level.
+    var_data widest_var{
+      Policy::max_label + 1,
+      std::numeric_limits<size_t>::max(),
+      0,
+    };
+
+    /// \brief The *narrowest* to-be quantified level.
+    var_data narrowest_var{ Policy::max_label + 1,
+                            std::numeric_limits<size_t>::max(),
+                            Policy::max_id + 1 };
+  };
 
   //////////////////////////////////////////////////////////////////////////////////////////////////
-  /// \brief Heuristically derive a bound for the number of partial sweeps based on the graph meta
-  ///        data.
+  /// \brief Obtain the deepest level that satisfies (or not) the requested level.
   //////////////////////////////////////////////////////////////////////////////////////////////////
   template <typename Policy>
-  inline typename Policy::label_type
-  __quantify__max_partial_sweeps(const typename Policy::dd_type& dd,
-                                 const predicate<typename Policy::label_type>& pred)
+  inline quantify__pred_profile<Policy>
+  __quantify__pred_profile(const typename Policy::dd_type& dd,
+                           const predicate<typename Policy::label_type>& pred)
   {
-    // Extract meta data constants about the DAG
-    const size_t size  = dd.size();
-    const size_t width = dd.width();
-
-    // ---------------------------------------------------------------------------------------------
-    // Shallow Variables Heuristic
+    // TODO: tighten 'shallow' to only be above shallowest widest level (inclusive)
+    // TODO: tighten 'deep' to not be 'shallow'
 
-    // Keep track of the number of nodes on the top-most levels in relation to the total size
-    size_t seen_nodes = 0u;
+    quantify__pred_profile<Policy> res;
+    res.dd_size  = dd_nodecount(dd);
+    res.dd_width = dd_width(dd);
+    res.dd_vars  = dd_varcount(dd);
 
-    // Threshold to stop after the first n/3 nodes.
-    const size_t max_nodes = size / 3;
+    level_info_stream<false /* top-down */> lis(dd);
 
-    // TODO: Turn `shallow_variables` into a double and decrease the weight of to-be quantified
-    //       variables depending on `seen_nodes`, the number of levels of width `width`, and/or in
-    //       general using a (quadratic?) decay.
-    typename Policy::label_type shallow_variables = 0u;
+    size_t shallow_threshold = res.dd_size / 3;
 
-    level_info_stream<false /*top-down*/> lis(dd);
+    size_t nodes_above       = 0u;
+    size_t nodes_below       = res.dd_size;
 
     while (lis.can_pull()) {
       const level_info li = lis.pull();
 
-      if (pred(li.label()) == Policy::quantify_onset) { shallow_variables++; }
+      nodes_below -= li.width();
 
-      // Stop at the (first) widest level
-      if (li.width() == width) { break; }
+      if (pred(li.label()) == Policy::quantify_onset) {
+        res.quant_all_vars += 1u;
+        res.quant_all_size += li.width();
+        res.quant_deep_vars += nodes_below < shallow_threshold;
+        res.quant_shallow_vars += nodes_above <= shallow_threshold;
 
-      // Stop when having seen too many nodes
-      seen_nodes += li.width();
-      if (max_nodes < seen_nodes) { break; }
+        { // Deepest variable (always updated due to top-down direction).
+          res.deepest_var.level       = li.level();
+          res.deepest_var.nodes_below = nodes_below;
+          res.deepest_var.width       = li.width();
+        }
+        // Shallowest variable
+        if (res.shallowest_var.level < li.level()) { res.shallowest_var = res.deepest_var; }
+        // Widest variable
+        if (res.widest_var.width < li.width()) { res.widest_var = res.deepest_var; }
+        // Narrowest variable
+        if (li.width() < res.narrowest_var.width) { res.narrowest_var = res.deepest_var; }
+      }
+
+      if (li.width() == res.dd_width) {
+        shallow_threshold = std::min(shallow_threshold, nodes_above);
+      }
+      nodes_above += li.width();
     }
+    return res;
+  }
 
-    adiar_assert(shallow_variables <= Policy::max_label);
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Obtain the deepest level that satisfies (or not) the requested level.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  // TODO: optimisations
+  //       - initial cheap check on is_terminal.
+  //       - initial '__quantify__get_deepest' should not terminate early but
+  //         determine whether any variable may "survive".
+  template <typename Policy>
+  inline typename Policy::label_type
+  __quantify__get_deepest(const typename Policy::dd_type& dd,
+                          const predicate<typename Policy::label_type>& pred)
+  {
+    level_info_stream<true /* bottom-up */> lis(dd);
 
-    // ---------------------------------------------------------------------------------------------
-    return shallow_variables;
+    while (lis.can_pull()) {
+      const typename Policy::label_type l = lis.pull().label();
+      if (pred(l) == Policy::quantify_onset) { return l; }
+    }
+    return Policy::max_label + 1;
   }
 
   //////////////////////////////////////////////////////////////////////////////////////////////////
@@ -1439,22 +1496,31 @@ namespace adiar::internal
     using unreduced_t = typename Policy::__dd_type;
     // TODO: check for missing std::move(...)
 
-    typename Policy::label_type label = __quantify__get_deepest<Policy>(dd, pred);
+    const quantify__pred_profile<Policy> pred_profile = __quantify__pred_profile<Policy>(dd, pred);
 
-    if (Policy::max_label < label) {
+    // -----------------------------------------------------------------------
+    // Case: Nothing to do
+    if (pred_profile.quant_all_vars == 0u) {
 #ifdef ADIAR_STATS
       stats_quantify.skipped += 1u;
 #endif
       return dd;
     }
 
+    // -----------------------------------------------------------------------
+    // Case: Only one variable to quantify
+    //
+    // TODO: pred_profile.quant_all_vars == 1u
+
     switch (ep.template get<exec_policy::quantify::algorithm>()) {
     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);
         if (dd_isterminal(dd)) { return dd; }
@@ -1467,19 +1533,18 @@ namespace adiar::internal
     case exec_policy::quantify::Nested: {
       // ---------------------------------------------------------------------
       // Case: Nested Sweeping
-      const size_t dd_size = dd.size();
 
       // Do Partial Quantification as long as...
       //   1. ... it stays smaller than 1+epsilon of the input size.
       const size_t transposition__size_threshold = (std::min(
         static_cast<double>(std::numeric_limits<size_t>::max() / 2u),
         static_cast<double>(ep.template get<exec_policy::quantify::transposition_growth>())
-          * static_cast<double>(dd_size)));
+          * static_cast<double>(pred_profile.dd_size)));
 
       //   2. ... it has not run more than the maximum number of iterations.
       const size_t transposition__max_iterations =
         std::min<size_t>({ ep.template get<exec_policy::quantify::transposition_max>(),
-                           __quantify__max_partial_sweeps<Policy>(dd, pred) });
+                           pred_profile.quant_shallow_vars });
 
       unreduced_t transposed;
 

src/adiar/internal/algorithms/select.h

@@ -133,9 +133,7 @@ namespace adiar::internal
         if (std::holds_alternative<typename Policy::node_type>(rec)) {
           const node rec_node = std::get<typename Policy::node_type>(rec);
 
-          if constexpr (Policy::skip_reduce) {
-            output_changes |= rec_node != n;
-          }
+          if constexpr (Policy::skip_reduce) { output_changes |= rec_node != n; }
 
           // Output/Forward outgoing arcs
           __select_recurse_out(pq, aw, n.uid().as_ptr(false), rec_node.low());
@@ -155,9 +153,7 @@ namespace adiar::internal
           const typename Policy::pointer_type rec_target =
             std::get<typename Policy::pointer_type>(rec);
 
-          if constexpr (Policy::skip_reduce) {
-            output_changes = true;
-          }
+          if constexpr (Policy::skip_reduce) { output_changes = true; }
 
           // Output/Forward extension of arc
           while (pq.can_pull() && pq.top().target == n.uid()) {
@@ -222,22 +218,19 @@ namespace adiar::internal
 #ifdef ADIAR_STATS
       stats_select.lpq.unbucketed += 1u;
 #endif
-      return __select<Policy,
-                      select_priority_queue_t<0, memory_mode::Internal>>(
+      return __select<Policy, select_priority_queue_t<0, memory_mode::Internal>>(
         ep, dd, policy, aux_available_memory, max_pq_size);
     } else if (!external_only && max_pq_size <= pq_memory_fits) {
 #ifdef ADIAR_STATS
       stats_select.lpq.internal += 1u;
 #endif
-      return __select<Policy,
-                      select_priority_queue_t<ADIAR_LPQ_LOOKAHEAD, memory_mode::Internal>>(
+      return __select<Policy, select_priority_queue_t<ADIAR_LPQ_LOOKAHEAD, memory_mode::Internal>>(
         ep, dd, policy, aux_available_memory, max_pq_size);
     } else {
 #ifdef ADIAR_STATS
       stats_select.lpq.external += 1u;
 #endif
-      return __select<Policy,
-                      select_priority_queue_t<ADIAR_LPQ_LOOKAHEAD, memory_mode::External>>(
+      return __select<Policy, select_priority_queue_t<ADIAR_LPQ_LOOKAHEAD, memory_mode::External>>(
         ep, dd, policy, aux_available_memory, max_pq_size);
     }
   }

src/adiar/internal/dd_func.h

@@ -131,6 +131,16 @@ namespace adiar::internal
     return dd->levels();
   }
 
+  ////////////////////////////////////////////////////////////////////////////
+  /// \brief Number of nodes on the widest level of a decision diagram.
+  ////////////////////////////////////////////////////////////////////////////
+  template <typename DD>
+  size_t
+  dd_width(const DD& dd)
+  {
+    return dd.width();
+  }
+
   ////////////////////////////////////////////////////////////////////////////
   /// \brief The variable labels (in order of their level) that are present in a
   ///        decision diagram.