Add 'relnext(states, relation, varcount)' and 'relprev(states, relati…

…on, varcount)' overloads

While maybe not as good in practice as the interleaved ordering, it is used in quite a
few academic texts (see the referenced unit tests and also the paper on Knor by Tom
van Dijk)

src/adiar/bdd.h

@@ -1456,6 +1456,31 @@ namespace adiar
               const function<optional<bdd::label_type>(bdd::label_type)>& m,
               replace_type m_type);
 
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Forwards step with the Relational Product for *disjoint* variable orderings,
+  ///        including relabelling.
+  ///
+  /// \param states
+  ///    A symbolic representation of the *current* set of states. These are all encoded with the
+  ///    variables `0`, `1`, ... `varcount - 1`.
+  ///
+  /// \param relation
+  ///    A relation between *current* and *next* state variables. The *next* state is encoded with
+  ///    variables `varcount`, `varcount+1`, ... `2*varcount - 1`.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_relnext(const bdd& states, const bdd& relation, const bdd::label_type varcount);
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Forwards step with the Relational Product for *disjoint* variable orderings,
+  ///        including relabelling.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_relnext(const exec_policy& ep,
+              const bdd& states,
+              const bdd& relation,
+              const bdd::label_type varcount);
+
   //////////////////////////////////////////////////////////////////////////////////////////////////
   /// \brief Forwards step with the Relational Product for *interleaved* variable orderings,
   ///        including relabelling.
@@ -1538,6 +1563,31 @@ namespace adiar
               const function<optional<bdd::label_type>(bdd::label_type)>& m,
               replace_type m_type);
 
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Backwards step with the Relational Product for *disjoint* variable orderings,
+  ///        including relabelling.
+  ///
+  /// \param states
+  ///    A symbolic representation of the *current* set of states. These are all encoded with the
+  ///    variables `0`, `1`, ... `varcount - 1`.
+  ///
+  /// \param relation
+  ///    A relation between *current* and *next* state variables. The *next* state is encoded with
+  ///    variables `varcount`, `varcount+1`, ... `2*varcount - 1`.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_relprev(const bdd& states, const bdd& relation, const bdd::label_type varcount);
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// \brief Backwards step with the Relational Product for *disjoint* variable orderings,
+  ///        including relabelling.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  bdd
+  bdd_relprev(const exec_policy& ep,
+              const bdd& states,
+              const bdd& relation,
+              const bdd::label_type varcount);
+
   //////////////////////////////////////////////////////////////////////////////////////////////////
   /// \brief Backwards step with the Relational Product for *interleaved* variable orderings,
   ///        including relabelling.

src/adiar/bdd/relprod.cpp

@@ -349,6 +349,24 @@ namespace adiar
     return bdd_relnext(exec_policy(), states, relation, m);
   }
 
+  bdd
+  bdd_relnext(const exec_policy& ep,
+              const bdd& states,
+              const bdd& relation,
+              const bdd::label_type varcount)
+  {
+    const auto map = [=](const bdd::label_type x) -> adiar::optional<int> {
+      return x < varcount ? adiar::make_optional<int>() : adiar::make_optional<int>(x - varcount);
+    };
+    return bdd_relnext(ep, states, relation, map, replace_type::Shift);
+  }
+
+  bdd
+  bdd_relnext(const bdd& states, const bdd& relation, const bdd::label_type varcount)
+  {
+    return bdd_relnext(exec_policy(), states, relation, varcount);
+  }
+
   bdd
   bdd_relnext(const exec_policy& ep, const bdd& states, const bdd& relation)
   {
@@ -415,6 +433,24 @@ namespace adiar
     return bdd_relprev(exec_policy(), states, relation, m);
   }
 
+  bdd
+  bdd_relprev(const exec_policy& ep,
+              const bdd& states,
+              const bdd& relation,
+              const bdd::label_type varcount)
+  {
+    const auto map = [=](const bdd::label_type x) -> adiar::optional<int> {
+      return varcount <= x ? adiar::make_optional<int>() : adiar::make_optional<int>(x + varcount);
+    };
+    return bdd_relprev(ep, states, relation, map, replace_type::Shift);
+  }
+
+  bdd
+  bdd_relprev(const bdd& states, const bdd& relation, const bdd::label_type varcount)
+  {
+    return bdd_relprev(exec_policy(), states, relation, varcount);
+  }
+
   bdd
   bdd_relprev(const exec_policy& ep, const bdd& states, const bdd& relation)
   {