Add 'bdd_relprod', 'bdd_relnext', and 'bdd_relprev'

This merely covers the API but none of the planned optimisations.

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/relprod:
+	$(MAKE) $(MAKE_FLAGS) test TEST_FOLDER=test/adiar/bdd TEST_NAME=relprod
+
 test/adiar/bdd/replace:
 	$(MAKE) $(MAKE_FLAGS) test TEST_FOLDER=test/adiar/bdd TEST_NAME=replace
 

src/adiar/CMakeLists.txt

@@ -118,6 +118,7 @@ set(SOURCES
   bdd/optmin.cpp
   bdd/pred.cpp
   bdd/quantify.cpp
+  bdd/relprod.cpp
   bdd/replace.cpp
   bdd/restrict.cpp
 

src/adiar/bdd.h

@@ -1131,6 +1131,150 @@ namespace adiar
 
   /// \endcond
 
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Relational Product of *states* and a *relation*.
+  ///
+  /// \param states
+  ///    A symbolic representation of the *current* (or *next*) set of states.
+  ///
+  /// \param relation
+  ///    A relation between *current* and *next* states.
+  ///
+  /// \param m
+  ///    Predicate whether a variable should be existentially quantified.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_relprod(const bdd& states, const bdd& relation, const predicate<bdd::label_type>& pred);
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Relational Product of *states* and a *relation*.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_relprod(const exec_policy& ep,
+              const bdd& states,
+              const bdd& relation,
+              const predicate<bdd::label_type>& pred);
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Forwards step with the Relational Product, including relabelling.
+  ///
+  /// \param states
+  ///    A symbolic representation of the *current* set of states.
+  ///
+  /// \param relation
+  ///    A relation between *current* and *next* states.
+  ///
+  /// \param m
+  ///    A (partial) variable relabelling from *next* to *current*. Variables for which `m` returns
+  ///    an empty value are existentially quantified, i.e. the previously *current* state variables.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_relnext(const bdd& states,
+              const bdd& relation,
+              const function<optional<bdd::label_type>(bdd::label_type)>& m);
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Forwards step with the Relational Product, including relabelling.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_relnext(const exec_policy& ep,
+              const bdd& states,
+              const bdd& relation,
+              const function<optional<bdd::label_type>(bdd::label_type)>& m);
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Forwards step with the Relational Product, including relabelling.
+  ///
+  /// \param states
+  ///    A symbolic representation of the *current* set of states.
+  ///
+  /// \param relation
+  ///    A relation between *current* and *next* states.
+  ///
+  /// \param m
+  ///    A (partial) variable relabelling from *next* to *current*. Variables for which `m` returns
+  ///    an empty value are existentially quantified, i.e. the previously *current* state variables.
+  ///
+  /// \param m_type
+  ///    Guarantees on the class of variable relabelling, e.g. whether it is monotonic.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_relnext(const bdd& states,
+              const bdd& relation,
+              const function<optional<bdd::label_type>(bdd::label_type)>& m,
+              replace_type m_type);
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Forwards step with the Relational Product, including relabelling.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_relnext(const exec_policy& ep,
+              const bdd& states,
+              const bdd& relation,
+              const function<optional<bdd::label_type>(bdd::label_type)>& m,
+              replace_type m_type);
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Backwards step with the Relational Product, including relabelling.
+  ///
+  /// \param states
+  ///    A symbolic representation of the *current* set of states.
+  ///
+  /// \param relation
+  ///    A relation between *current* and *next* states.
+  ///
+  /// \param m
+  ///    A (partial) variable relabelling from *current* to *next*. Variables for which `m` returns
+  ///    an empty value are existentially quantified, i.e. the *next* state variables (the
+  ///    previously *current* state variables).
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_relprev(const bdd& states,
+              const bdd& relation,
+              const function<optional<bdd::label_type>(bdd::label_type)>& m);
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Forwards step with the Relational Product, including relabelling.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_relprev(const exec_policy& ep,
+              const bdd& states,
+              const bdd& relation,
+              const function<optional<bdd::label_type>(bdd::label_type)>& m);
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Backwards step with the Relational Product, including relabelling.
+  ///
+  /// \param states
+  ///    A symbolic representation of the *current* set of states.
+  ///
+  /// \param relation
+  ///    A relation between *current* and *next* states.
+  ///
+  /// \param m
+  ///    A (partial) variable relabelling from *current* to *next*. Variables for which `m` returns
+  ///    an empty value are existentially quantified, i.e. the *next* state variables (the
+  ///    previously *current* state variables).
+  ///
+  /// \param m_type
+  ///    Guarantees on the class of variable relabelling, e.g. whether it is monotonic.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_relprev(const bdd& states,
+              const bdd& relation,
+              const function<optional<bdd::label_type>(bdd::label_type)>& m,
+              replace_type m_type);
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Forwards step with the Relational Product, including relabelling.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_relprev(const exec_policy& ep,
+              const bdd& states,
+              const bdd& relation,
+              const function<optional<bdd::label_type>(bdd::label_type)>& m,
+              replace_type m_type);
+
   /// \}
   //////////////////////////////////////////////////////////////////////////////////////////////////
 

src/adiar/bdd/relprod.cpp

@@ -0,0 +1,122 @@
+#include <adiar/bdd.h>
+#include <adiar/bdd/bdd_policy.h>
+#include <adiar/types.h>
+
+#include <adiar/internal/algorithms/replace.h>
+
+namespace adiar
+{
+  bdd
+  bdd_relprod(const exec_policy& ep,
+              const bdd& states,
+              const bdd& relation,
+              const predicate<bdd::label_type>& pred)
+  {
+    return bdd_exists(ep, bdd_and(ep, states, relation), pred);
+  }
+
+  bdd
+  bdd_relprod(const bdd& states, const bdd& relation, const predicate<bdd::label_type>& m)
+  {
+    return bdd_relprod(exec_policy(), states, relation, m);
+  }
+
+  bdd
+  bdd_relnext(const exec_policy& ep,
+              const bdd& states,
+              const bdd& relation,
+              const function<optional<bdd::label_type>(bdd::label_type)>& m,
+              replace_type m_type)
+  {
+    const bdd tmp_1 = bdd_and(ep, states, relation);
+
+    const bdd tmp_2 =
+      bdd_exists(ep, std::move(tmp_1), [&m](bdd::label_type x) { return !m(x).has_value(); });
+
+    const bdd tmp_3 =
+      bdd_replace(ep, std::move(tmp_2), [&m](bdd::label_type x) { return m(x).value(); }, m_type);
+
+    return tmp_3;
+  }
+
+  bdd
+  bdd_relnext(const bdd& states,
+              const bdd& relation,
+              const function<optional<bdd::label_type>(bdd::label_type)>& m,
+              replace_type m_type)
+  {
+    return bdd_relnext(exec_policy(), states, relation, m, m_type);
+  }
+
+  bdd
+  bdd_relnext(const exec_policy& ep,
+              const bdd& states,
+              const bdd& relation,
+              const function<optional<bdd::label_type>(bdd::label_type)>& m)
+  {
+    replace_type m_type;
+    {
+      internal::level_info_stream<false> ls(relation);
+      m_type = internal::__replace__infer_type<bdd_policy>(ls, m);
+    }
+    return bdd_relnext(ep, states, relation, m, m_type);
+  }
+
+  bdd
+  bdd_relnext(const bdd& states,
+              const bdd& relation,
+              const function<optional<bdd::label_type>(bdd::label_type)>& m)
+  {
+    return bdd_relnext(exec_policy(), states, relation, m);
+  }
+
+  bdd
+  bdd_relprev(const exec_policy& ep,
+              const bdd& states,
+              const bdd& relation,
+              const function<optional<bdd::label_type>(bdd::label_type)>& m,
+              replace_type m_type)
+  {
+    const bdd tmp_1 =
+      bdd_replace(ep, states, [&m](bdd::label_type x) { return m(x).value(); }, m_type);
+
+    const bdd tmp_2 = bdd_and(ep, std::move(tmp_1), relation);
+
+    const bdd tmp_3 =
+      bdd_exists(ep, std::move(tmp_2), [&m](bdd::label_type x) { return !m(x).has_value(); });
+
+    return tmp_3;
+  }
+
+  bdd
+  bdd_relprev(const bdd& states,
+              const bdd& relation,
+              const function<optional<bdd::label_type>(bdd::label_type)>& m,
+              replace_type m_type)
+  {
+    return bdd_relprev(exec_policy(), states, relation, m, m_type);
+  }
+
+  bdd
+  bdd_relprev(const exec_policy& ep,
+              const bdd& states,
+              const bdd& relation,
+              const function<optional<bdd::label_type>(bdd::label_type)>& m)
+  {
+    replace_type m_type;
+    {
+      internal::level_info_stream<false> ls(states);
+      m_type = internal::__replace__infer_type<bdd_policy>(ls, m);
+    }
+
+    return bdd_relprev(ep, states, relation, m, m_type);
+  }
+
+  bdd
+  bdd_relprev(const bdd& states,
+              const bdd& relation,
+              const function<optional<bdd::label_type>(bdd::label_type)>& m)
+  {
+    return bdd_relprev(exec_policy(), states, relation, m);
+  }
+}

src/adiar/internal/algorithms/replace.h

@@ -5,6 +5,7 @@
 
 #include <adiar/exception.h>
 #include <adiar/functional.h>
+#include <adiar/type_traits.h>
 #include <adiar/types.h>
 
 #include <adiar/internal/algorithms/reduce.h>
@@ -55,26 +56,40 @@ namespace adiar::internal
   ///
   /// \param ls A stream of `level_info` structs in *descending* order.
   //////////////////////////////////////////////////////////////////////////////////////////////////
-  template <typename Policy, typename LevelInfoStream>
+  template <typename Policy, typename LevelInfoStream, typename ReplaceFunction>
   replace_type
-  __replace__infer_type(LevelInfoStream& ls, const replace_func<Policy>& m)
+  __replace__infer_type(LevelInfoStream& ls, const ReplaceFunction& m)
   {
-    using signed_label = typename std::make_signed<typename Policy::label_type>::type;
+    using label_type  = typename Policy::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 monotone = true;
 
-    signed_label prev_before = -1;
-    signed_label prev_after  = -1;
+    label_type prev_before = Policy::max_label + 1;
+    label_type prev_after  = Policy::max_label + 1;
     while (ls.can_pull()) {
-      const signed_label next_before = ls.pull().level();
-      const signed_label next_after  = m(next_before);
+      const label_type next_before = ls.pull().level();
+      const result_type next_after = m(next_before);
+
+      if constexpr (is_partial_map) {
+        if (!next_after.has_value()) { continue; }
+      }
 
       identity &= next_before == next_after;
-      monotone &= prev_before < 0 || prev_after < next_after;
+      monotone &= Policy::max_label < prev_before || prev_after < next_after;
 
       prev_before = next_before;
-      prev_after  = next_after;
+      if constexpr (is_partial_map) {
+        prev_after = *next_after;
+      } else {
+        prev_after = next_after;
+      }
     }
 
     if (identity) { return replace_type::Identity; }

test/adiar/bdd/CMakeLists.txt

@@ -8,6 +8,7 @@ add_test(adiar-bdd-optmin       test_optmin.cpp)
 add_test(adiar-bdd-pred         test_pred.cpp)
 add_test(adiar-bdd-negate       test_negate.cpp)
 add_test(adiar-bdd-quantify     test_quantify.cpp)
+add_test(adiar-bdd-relprod      test_relprod.cpp)
 add_test(adiar-bdd-replace      test_replace.cpp)
 add_test(adiar-bdd-restrict     test_restrict.cpp)