Overload 'bdd_satmin' and 'bdd_satmax' with symbolic set of variables

Author: SSoelvsten

src/adiar/bdd.h

@@ -1381,6 +1381,23 @@ namespace adiar
     return bdd_satmin(f, make_generator(cbegin, cend), std::distance(cbegin, cend));
   }
 
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief The lexicographically smallest x such that f(x) is true.
+  ///
+  /// \param f
+  ///    BDD of interest.
+  ///
+  /// \param d
+  ///    BDD cube of variables that ought to be included.
+  ///
+  /// \returns A bdd whos only path to the `true` terminal reflects the minimal assignment.
+  ///
+  /// \throws domain_error
+  ///    If `bdd_iscube(d)` is not satisfied.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_satmin(const bdd& f, const bdd& d);
+
   //////////////////////////////////////////////////////////////////////////////////////////////////
   /// \brief The lexicographically smallest x such that f(x) is true.
   ///
@@ -1466,6 +1483,23 @@ namespace adiar
     return bdd_satmax(f, make_generator(cbegin, cend), std::distance(cbegin, cend));
   }
 
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief The lexicographically largest x such that f(x) is true.
+  ///
+  /// \param f
+  ///    BDD of interest.
+  ///
+  /// \param d
+  ///    BDD cube of variables that ought to be included.
+  ///
+  /// \returns A bdd whos only path to the `true` terminal reflects the minimal assignment.
+  ///
+  /// \throws domain_error
+  ///    If `bdd_iscube(d)` is not satisfied.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_satmax(const bdd& f, const bdd& d);
+
   //////////////////////////////////////////////////////////////////////////////////////////////////
   /// \brief   The lexicographically largest x such that f(x) is true.
   ///

src/adiar/bdd/evaluate.cpp

@@ -297,6 +297,19 @@ namespace adiar
     return __bdd_satX<internal::traverse_satmin_visitor>(f, d, total_levels);
   }
 
+  bdd
+  bdd_satmin(const bdd& f, const bdd& d)
+  {
+    if (!bdd_iscube(d)) { throw domain_error("BDD 'd' is not a cube"); }
+
+    typename internal::level_stream_t<bdd>::template stream_t<> d_levels(d);
+    const generator<bdd::label_type> d_gen = make_generator__levels(d_levels);
+
+    const size_t total_levels = std::min<size_t>(f->levels() + d->levels(), bdd::max_label+1);
+
+    return __bdd_satX<internal::traverse_satmin_visitor>(f, d_gen, total_levels);
+  }
+
   void
   bdd_satmin(const bdd& f, const consumer<pair<bdd::label_type, bool>>& c)
   {
@@ -316,6 +329,19 @@ namespace adiar
     return __bdd_satX<internal::traverse_satmax_visitor>(f, d, total_levels);
   }
 
+  bdd
+  bdd_satmax(const bdd& f, const bdd& d)
+  {
+    if (!bdd_iscube(d)) { throw domain_error("BDD 'd' is not a cube"); }
+
+    typename internal::level_stream_t<bdd>::template stream_t<> d_levels(d);
+    const generator<bdd::label_type> d_gen = make_generator__levels(d_levels);
+
+    const size_t total_levels = std::min<size_t>(f->levels() + d->levels(), bdd::max_label+1);
+
+    return __bdd_satX<internal::traverse_satmax_visitor>(f, d_gen, total_levels);
+  }
+
   void
   bdd_satmax(const bdd& f, const consumer<pair<bdd::label_type, bool>>& c)
   {

src/adiar/internal/util.h

@@ -40,24 +40,42 @@ namespace adiar::internal
   template <typename File>
   struct level_stream_t
   {
-    template <bool reverse = false>
-    using stream_t = level_info_stream<reverse>;
+    template <bool Reverse = false>
+    using stream_t = level_info_stream<Reverse>;
   };
 
   template <>
   struct level_stream_t<file<ptr_uint64::label_type>>
   {
-    template <bool reverse = false>
-    using stream_t = file_stream<ptr_uint64::label_type, reverse>;
+    template <bool Reverse = false>
+    using stream_t = file_stream<ptr_uint64::label_type, Reverse>;
   };
 
   template <>
   struct level_stream_t<shared_file<ptr_uint64::label_type>>
   {
-    template <bool reverse = false>
-    using stream_t = file_stream<ptr_uint64::label_type, reverse>;
+    template <bool Reverse = false>
+    using stream_t = file_stream<ptr_uint64::label_type, Reverse>;
   };
 
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief  Turn a `level_stream<...>` into a level-only generator function.
+  ///
+  /// \remark The direction (*ascending* vs. *descending*) of the generator is dictated by the given
+  ///         stream's direction.
+  ///
+  /// \see level_stream_t, generator
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  template <typename LevelStream>
+  generator<ptr_uint64::label_type>
+  make_generator__levels(LevelStream& ls)
+  {
+    return [&ls]() mutable -> optional<ptr_uint64::label_type> {
+      if (!ls.can_pull()) { return {}; }
+      return level_of(ls.pull());
+    };
+  }
+
   //////////////////////////////////////////////////////////////////////////////////////////////////
   /// \brief Obtain whether the levels in two files are disjoint.
   //////////////////////////////////////////////////////////////////////////////////////////////////