Add bdd_replace

makefile

@@ -111,6 +111,9 @@ test/adiar/bdd/negate:
 test/adiar/bdd/quantify:
 	$(MAKE) $(MAKE_FLAGS) test TEST_FOLDER=test/adiar/bdd TEST_NAME=quantify
 
+test/adiar/bdd/replace:
+	$(MAKE) $(MAKE_FLAGS) test TEST_FOLDER=test/adiar/bdd TEST_NAME=replace
+
 test/adiar/bdd/restrict:
 	$(MAKE) $(MAKE_FLAGS) test TEST_FOLDER=test/adiar/bdd TEST_NAME=restrict
 

src/adiar/CMakeLists.txt

@@ -55,6 +55,7 @@ set(HEADERS
   internal/algorithms/prod2.h
   internal/algorithms/quantify.h
   internal/algorithms/reduce.h
+  internal/algorithms/replace.h
   internal/algorithms/select.h
   internal/algorithms/traverse.h
 
@@ -117,6 +118,7 @@ set(SOURCES
   bdd/optmin.cpp
   bdd/pred.cpp
   bdd/quantify.cpp
+  bdd/replace.cpp
   bdd/restrict.cpp
 
   # adiar/zdd/
@@ -144,6 +146,7 @@ set(SOURCES
   internal/algorithms/prod2.cpp
   internal/algorithms/quantify.cpp
   internal/algorithms/reduce.cpp
+  internal/algorithms/replace.cpp
   internal/algorithms/select.cpp
 
   # adiar/internal/data_structures

src/adiar/bdd.h

@@ -1331,7 +1331,7 @@ namespace adiar
   bdd_satcount(const bdd& f);
 
   //////////////////////////////////////////////////////////////////////////////////////////////////
-  /// \brief   Count the number of assignments x that make f(x) true.
+  /// \brief   Count the number of assignments *x that make f(x) true.
   //////////////////////////////////////////////////////////////////////////////////////////////////
   uint64_t
   bdd_satcount(const exec_policy& ep, const bdd& f);
@@ -1344,6 +1344,120 @@ namespace adiar
   ///
   /// \{
 
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Replace variables in *f* according to the mapping in *m*.
+  ///
+  /// \param f
+  ///    BDD to replace variables within
+  ///
+  /// \param m
+  ///    Function from BDD label to another (or itself).
+  ///
+  /// \throws invalid_argument if `m` is not a monotonic relabelling.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_replace(const bdd& f, const function<bdd::label_type(bdd::label_type)>& m);
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Replace variables in *f* according to the mapping in *m*.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_replace(const exec_policy& ep,
+              const bdd& f,
+              const function<bdd::label_type(bdd::label_type)>& m);
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Replace variables in *f* according to the mapping in *m*.
+  ///
+  /// \param f
+  ///    BDD to replace variables within
+  ///
+  /// \param m
+  ///    Function from BDD label to another (or itself).
+  ///
+  /// \param m_type
+  ///    Guarantees on the class of variable relabelling, e.g. whether it is monotonic.
+  ///
+  /// \throws invalid_argument if `m_type` classifies `m` as not monotonic.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_replace(const bdd& f,
+              const function<bdd::label_type(bdd::label_type)>& m,
+              replace_type m_type);
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Replace variables in *f* according to the mapping in *m*.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_replace(const exec_policy& ep,
+              const bdd& f,
+              const function<bdd::label_type(bdd::label_type)>& m,
+              replace_type m_type);
+
+  /// \cond
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Replace variables in *f* according to the mapping in *m*.
+  ///
+  /// \details Unlike the `bdd_replace(const bdd& f, ...)` variants, this saves *2N/B* I/Os by
+  ///          incorporating the renaming into the Reduce algorithm.
+  ///
+  /// \param f
+  ///    Possibly unreduced BDD to replace variables within
+  ///
+  /// \param m
+  ///    Function from BDD label to another (or itself).
+  ///
+  /// \throws invalid_argument if `m` is not monotonic.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_replace(__bdd&& f, const function<bdd::label_type(bdd::label_type)>& m);
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Replace variables in *f* according to the mapping in *m*.
+  ///
+  /// \details Unlike the `bdd_replace(const bdd& f, ...)` variants, this saves *2N/B* I/Os by
+  ///          incorporating the renaming into the Reduce algorithm.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_replace(const exec_policy& ep,
+              __bdd&& f,
+              const function<bdd::label_type(bdd::label_type)>& m);
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Replace variables in *f* according to the mapping in *m*.
+  ///
+  /// \details Unlike the `bdd_replace(const bdd& f, ...)` variants, this saves *2N/B* I/Os by
+  ///          incorporating the renaming into the Reduce algorithm.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_replace(__bdd&& f, const function<bdd::label_type(bdd::label_type)>& m, replace_type m_type);
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Replace variables in *f* according to the mapping in *m*.
+  ///
+  /// \details Unlike the `bdd_replace(const bdd& f, ...)` variants, this saves *2N/B* I/Os by
+  ///          incorporating the renaming into the Reduce algorithm.
+  ///
+  /// \param f
+  ///    Possibly unreduced BDD to replace variables within
+  ///
+  /// \param m
+  ///    Function from BDD label to another (or itself).
+  ///
+  /// \param m_type
+  ///    Guarantees on the class of variable relabelling, e.g. whether it is monotonic.
+  ///
+  /// \throws invalid_argument if `m_type` classifies `m` as not monotonic.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_replace(const exec_policy& ep,
+              __bdd&& f,
+              const function<bdd::label_type(bdd::label_type)>& m,
+              replace_type m_type);
+
+  /// \endcond
+
   //////////////////////////////////////////////////////////////////////////////////////////////////
   /// \brief Get (in \em ascending order) all of the variable labels that occur
   ///        in the BDD.

src/adiar/bdd/replace.cpp

@@ -0,0 +1,67 @@
+#include <adiar/bdd.h>
+#include <adiar/bdd/bdd_policy.h>
+#include <adiar/functional.h>
+#include <adiar/types.h>
+
+#include <adiar/internal/algorithms/replace.h>
+
+namespace adiar
+{
+  bdd
+  bdd_replace(const exec_policy& ep,
+              const bdd& f,
+              const function<bdd::label_type(bdd::label_type)>& m,
+              replace_type m_type)
+  {
+    return internal::replace<bdd_policy>(ep, f, m, m_type);
+  }
+
+  bdd
+  bdd_replace(const bdd& f,
+              const function<bdd::label_type(bdd::label_type)>& m,
+              replace_type m_type)
+  {
+    return bdd_replace(exec_policy(), f, m, m_type);
+  }
+
+  bdd
+  bdd_replace(const exec_policy& ep,
+              const bdd& f,
+              const function<bdd::label_type(bdd::label_type)>& m)
+  {
+    return internal::replace<bdd_policy>(ep, f, m);
+  }
+
+  bdd
+  bdd_replace(const bdd& f, const function<bdd::label_type(bdd::label_type)>& m)
+  {
+    return bdd_replace(exec_policy(), f, m);
+  }
+
+  bdd
+  bdd_replace(const exec_policy& ep, __bdd&& f, const function<bdd::label_type(bdd::label_type)>& m)
+  {
+    return internal::replace<bdd_policy>(ep, std::move(f), m);
+  }
+
+  bdd
+  bdd_replace(__bdd&& f, const function<bdd::label_type(bdd::label_type)>& m)
+  {
+    return internal::replace<bdd_policy>(std::move(f), m);
+  }
+
+  bdd
+  bdd_replace(const exec_policy& ep,
+              __bdd&& f,
+              const function<bdd::label_type(bdd::label_type)>& m,
+              replace_type m_type)
+  {
+    return internal::replace<bdd_policy>(ep, std::move(f), m, m_type);
+  }
+
+  bdd
+  bdd_replace(__bdd&& f, const function<bdd::label_type(bdd::label_type)>& m, replace_type m_type)
+  {
+    return internal::replace<bdd_policy>(std::move(f), m, m_type);
+  }
+}

src/adiar/internal/algorithms/dot.h

@@ -28,18 +28,22 @@ namespace adiar::internal
   inline void
   __print_dot(const File& nodes, std::ostream& out, bool include_id)
   {
-    out << "digraph DD {" << "\n";
+    out << "digraph DD {"
+        << "\n";
 
     node_stream<> ns(nodes);
 
     if (nodes->is_terminal()) {
       const bool value = ns.pull().value();
 
       out << "\tn" << ptr_uint64(value)._raw << " [shape=box, label=<"
-          << (value ? File::true_print : File::false_print) << ">];" << "\n";
+          << (value ? File::true_print : File::false_print) << ">];"
+          << "\n";
     } else {
-      out << "\t// Nodes" << "\n";
-      out << "\tnode [shape=" << (include_id ? "box" : "circle") << "];" << "\n";
+      out << "\t// Nodes"
+          << "\n";
+      out << "\tnode [shape=" << (include_id ? "box" : "circle") << "];"
+          << "\n";
 
       while (ns.can_pull()) {
         const node n = ns.pull();
@@ -49,37 +53,49 @@ namespace adiar::internal
         out << "</SUB>>, style=rounded];\n";
       }
 
-      out << "\tnode [shape=box];" << "\n";
-      out << "\tn" << ptr_uint64(false)._raw << " [label=<" << File::false_print << ">];" << "\n";
-      out << "\tn" << ptr_uint64(true)._raw << " [label=<" << File::true_print << ">];" << "\n";
+      out << "\tnode [shape=box];"
+          << "\n";
+      out << "\tn" << ptr_uint64(false)._raw << " [label=<" << File::false_print << ">];"
+          << "\n";
+      out << "\tn" << ptr_uint64(true)._raw << " [label=<" << File::true_print << ">];"
+          << "\n";
 
-      out << std::endl << "\t// Arcs" << "\n";
+      out << std::endl
+          << "\t// Arcs"
+          << "\n";
 
       ns.reset();
       while (ns.can_pull()) {
         const node node = ns.pull();
 
-        out << "\tn" << node.uid()._raw << " -> " << "n" << node.low()._raw << " [style=dashed];"
+        out << "\tn" << node.uid()._raw << " -> "
+            << "n" << node.low()._raw << " [style=dashed];"
             << "\n";
-        out << "\tn" << node.uid()._raw << " -> " << "n" << node.high()._raw << " [style=solid];"
+        out << "\tn" << node.uid()._raw << " -> "
+            << "n" << node.high()._raw << " [style=solid];"
             << "\n";
       }
 
       out << "\n"
-          << "\t// Ranks" << "\n";
+          << "\t// Ranks"
+          << "\n";
 
       ns.reset();
-      out << "\t{ rank=same; " << "n" << ns.pull().uid()._raw << " }" << "\n";
+      out << "\t{ rank=same; "
+          << "n" << ns.pull().uid()._raw << " }"
+          << "\n";
 
       while (ns.can_pull()) {
         const node current_node = ns.pull();
 
-        out << "\t{ rank=same; " << "n" << current_node.uid()._raw << " ";
+        out << "\t{ rank=same; "
+            << "n" << current_node.uid()._raw << " ";
 
         while (ns.can_pull() && current_node.label() == ns.peek().label()) {
           out << "n" << ns.pull().uid()._raw << " ";
         }
-        out << "}" << "\n";
+        out << "}"
+            << "\n";
       }
     }
     out << "}" << std::endl;
@@ -141,8 +157,9 @@ namespace adiar::internal
     arc_stream<> as(arcs);
     while (as.can_pull_internal()) {
       const arc a = as.pull_internal();
-      out << "\t" << "n" << a.target().label() << "_" << a.target().id() << " -> " << "n"
-          << a.source().label() << "_" << a.source().id()
+      out << "\t"
+          << "n" << a.target().label() << "_" << a.target().id() << " -> "
+          << "n" << a.source().label() << "_" << a.source().id()
           << " [style=" << (a.out_idx() ? "solid" : "dashed") << ", color=blue];" << std::endl;
     }
 
@@ -153,8 +170,9 @@ namespace adiar::internal
 
     while (as.can_pull_terminal()) {
       const arc a = as.pull_terminal();
-      out << "\t" << "n" << a.source().label() << "_" << a.source().id() << " -> " << "s"
-          << a.target().value() << " [style=" << (a.out_idx() ? "solid" : "dashed")
+      out << "\t"
+          << "n" << a.source().label() << "_" << a.source().id() << " -> "
+          << "s" << a.target().value() << " [style=" << (a.out_idx() ? "solid" : "dashed")
           << ", color=red];" << std::endl;
     }
 

src/adiar/internal/algorithms/nested_sweeping.h

@@ -110,7 +110,7 @@ namespace adiar::internal
 
       // Set up priority queue for next level
       constexpr bool terminal_value = false; // <-- NOTE: Dummy value
-      __reduce_level__epilogue<>(arcs, label, pq, out_writer, terminal_value);
+      __reduce_level__epilogue<>(arcs, pq, out_writer, terminal_value);
     }
 
     ////////////////////////////////////////////////////////////////////////////////////////////////
@@ -540,6 +540,24 @@ namespace adiar::internal
           }
         }
 
+        ////////////////////////////////////////////////////////////////////////////////////////////
+        /// \brief Whether the priority queue has a current level.
+        ////////////////////////////////////////////////////////////////////////////////////////////
+        bool
+        has_current_level() const
+        {
+          return _outer_pq.has_current_level();
+        }
+
+        ////////////////////////////////////////////////////////////////////////////////////////////
+        /// \brief Obtain the current level from the priority queue.
+        ////////////////////////////////////////////////////////////////////////////////////////////
+        level_type
+        current_level() const
+        {
+          return _outer_pq.current_level();
+        }
+
         ////////////////////////////////////////////////////////////////////////////////////////////
         /// \brief Set up the next nonempty level in the priority queue and the sorter (down to the
         ///        given `stop_level`).
@@ -1617,7 +1635,7 @@ namespace adiar::internal
 #ifdef ADIAR_STATS
       nested_sweeping::stats.skips += 1u;
 #endif
-      return reduce<nesting_policy>(typename nesting_policy::__dd_type(dag, ep));
+      return reduce(ep, policy_impl, typename nesting_policy::__dd_type(dag, ep));
     }
 #ifdef ADIAR_STATS
     nested_sweeping::stats.runs += 1u;
@@ -1711,6 +1729,7 @@ namespace adiar::internal
                                                                 nested_sweeping::stats.outer_up);
         } else {
           const size_t unreduced_width = outer_level.width();
+
           if (unreduced_width <= outer_internal_sorter_can_fit) {
             __reduce_level<nesting_policy, internal_sorter>(outer_arcs,
                                                             outer_level.level(),