Add bdd_relprod

[SSoelvsten]

For model checking, we want the bdd_relprod operatios 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 the exists and replace are provided with a single function<optional<label_type>(label_type)>.

• Add bdd_relprod with the following signature

  bdd
  bdd_relprod(const bdd& states, 
              const bdd& rel, 
              const predicate<bdd::label_type>>& pred);

• Add bdd_relnext with the following signature

  bdd
  bdd_relnext(const bdd& states,
              const bdd& rel,
              const function<optional<bdd::label_type>(bdd::label_type)>& m
              replace_type m_type);

• Add bdd_relprev with the following signature

  bdd
  bdd_relprev(const bdd& states,
              const bdd& rel,
              const function<optional<bdd::label_type>(bdd::label_type)>& m
              replace_type m_type);

To do so, use the Apply from v1.0 ( #35 etc. ), the Multi-variable Quantification of v2.0 ( #499 etc ), and Relabelling of v2.1 ( #498 ).

Optimisations

• Use transposed result of bdd_and directly inside of bdd_exists
• Add pruning optimisation to the initial transposition with bdd_and: prune a node if it has a true child and will be quantified later.
• bdd_relnext: Include the relabelling directly inside the nested quantification sweep, if it is monotonic.
• bdd_relprev: Support the replace_type::shift ( Add bdd_replace for monotonic renamings #498 ).
• If it is not monotonic, then throw an exception until Extend dd_replace with non-monotonic renamings #500 is done.