Add `bdd_relnext` and `bdd_relprev`

[SSoelvsten]

For model checking, we want the bdd_relnext/bdd_relprev operations to apply a transition relation to a set of states.

Basic Non-trivial Implementation

The most basic version is by using all of our pieces to compute (∃ x : S(x) ∧T(x,x') )[x'/x] , where x and x' is a vector of n variables.

• [ ] To implement the relational product, combine the Apply from v1.0 ( #35 etc. ), the Multi-variable Quantification of v2.0 ( #499 etc ), and Relabelling of v2.1 ( #498 ).
  • [ ] Add pruning optimisation to the initial transposition with Apply.
  • [ ] Include the relabelling directly inside the nested quantification sweep, if it is monotonic. If it is not monotonic, then throw an exception until #500 is done.

Interleaved Orderings : Frame Rule

Looking at the support of T, we know whether the frame rule can apply to a node. In that case, the level can immediately be output as x' rather than x.