RelProd : Frame Rule for Interleaved Ordering

[SSoelvsten]

As a follow-up on #502 and the overloads in #682 , we should consider to make the creation of transitions even easier.

Add Frame-Rules to Relations

• Given a relation, look at its support and generate the missing frame rule. Either provide the frame rule itself or and it onto the relation.

RelProd with Built-in Frame Rule

• Preface bdd_relnext(states, relation) and bdd_relprev(states, relation) with the addition of the frame rule.

• As in Sylvan, this can be further improved by applying the frame rule on-the-fly during the product construction between states and relation: for every pair, x x', if only one or none of them is mentioned then add the missing nodes during the top-down sweep.

  To do so, one may need a third argument with the support cube (type: generator<int>, ForwardIt, or bdd in ascending order); variables not in support are kept as-is.

  For such a case, we probably need some new tests that exposes the use (and/or lack thereof) of the on-the-fly frame rule.