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.

Tasks

• Implement the dd_replace with a Jump_Down reordering. This moves levels down to an empty level below the one that immediately follows.
• Implement the dd_replace with the Non_Monotone reordering. Replace the non-monotonic exception in dd_replace<dd_policy>(dd, var_map) with the Nested Sweeping Framework ( Implement Nested Sweeping Framework (for quantify) #499 ) with (1) a simple initial transposition, (2) the Jump_Down (sub)routine, and (3) making reduce_level able to output nodes with another label.

See [Sølvsten25] for more details.

References

• [Sølvsten25] S. Sølvsten “I/O-efficient Symbolic Model Checking”. Aarhus University (2025)