Add O(1) shifting case to 'bdd_replace'

Author: SSoelvsten

src/adiar/bdd/relprod.cpp

@@ -307,6 +307,7 @@ namespace adiar
       throw invalid_argument("Non-monotonic variable replacement not (yet) supported.");
 
     case replace_type::Monotone:
+    case replace_type::Shift:
     case replace_type::Identity:
 #ifdef ADIAR_STATS
       internal::stats_replace.monotonic_reduces += 1u;

src/adiar/internal/algorithms/replace.h

@@ -10,6 +10,7 @@
 
 #include <adiar/internal/algorithms/reduce.h>
 #include <adiar/internal/assert.h>
+#include <adiar/internal/dd_func.h>
 #include <adiar/internal/io/levelized_file_stream.h>
 #include <adiar/internal/io/node_file.h>
 #include <adiar/internal/io/node_stream.h>
@@ -60,19 +61,24 @@ namespace adiar::internal
   replace_type
   __replace__infer_type(LevelInfoStream& ls, const ReplaceFunction& m)
   {
-    using label_type  = typename Policy::label_type;
-    using result_type = typename ReplaceFunction::result_type;
+    using label_type        = typename Policy::label_type;
+    using signed_label_type = typename Policy::signed_label_type;
+    using result_type       = typename ReplaceFunction::result_type;
 
     constexpr bool is_total_map   = is_same<result_type, label_type>;
     constexpr bool is_partial_map = is_same<result_type, optional<label_type>>;
 
     static_assert(is_total_map || is_partial_map);
 
     bool identity = true;
+    bool shift    = true;
     bool monotone = true;
 
     label_type prev_before = Policy::max_label + 1;
     label_type prev_after  = Policy::max_label + 1;
+
+    signed_label_type prev_diff = 0;
+
     while (ls.can_pull()) {
       const label_type next_before     = ls.pull().level();
       const result_type next_after_opt = m(next_before);
@@ -89,6 +95,14 @@ namespace adiar::internal
         next_after = next_after_opt;
       }
 
+      if (shift) {
+        const signed_label_type next_diff =
+          static_cast<signed_label_type>(next_before) - static_cast<signed_label_type>(next_after);
+
+        shift &= Policy::max_label < prev_before || prev_diff == next_diff;
+        prev_diff = next_diff;
+      }
+
       identity &= next_before == next_after;
       monotone &= Policy::max_label < prev_before || prev_after < next_after;
 
@@ -97,13 +111,32 @@ namespace adiar::internal
     }
 
     if (!monotone) { return replace_type::Non_Monotone; }
-    if (!identity) { return replace_type::Monotone; }
+    if (!shift) { return replace_type::Monotone; }
+    if (!identity) { return replace_type::Shift; }
     return replace_type::Identity;
   }
 
   //////////////////////////////////////////////////////////////////////////////////////////////////
   // Algorithms
 
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Replace the level in constant time
+  ///
+  /// \remark This requires that the mapping, `m`, is *monotonic*.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  template <typename Policy>
+  inline typename Policy::dd_type
+  __replace__shift_return(const typename Policy::dd_type& dd, const replace_func<Policy>& m)
+  {
+    adiar_assert(!dd->is_terminal());
+
+    const typename Policy::signed_label_type topvar         = dd_topvar(dd);
+    const typename Policy::signed_label_type shifted_topvar = m(topvar);
+
+    return typename Policy::dd_type(
+      dd.file_ptr(), dd.is_negated(), dd.shift() + (shifted_topvar - topvar));
+  }
+
   //////////////////////////////////////////////////////////////////////////////////////////////////
   /// \brief Replace the level of all nodes in a single linear scan.
   ///
@@ -211,6 +244,12 @@ namespace adiar::internal
 #endif
       return __replace__monotonic_scan<Policy>(dd, m);
 
+    case replace_type::Shift:
+#ifdef ADIAR_STATS
+      stats_replace.shift_returns += 1u;
+#endif
+      return __replace__shift_return<Policy>(dd, m);
+
     case replace_type::Identity:
 #ifdef ADIAR_STATS
       stats_replace.identity_returns += 1u;
@@ -263,6 +302,7 @@ namespace adiar::internal
       throw invalid_argument("Non-monotonic variable replacement not (yet) supported.");
 
     case replace_type::Monotone:
+    case replace_type::Shift:
 #ifdef ADIAR_STATS
       stats_replace.monotonic_reduces += 1u;
 #endif

src/adiar/statistics.h

@@ -546,6 +546,12 @@ namespace adiar
       ////////////////////////////////////////////////////////////////////////////////////////////
       uintwide identity_reduces = 0;
 
+      ////////////////////////////////////////////////////////////////////////////////////////////
+      /// \brief Number of runs using 0 I/Os due to the variables are replaced according to a
+      ///        simple linear shift.
+      ////////////////////////////////////////////////////////////////////////////////////////////
+      uintwide shift_returns = 0;
+
       ////////////////////////////////////////////////////////////////////////////////////////////
       /// \brief Number of runs using a 2N/B linear copy-paste.
       ////////////////////////////////////////////////////////////////////////////////////////////

src/adiar/types.h

@@ -36,12 +36,11 @@ namespace adiar
     /** For any `x < y` then the mapped values preserve that order, i.e. `m(x) < m(y)`. */
     Monotone = 2,
 
-    /* TODO (constant time variable replacement): `m(x)` is of the form `ax + b` for a positive
-                                                  fraction `a` and integer `b`. */
-    // Affine      = 1,
+    /* TODO (faster version of 'Monotone'): `m(x) = ax + b` for some integers `a` and `b`. */
+    // Affine = 1,
 
-    /* TODO (faster version of 'Affine'): `m(x)` is of the form `x + b` for an integer `b`. */
-    // Shift       = 0,
+    /** (faster version of 'Monotone'): `m(x) = x + b` for an integer `b`. */
+    Shift = 0,
 
     /** Nothing needs to be done, as `m(x) = x`. */
     Identity = -1