Update Intercut-based algorithms to use Generators/Iterators

Since we (1) may have to read the input in reverse or (2) we need to retrieve
from two different places (once for the priority queue and once for the
algorithm), we still copy the entire input into a file. Hopefully, we can find a
better solution some other day.

src/adiar/bdd.h

@@ -875,14 +875,27 @@ namespace adiar
   ///
   /// \param A   Family of a set (within the given domain)
   ///
-  /// \param dom Domain of all variables (in ascending order)
+  /// \param dom Generator function of domain variables in ascending order
   ///
   /// \returns   BDD that is true for the exact same assignments to variables in
   ///            the given domain.
+  //////////////////////////////////////////////////////////////////////////////
+  __bdd bdd_from(const zdd &A, const std::function<bdd::label_t()> &dom);
+
+  //////////////////////////////////////////////////////////////////////////////
+  /// \brief     Obtains the BDD that represents the same function/set as the
+  ///            given ZDD within the given domain.
   ///
-  /// \pre       Labels in `dom` are provided in ascending order.
+  /// \param A   Family of a set (within the given domain)
+  ///
+  /// \param dom Iterator over the domain in ascending order
+  ///
+  /// \returns   BDD that is true for the exact same assignments to variables in
+  ///            the given domain.
   //////////////////////////////////////////////////////////////////////////////
-  __bdd bdd_from(const zdd &A, const shared_file<bdd::label_t> &dom);
+  template<typename IT>
+  __bdd bdd_from(const zdd &A, IT begin, IT end)
+  { return bdd_from(A, internal::iterator_gen<bdd::label_t>(begin, end)); }
 
   //////////////////////////////////////////////////////////////////////////////
   /// \copybrief bdd_from

src/adiar/bdd/bdd.cpp

@@ -163,15 +163,19 @@ namespace adiar
 
   //////////////////////////////////////////////////////////////////////////////
   // Conversion
-  __bdd bdd_from(const zdd &A, const shared_file<bdd::label_t> &dom)
+  __bdd bdd_from(const zdd &A, const std::function<bdd::label_t()> &dom)
   {
-    return internal::intercut<internal::convert_dd_policy<bdd_policy, zdd_policy>>(A, dom);
+    return internal::intercut<internal::convert_dd_policy<bdd_policy, zdd_policy>>
+      (A, dom);
   }
 
   __bdd bdd_from(const zdd &A)
   {
     const shared_file<bdd::label_t> dom = adiar_get_domain();
-    return internal::intercut<internal::convert_dd_policy<bdd_policy, zdd_policy>>(A, dom);
+    internal::file_stream<domain_var_t> ds(dom);
+
+    return internal::intercut<internal::convert_dd_policy<bdd_policy, zdd_policy>>
+      (A, internal::stream_gen<bdd::label_t>(ds));
   }
 
   //////////////////////////////////////////////////////////////////////////////

src/adiar/internal/algorithms/intercut.h

@@ -159,18 +159,37 @@ namespace adiar::internal
 
   template<typename intercut_policy, typename pq_t>
   typename intercut_policy::unreduced_t __intercut (const typename intercut_policy::reduced_t &dd,
-                                                    const shared_file<typename intercut_policy::label_t> &labels,
+                                                    const std::function<typename intercut_policy::label_t()> &xs,
                                                     const size_t pq_memory,
                                                     const size_t max_pq_size)
   {
     node_stream<> in_nodes(dd);
     node n = in_nodes.pull();
 
+    // TODO: Only copy `xs` into a `shared_file<label_t>`, in the degenerate
+    //       case, that we have to reverse it.
+    //
+    // In the general case, we have to use it both in the priority queue
+    // `intercut_pq` below, and for a lookahead of the algorithm. The main issue
+    // is how to design the priority queue such that it can retrieve, merge with
+    // `dd_levels`, and expose `xs`.
+    shared_file<typename intercut_policy::label_t> hit_levels;
+    {
+      file_writer<typename intercut_policy::label_t> lw(hit_levels);
+      for (auto x = xs(); x <= intercut_policy::MAX_LABEL; x = xs()) {
+        lw << x;
+      }
+
+      if (lw.size() == 0) {
+        return intercut_policy::on_empty_labels(dd);
+      }
+    }
+
     if (n.is_terminal()) {
-      return intercut_policy::on_terminal_input(n.value(), dd, labels);
+      return intercut_policy::on_terminal_input(n.value(), dd, hit_levels);
     }
 
-    file_stream<typename intercut_policy::label_t> ls(labels);
+    file_stream<typename intercut_policy::label_t> ls(hit_levels);
     typename intercut_policy::label_t l = ls.pull();
 
     shared_levelized_file<arc> out_arcs;
@@ -184,7 +203,7 @@ namespace adiar::internal
       });
     }
 
-    pq_t intercut_pq({dd_levels, labels}, pq_memory, max_pq_size, stats_intercut.lpq);
+    pq_t intercut_pq({dd_levels, hit_levels}, pq_memory, max_pq_size, stats_intercut.lpq);
 
     // Add request for root in the queue
     typename intercut_policy::label_t out_label = std::min(l, n.label());
@@ -297,12 +316,8 @@ namespace adiar::internal
 
   template<typename intercut_policy>
   typename intercut_policy::unreduced_t intercut(const typename intercut_policy::reduced_t &dd,
-                                                 const shared_file<typename intercut_policy::label_t> &labels)
+                                                 const std::function<typename intercut_policy::label_t()> &xs)
   {
-    if (labels->size() == 0) {
-      return intercut_policy::on_empty_labels(dd);
-    }
-
     // Compute amount of memory available for auxiliary data structures after
     // having opened all streams.
     //
@@ -333,21 +348,21 @@ namespace adiar::internal
 #endif
       return __intercut<intercut_policy,
                         intercut_priority_queue_t<0, memory_mode_t::INTERNAL>>
-        (dd, labels, pq_memory, max_pq_size);
+        (dd, xs, pq_memory, max_pq_size);
     } else if(!external_only && max_pq_size <= pq_memory_fits) {
 #ifdef ADIAR_STATS
       stats_intercut.lpq.internal += 1u;
 #endif
       return __intercut<intercut_policy,
                         intercut_priority_queue_t<ADIAR_LPQ_LOOKAHEAD, memory_mode_t::INTERNAL>>
-        (dd, labels, pq_memory, max_pq_size);
+        (dd, xs, pq_memory, max_pq_size);
     } else {
 #ifdef ADIAR_STATS
       stats_intercut.lpq.external += 1u;
 #endif
       return __intercut<intercut_policy,
                         intercut_priority_queue_t<ADIAR_LPQ_LOOKAHEAD, memory_mode_t::EXTERNAL>>
-        (dd, labels, pq_memory, max_pq_size);
+        (dd, xs, pq_memory, max_pq_size);
     }
   }
 }

src/adiar/zdd.h

@@ -339,28 +339,64 @@ namespace adiar
   /// \endcond
 
   //////////////////////////////////////////////////////////////////////////////
-  /// \brief     The symmetric difference between each set in the family and the
-  ///            given set of variables.
+  /// \brief      The symmetric difference between each set in the family and
+  ///             the given set of variables.
   ///
   /// \param A    ZDD to apply with the other.
   ///
-  /// \param vars Labels that should be flipped
+  /// \param vars Generator function of labels to flip in *ascending* order.
   ///
   /// \returns
   /// \f$ \{ \mathit{vars} \Delta a \mid a \in A \} \f$
   //////////////////////////////////////////////////////////////////////////////
-  __zdd zdd_change(const zdd &A, const shared_file<zdd::label_t> &vars);
+  __zdd zdd_change(const zdd &A, const std::function<zdd::label_t()> &vars);
+
+  //////////////////////////////////////////////////////////////////////////////
+  /// \brief      The symmetric difference between each set in the family and
+  ///             the given set of variables.
+  ///
+  /// \param A    ZDD to apply with the other.
+  ///
+  /// \param begin Iterator with variables to flip in *ascending* order.
+  ///
+  /// \param end   Iterator that marks the end for `begin`.
+  ///
+  /// \returns
+  /// \f$ \{ \mathit{vars} \Delta a \mid a \in A \} \f$
+  //////////////////////////////////////////////////////////////////////////////
+  template<typename IT>
+  __zdd zdd_change(const zdd &A, IT begin, IT end)
+  {
+    return zdd_change(A, internal::iterator_gen<zdd::label_t>(begin, end));
+  }
+
+  //////////////////////////////////////////////////////////////////////////////
+  /// \brief     Complement of A within the given domain.
+  ///
+  /// \param A   family of sets to complement
+  ///
+  /// \param dom Labels of the domain in *ascending* order
+  ///
+  /// \returns    \f$ 2^{\mathit{dom}} \setminus A \f$
+  //////////////////////////////////////////////////////////////////////////////
+  __zdd zdd_complement(const zdd &A, const std::function<zdd::label_t()> &dom);
 
   //////////////////////////////////////////////////////////////////////////////
   /// \brief     Complement of A within the given domain.
   ///
   /// \param A   family of sets to complement
   ///
-  /// \param dom Labels of the domain (in ascending order)
+  /// \param begin Iterator that provides the domain in *ascending* order.
+  ///
+  /// \param end   Iterator that marks the end for `begin`.
   ///
   /// \returns    \f$ 2^{\mathit{dom}} \setminus A \f$
   //////////////////////////////////////////////////////////////////////////////
-  __zdd zdd_complement(const zdd &A, const shared_file<zdd::label_t> &dom);
+  template<typename IT>
+  __zdd zdd_complement(const zdd &A, IT begin, IT end)
+  {
+    return zdd_complement(A, internal::iterator_gen<zdd::label_t>(begin, end));
+  }
 
   //////////////////////////////////////////////////////////////////////////////
   /// \brief     Complement of A within the global \ref module__domain
@@ -394,13 +430,35 @@ namespace adiar
   ///
   /// \param A    Family of set to expand
   ///
-  /// \param vars Labels of variables to expand with (in ascending order). This
-  ///             set of labels may \em not occur in A
+  /// \param vars Generator function of labels to expand with (in ascending
+  ///             order). This set of labels may \em not occur in A
+  ///
+  /// \returns
+  /// \f$ \bigcup_{a \in A, i \in 2^{vars}} (a \cup i) \f$
+  //////////////////////////////////////////////////////////////////////////////
+  __zdd zdd_expand(const zdd &A, const std::function<zdd::label_t()> &vars);
+
+  //////////////////////////////////////////////////////////////////////////////
+  /// \brief      Expands the domain of the given ZDD to also include the given
+  ///             set of labels.
+  ///
+  /// \details    Adds don't care nodes on each levels in `vars`. The variables
+  ///             in `vars` may \em not be present in `A`.
+  ///
+  /// \param A    Family of set to expand
+  ///
+  /// \param begin Iterator that provides the variables in *ascending* order.
+  ///
+  /// \param end   Iterator that marks the end for `begin`.
   ///
   /// \returns
   /// \f$ \bigcup_{a \in A, i \in 2^{vars}} (a \cup i) \f$
   //////////////////////////////////////////////////////////////////////////////
-  __zdd zdd_expand(const zdd &A, const shared_file<zdd::label_t> &vars);
+  template<typename IT>
+  __zdd zdd_expand(const zdd &A, IT begin, IT end)
+  {
+    return zdd_expand(A, internal::iterator_gen<zdd::label_t>(begin, end));
+  }
 
   //////////////////////////////////////////////////////////////////////////////
   /// \brief      Subset that do \em not include the given set of variables.
@@ -509,6 +567,8 @@ namespace adiar
   ///
   /// \param begin Iterator that provides the domain in *descending* order.
   ///
+  /// \param end   Iterator that marks the end for `begin`.
+  ///
   /// \returns
   /// \f$ \prod_{\mathit{dom}}(A) = \{ a \setminus \mathit{dom}^c \mid a \in A \} \f$
   //////////////////////////////////////////////////////////////////////////////
@@ -728,7 +788,7 @@ namespace adiar
   //////////////////////////////////////////////////////////////////////////////
   /// \brief   Retrieves the lexicographically smallest set a in A.
   ///
-  /// \param cb Callback function that is called in ascending order of the zdd's
+  /// \param cb Callback function that is called in *ascending* order of the zdd's
   ///           levels with the variable in the smallest set.
   ///
   /// \pre `A != zdd_empty()`
@@ -753,7 +813,7 @@ namespace adiar
   //////////////////////////////////////////////////////////////////////////////
   /// \brief   Retrieves the lexicographically largest set a in A.
   ///
-  /// \param cb Callback function that is called in ascending order of the zdd's
+  /// \param cb Callback function that is called in *ascending* order of the zdd's
   ///           levels with the variable in the largest set.
   ///
   /// \pre `A != zdd_empty()`
@@ -771,7 +831,7 @@ namespace adiar
   ///
   /// \param A  ZDD of interest.
   ///
-  /// \param cb Callback function that consumes the levels (in ascending order).
+  /// \param cb Callback function that consumes the levels in *ascending* order.
   //////////////////////////////////////////////////////////////////////////////
   void zdd_varprofile(const zdd &A, const std::function<void(zdd::label_t)> &cb);
 
@@ -813,12 +873,27 @@ namespace adiar
   ///
   /// \param f   Boolean function with the given domain
   ///
-  /// \param dom Domain of all variables (in ascending order)
+  /// \param dom Domain of all variables in *ascending* order.
   ///
   /// \returns   ZDD that is true for the exact same assignments to variables in
   ///            the given domain.
   //////////////////////////////////////////////////////////////////////////////
-  __zdd zdd_from(const bdd &f, const shared_file<zdd::label_t> &dom);
+  __zdd zdd_from(const bdd &f, const std::function<zdd::label_t()> &dom);
+
+  //////////////////////////////////////////////////////////////////////////////
+  /// \brief     Obtains the ZDD that represents the same function/set as the
+  ///            given BDD within the given domain.
+  ///
+  /// \param f   Boolean function with the given domain
+  ///
+  /// \param dom Iterator over the domain in *ascending* order
+  ///
+  /// \returns   BDD that is true for the exact same assignments to variables in
+  ///            the given domain.
+  //////////////////////////////////////////////////////////////////////////////
+  template<typename IT>
+  __zdd zdd_from(const bdd &f, IT begin, IT end)
+  { return zdd_from(f, internal::iterator_gen<bdd::label_t>(begin, end)); }
 
   //////////////////////////////////////////////////////////////////////////////
   /// \brief     Obtains the ZDD that represents the same function/set as the

src/adiar/zdd/build.cpp

@@ -67,9 +67,9 @@ namespace adiar
   zdd zdd_ithvar(const zdd::label_t var)
   {
     const shared_file<domain_var_t> dom = adiar_get_domain();
-    internal::file_stream<domain_var_t, true> s(dom);
+    internal::file_stream<domain_var_t, true> ds(dom);
 
-    return zdd_ithvar(var, internal::stream_gen<zdd::label_t>(s));
+    return zdd_ithvar(var, internal::stream_gen<zdd::label_t>(ds));
   }
 
   //////////////////////////////////////////////////////////////////////////////
@@ -104,9 +104,9 @@ namespace adiar
   zdd zdd_nithvar(const zdd::label_t var)
   {
     const shared_file<domain_var_t> dom = adiar_get_domain();
-    internal::file_stream<domain_var_t, true> s(dom);
+    internal::file_stream<domain_var_t, true> ds(dom);
 
-    return zdd_nithvar(var, internal::stream_gen<zdd::label_t>(s));
+    return zdd_nithvar(var, internal::stream_gen<zdd::label_t>(ds));
   }
 
   //////////////////////////////////////////////////////////////////////////////

src/adiar/zdd/change.cpp

@@ -58,8 +58,8 @@ namespace adiar
     }
   };
 
-  __zdd zdd_change(const zdd &dd, const shared_file<zdd::label_t> &labels)
+  __zdd zdd_change(const zdd &dd, const std::function<zdd::label_t()> &vars)
   {
-    return internal::intercut<zdd_change_policy>(dd, labels);
+    return internal::intercut<zdd_change_policy>(dd, vars);
   }
 }

src/adiar/zdd/complement.cpp

@@ -102,14 +102,17 @@ namespace adiar
     // LCOV_EXCL_STOP
   };
 
-  __zdd zdd_complement(const zdd &dd, const shared_file<zdd::label_t> &universe)
+  __zdd zdd_complement(const zdd &dd, const std::function<zdd::label_t()> &dom)
   {
-    return internal::intercut<zdd_complement_policy>(dd, universe);
+    return internal::intercut<zdd_complement_policy>(dd, dom);
   }
 
   __zdd zdd_complement(const zdd &dd)
   {
-    const shared_file<zdd::label_t> universe = adiar_get_domain();
-    return internal::intercut<zdd_complement_policy>(dd, universe);
+    const shared_file<zdd::label_t> dom = adiar_get_domain();
+    internal::file_stream<domain_var_t> ds(dom);
+
+    return internal::intercut<zdd_complement_policy>
+      (dd, internal::stream_gen<bdd::label_t>(ds));
   }
 }

src/adiar/zdd/expand.cpp

@@ -61,8 +61,8 @@ namespace adiar
     }
   };
 
-  __zdd zdd_expand(const zdd &dd, const shared_file<zdd::label_t> &labels)
+  __zdd zdd_expand(const zdd &dd, const std::function<zdd::label_t()> &vars)
   {
-    return internal::intercut<zdd_expand_policy>(dd, labels);
+    return internal::intercut<zdd_expand_policy>(dd, vars);
   }
 }