Generalize `bdd_compose` to compose multiple variables at once

[SSoelvsten]

In #148 we intend to add the bdd_compose(bdd f, bdd g, label_t var) single-variable compose function. This can be generalised to a multi-variable bdd_compose(bdd f, map<label_t, bdd> m) with the nested sweeping of v2.0.

Here is C++ pseudocode for the recursive version of this function based on the code in Sylvan. One may want to understand the Sylvan version in more detail, to find some more ideas for optimisations. Notice, they use a BDDMAP which is an MTBDD ( #438 ) whos leaves are other decision diagrams - yet, they still only use it as a simple map from labels to bdds.

//////////////////////////////////////////////////////////////////////////////
/// \brief Multi-functional composition.
///
/// \param f Outer function
///
/// \param m Map of *inner* functions intended to replace some variables
///          \f$ x_i \f$ in `f`.
///
/// \returns \f$ f|_{x_{\mathit{var}} = g} \f$ for each \f$ g \in m \f$.
//////////////////////////////////////////////////////////////////////////////
bdd bdd_compose(bdd f, map<label_t, bdd> m)
{
  /* Trivial Case */
  if (f == true || f == false) return f;

  /* Recursive Call */
  bdd low = bdd_compose(f.low, m);
  bdd high = bdd_compose(f.high, m);

  /* Call 'bdd_ite(...)' if this level is to be composed */
  return (m.contains(f.level))
    ? bdd_ite(m.get(f.level), high, low)
    : { f.level, low, high };
}

In general, we can do this by extending the nested sweeping framework as follows

• Transpose f and do an outer reduce
• Do a nested sweep back down for each m.contains(f.level) with the algorithm from #148 . To this end, we might want to let the inner_down_sweep policy be stateful, such that it can hold the map m and hide away the second BDD from the nested sweeping framework.