Add zdd_join, zdd_joinnext, and zdd_joinprev

[SSoelvsten]

With v2.1 ( #502 ), we have added the Relational Product for BDDs. We should do the same for ZDDs to support symbolic model checking with sparse bit vectors.

• Add zdd_replace similar to bdd_replace.
• Add zdd_join (and zdd_joinnext and zdd_joinprev) similar to bdd_relprod (and bdd_relnext and bdd_relprev).
  • Here, it is quite important to first zdd_expand the set of states to also include the to-be quantified variables as don't cares.
  • As an optimisation, we should be expanding the set of states on-the-fly during the intersection operation.