Extend `dd_replace` with non-monotonic renamings

[SSoelvsten]

In #498 we added the dd_replace(dd, var_map) algorithm, but only with support for monotonic variable replacement. That is, up to this point, we only support variable replacements that do not change the order of the levels within the decision diagram.

• [ ] Implement the dd_bubble(dd, i, j) algorithm to move level i down to an empty level j (assuming i < j). We would want to have it as its own internal algorithm such that we can test it in isolation. We probably can do it by generalising the quantify algorithm into a prod2_unary (#614).
• [ ] Replace the non-monotonic exception in dd_replace<dd_policy>(dd, var_map) with the Nested Sweeping Framework ( #499 ) with (1) a simple initial transposition, (2) dd_bubble as the nested sweep, and (3) making the reduce_level able to output nodes with another label.