#947 Using saturation to improve BDD reachability performance

Closes #947 (closed).

This PR contributes the saturation exploration strategy. Short summary of changes:

• I added a new option --exploration-strategy which replaces --edge-workset. The currently available exploration strategies are: chaining-fixed, chaining-workset, and saturation. The saturation strategy is now the default.
• I updated the existing regression tests, which now (mostly) use saturation. I made two extra regression tests for chaining-fixed. We may want to add more, not sure.
• I implemented saturation as part of CifBddReachability. This also required two small changes to CifBddEdge. The change to CifBddEdge#getSupportFor is rather technical. Currently relnext and relprev assume that, if some new-state BDD variable is in the support set of a transition relation, then the corresponding old-state variable is relevant as well for applying the edge, even if that variable is not in the support set. Saturation doesn't make that assumption. Adapting saturation according to this assumption is possible, but more difficult than simply changing CifBddEdge#getSupportFor to capture all relevant variables explicitly.

I ran the CIF data-based synthesis benchmarks with and without saturation: _overview.html. Saturation is always at least as good as chaining-fixed in terms of required memory, and is always better in terms of number of BDD operations. On average saturation is 14.5x faster. But is model dependent. Some models get slightly faster, while others get >100x faster.

Best to review commit by commit.