Add `zdd_cross`

[SSoelvsten]

The following is the pseudocode for Knuth's Cross operation is based from the paper ZDD Boolean Synthesis by Yi Lin, Lucas M. Tabajara, and Moshe Y. Vardi.

zdd_cross(Z):
  if Z == Ø:  return {Ø}
  if Z == {Ø}: return Ø

  Z_r  = zdd_union(Z.low, Z.high)
  Z_rr = zdd_cross(Z.low)
  Z_ll = zdd_cross(Z_r)
  Z_hh = zdd_diff(Z_rr, Z_ll)

  return (Z.var, Z_ll, Z_hh)

This requires the multi-recursion framework to be implemented and heavily generalised.

Additional context This was one of the key operations to convert they used in their ZDD-based synthesis tool to convert between DNF and CNF.