BDD/Generator API

docs/example/queens.md

@@ -218,21 +218,15 @@ uint64_t n_queens_list(uint64_t N, uint64_t column,
     partial_assignment.push_back(row_q);
 
     // Construct the assignment for this entire column
-    adiar::assignment_file column_assignment;
+    std::vector<adiar::pair<adiar::bdd::label_type, bool>> column_assignment;
 
-    { // The assignment_writer has to be detached, before we call any
-      // bdd functions. It is automatically detached upon destruction,
-      //  hence we have it in this little scope.
-      adiar::file_writer<map_pair<bdd::label_t, bool>> aw(column_assignment);
-
-      for (uint64_t row = 0; row < N; row++) {
-        aw << assignment(label_of_position(N, row, column),
-                                row == row_q);
-      }
+    for (uint64_t row = 0; row < N; row++) {
+      column_assignment.push_back({label_of_position(N, row, column), row == row_q});
     }
 
     adiar::bdd restricted_constraints = adiar::bdd_restrict(constraints,
-                                                            column_assignment);
+                                                            column_assignment.begin(),
+                                                            column_assignment.end());
 
     if (adiar::bdd_pathcount(restricted_constraints) == 1) {
       solutions += 1;

example/queens.cpp

@@ -248,19 +248,15 @@ uint64_t n_queens_list(uint64_t N, uint64_t column,
     partial_assignment.push_back(row_q);
 
     // Construct the assignment for this entire column
-    adiar::shared_file<adiar::map_pair<adiar::bdd::label_type, adiar::assignment>> column_assignment;
+    std::vector<adiar::pair<adiar::bdd::label_type, bool>> column_assignment;
 
-    { // The assignment_writer has to be detached, before we call any bdd
-      // functions. It is automatically detached upon destruction, hence we have
-      // it in this little scope.
-      adiar::file_writer<adiar::map_pair<adiar::bdd::label_type, adiar::assignment>> aw(column_assignment);
-
-      for (uint64_t row = 0; row < N; row++) {
-        aw << adiar::map_pair<adiar::bdd::label_type, adiar::assignment>(label_of_position(N, row, column), row == row_q);
-      }
+    for (uint64_t row = 0; row < N; row++) {
+      column_assignment.push_back({label_of_position(N, row, column), row == row_q});
     }
 
-    adiar::bdd restricted_constraints = adiar::bdd_restrict(constraints, column_assignment);
+    adiar::bdd restricted_constraints = adiar::bdd_restrict(constraints,
+                                                            column_assignment.begin(),
+                                                            column_assignment.end());
 
     if (adiar::bdd_pathcount(restricted_constraints) == 1) {
       solutions += 1;

makefile

@@ -72,9 +72,6 @@ test/adiar/domain:
 test/adiar/exec_policy:
 	make $(MAKE_FLAGS) test TEST_FOLDER=test/adiar TEST_NAME=exec_policy
 
-test/adiar/map:
-	make $(MAKE_FLAGS) test TEST_FOLDER=test/adiar TEST_NAME=map
-
 test/adiar/bdd/apply:
 	make $(MAKE_FLAGS) test TEST_FOLDER=test/adiar/bdd TEST_NAME=apply
 

src/adiar/CMakeLists.txt

@@ -6,17 +6,15 @@ set_property(GLOBAL PROPERTY USE_FOLDERS On)
 set(HEADERS
   # adiar
   adiar.h
-  assignment.h
   bool_op.h
   builder.h
   deprecated.h
   domain.h
   exception.h
   exec_policy.h
-  file.h
   functional.h
-  map.h
   statistics.h
+  types.h
 
   # adiar/bdd
   bdd.h

src/adiar/adiar.h

@@ -14,7 +14,6 @@
 #include <adiar/exception.h>
 #include <adiar/exec_policy.h>
 #include <adiar/functional.h>
-#include <adiar/file.h> // <-- TODO: Remove!
 
 ////////////////////////////////////////////////////////////////////////////////
 /// Global Domain

src/adiar/bdd.h

@@ -17,11 +17,10 @@
 #include <string>
 #include <iostream>
 
-#include <adiar/assignment.h>
 #include <adiar/bool_op.h>
 #include <adiar/exec_policy.h>
-#include <adiar/file.h> // <-- TODO: Remove
 #include <adiar/functional.h>
+#include <adiar/types.h>
 
 #include <adiar/bdd/bdd.h>
 #include <adiar/zdd/zdd.h>
@@ -33,6 +32,20 @@ namespace adiar
   ///
   /// \{
 
+  /// \cond
+  //////////////////////////////////////////////////////////////////////////////
+  /// \brief End marker for the BDD assignment generators.
+  //////////////////////////////////////////////////////////////////////////////
+  template<>
+  struct generator_end<pair<bdd::label_type, bool>>
+  {
+    using value_type = pair<bdd::label_type, bool>;
+
+    static constexpr value_type value =
+      make_pair(static_cast<bdd::label_type>(-1), false);
+  };
+  /// \endcond
+
   //////////////////////////////////////////////////////////////////////////////
   /// \name Basic BDD Constructors
   ///
@@ -459,28 +472,55 @@ namespace adiar
   //////////////////////////////////////////////////////////////////////////////
   /// \brief    Restrict a subset of variables to constant values.
   ///
-  /// \details  For each tuple (i,v) in the assignment `xs` the variable
+  /// \details  For each tuple (i,v) in the assignment `xs`, the variable
   ///           with label i is set to the constant value v. This binds the
   ///           scope of the variables in `xs`, i.e. any later mention of
   ///           a variable i is not the same as variable i in `xs`.
   ///
-  /// \param f  BDD to restrict
+  /// \param f  BDD to restrict.
   ///
-  /// \param xs Assignments (i,v) to variables in (in ascending order)
+  /// \param xs Assignments (i,v) to variables in (in ascending order).
   ///
   /// \returns  \f$ f|_{(i,v) \in xs : x_i = v} \f$
   //////////////////////////////////////////////////////////////////////////////
-  // TODO v2.0 : Replace with `generator<pair<...>>`.
   __bdd bdd_restrict(const bdd &f,
-                     const shared_file<map_pair<bdd::label_type, assignment>> &xs);
+                     const generator<pair<bdd::label_type, bool>> &xs);
 
   //////////////////////////////////////////////////////////////////////////////
   /// \brief Restrict a subset of variables to constant values.
   //////////////////////////////////////////////////////////////////////////////
-  // TODO v2.0 : Replace with `generator<pair<...>>`.
   __bdd bdd_restrict(const exec_policy &ep,
                      const bdd &f,
-                     const shared_file<map_pair<bdd::label_type, assignment>> &xs);
+                     const generator<pair<bdd::label_type, bool>> &xs);
+
+  //////////////////////////////////////////////////////////////////////////////
+  /// \brief       Restrict a subset of variables to constant values.
+  ///
+  /// \details     For each tuple (i,v) provided by the iterator, the variable
+  ///              with label i is set to the constant value v.
+  ///
+  /// \param f     BDD to restrict
+  ///
+  /// \param begin Single-pass forward iterator that provides the to-be
+  ///              restricted variables in \em ascending order.
+  ///
+  /// \param end   Marks the end for `begin`.
+  ///
+  /// \returns  \f$ f|_{(i,v) \in xs : x_i = v} \f$
+  //////////////////////////////////////////////////////////////////////////////
+  template<typename ForwardIt>
+  __bdd bdd_restrict(const bdd& f, ForwardIt begin, ForwardIt end)
+  { return bdd_restrict(f, make_generator(begin, end)); }
+
+  //////////////////////////////////////////////////////////////////////////////
+  /// \brief Restrict a subset of variables to constant values.
+  //////////////////////////////////////////////////////////////////////////////
+  template<typename ForwardIt>
+  __bdd bdd_restrict(const exec_policy &ep,
+                     const bdd& f,
+                     ForwardIt begin,
+                     ForwardIt end)
+  { return bdd_restrict(ep, f, make_generator(begin, end)); }
 
   //////////////////////////////////////////////////////////////////////////////
   /// \brief     Existential quantification of a single variable.
@@ -1016,9 +1056,9 @@ namespace adiar
   //////////////////////////////////////////////////////////////////////////////
   /// \brief    Evaluate a BDD according to an assignment to its variables.
   ///
-  /// \param f  The BDD to evaluate
+  /// \param f  The BDD to evaluate.
   ///
-  /// \param xs A list of tuples `(i,v)` in ascending order of `i`.
+  /// \param xs Assignments (i,v) to variables in (in ascending order).
   ///
   /// \pre      Assignment tuples in `xs` is in ascending order
   ///
@@ -1027,9 +1067,26 @@ namespace adiar
   ///
   /// \throws invalid_argument If a level in the BDD does not exist in `xs`.
   //////////////////////////////////////////////////////////////////////////////
-  // TODO v2.0 : Replace with `generator<pair<...>>`
-  bool bdd_eval(const bdd &f,
-                const shared_file<map_pair<bdd::label_type, boolean>> &xs);
+  bool bdd_eval(const bdd &f, const generator<pair<bdd::label_type, bool>> &xs);
+
+  //////////////////////////////////////////////////////////////////////////////
+  /// \brief       Evaluate a BDD according to an assignment to its variables.
+  ///
+  /// \param f     The BDD to evaluate.
+  ///
+  /// \param begin Single-pass forward iterator that provides the assignment in
+  ///              \em ascending order.
+  ///
+  /// \param end   Marks the end for `begin`.
+  ///
+  /// \throws out_of_range If traversal of the BDD leads to going beyond the end
+  ///                      of the content of `xs`.
+  ///
+  /// \throws invalid_argument If a level in the BDD does not exist in `xs`.
+  //////////////////////////////////////////////////////////////////////////////
+  template<typename ForwardIt>
+  bool bdd_eval(const bdd &f, ForwardIt begin, ForwardIt end)
+  { return bdd_eval(f, make_generator(begin, end)); }
 
   //////////////////////////////////////////////////////////////////////////////
   /// \brief Get the labels of the levels of the BDD.

src/adiar/bdd/bdd.cpp

@@ -186,7 +186,7 @@ namespace adiar
 
   __bdd bdd_from(const exec_policy &ep, const zdd &A)
   {
-    const shared_file<bdd::label_type> dom = domain_get();
+    const internal::shared_file<bdd::label_type> dom = domain_get();
     internal::file_stream<domain_var> ds(dom);
 
     return bdd_from(ep, A, make_generator(ds));

src/adiar/bdd/count.cpp

@@ -114,9 +114,7 @@ namespace adiar
 
   uint64_t bdd_satcount(const exec_policy &ep, const bdd &f)
   {
-    const bdd::label_type domain_size = domain_isset() ? domain_get()->size() : 0;
-    const bdd::label_type varcount = bdd_varcount(f);
-    return bdd_satcount(ep, f, std::max(domain_size, varcount));
+    return bdd_satcount(ep, f, std::max<bdd::label_type>(domain_size(), bdd_varcount(f)));
   };
 
   uint64_t bdd_satcount(const bdd &f)