Add `bdd_compose` - Githubissues

The Composition of two BDDs f and g for some label i ∊ [n] is f _{i = g} is to be interpreted as f(x₁, ..., x_i-1, g(x₁, ..., x_n), x_i+1, ..., x_n), i.e. g dictates the value of the ith input variable. This function is used in some model checking algorithms.

Based on BuDDy, the declarations in adiar/bdd.h should be

  //////////////////////////////////////////////////////////////////////////////
  /// \brief Functional composition.
  ///
  /// \param f   Outer function
  ///
  /// \param g   Inner function
  ///
  /// \param var The variable that \c g replaces in the input of \c f
  /// 
  /// \returns \f$ f|_{x_{\mathit{var}} = g} \f$
  //////////////////////////////////////////////////////////////////////////////
  __bdd bdd_compose(const bdd &f, const bdd &g, label_t var);

  inline __bdd bdd_compose(const bdd &f, const bdd &g, const bdd &var)
  { bdd_compose(f, g, min_label(v)); }

Implementation

This can be implemented with a single sweep through f and g by reusing the ideas in the Quantification and the If-Then-Else algorithms. A priority queue contains requests on triples t1, t2, t3 where t2 and t3 are nodes from f and t1 is from g. Here, similar to If-Then-Else, t2 represents the true (high) branch on variable i and t3 the false branch (low).

For level i we deal with it somewhat similar to Quantify where a single node of f is turned into two. To this end, we need to introduce the same idea as we did for the product construction etc. with the std::variant<skipto, output> and the policy::may_skip optimisation, where we use skipto if g is not on level i.

The pruning of the If-Then-Else still apply. Ideas from Quantification also somewhat applies here.

If any branches of f become NIL (due to a sink in g), then we should not differentiate between (..., t, NIL) and (..., NIL, t). As a convention, just always have the NIL in the last of the two.
If both branches are for the same node in f then set both the g and the second f node to NIL.
Unlike in Quantification we cannot sort f's targets! This is due to us having to remember which one belongs to the true and which one to the false branch.

All of this should be possible to do with the policy pattern on the algorithm in the adiar/bdd/if_then_else.cpp.

Move the main logic in adiar/bdd/if_then_else.cpp to a templated function in adiar/internal/prod3.h and turn bdd_ite into a call to prod3. The following things should stay in bdd_ite
- Collapse to the Apply operation.
- Zipping of disjunct levels case.

When this is done, then slowly add enough hooks in the policy of prod3 to vary the behaviour between the two algorithms.

SSoelvsten / adiar

Add `bdd_compose` #148