RelProd : Overloads for Quality of Life

[SSoelvsten]

With #502 , we added the basic API of bdd_relprod, bdd_relnext, and bdd_relprev.

Variable Order: Separated (easy)

Often the variable ordering starts with all current states and then includes all next states, e.g. x y x' y'. In this case, we may just provide the number of current/next variables.

• bdd_relnext(states, relation, varcount)
• bdd_relprev(states, relation, varcount)

The relnext(...) and relprev(...) just call the other functions with the correct m and m_type.

The kalin unit tests can be copied into a new group for this overload.

Variable Order: Interleaved (easy)

Even better is to interleave the current and next state variables, e.g. x x' y y'. In this case, we may just provide nothing as an argument.

• bdd_relnext(states, relation)
• bdd_relprev(states, relation)

The relnext(...) and relprev(...) just call the other functions with the correct m and m_type.

The huth unit tests can be copied into a new group for this overload.