Add `bdd_iscube` and `bdd_cube`

[SSoelvsten]

In CAL, there is the predicate Cal_BddIsCube(...) that identifies whether a decision diagram represents a cube. This is quite a simple operation to add here too.

• Declare the new predicate bdd_iscube in adiar/bdd.h (implemented in adiar/bdd/build.cpp). It is true iff
  • If the DD is a terminal, then it is a cube iff it is the true terminal
  • Otherwise, each node has to have exactly one of its children pointing to the false terminal (and hence there should only ever be one node per level). Yet, we have enough metadata to check this in O(1) time.
    • Check whether the width is 1
    • Check the number of arcs to true exactly 1.
    • Check the number of of arcs to false is exactly bdd_varcount.
• Declare in adiar/bdd.h the bdd_cube function (implemented in adiar/bdd/build.cpp).
  • Given a (descending) generator function it constructs the cube.
  • This is a mere alias for #556 .
  • Afterwards, simplify the code in bdd_sat_bdd_callback in adiar/bdd/evaluate.cpp

Of course, both operations above should be unit tested.

[SSoelvsten]

I am unsure how a ZDD ought to be a cube. If the DAG has to be of the same shape as the BDD one, then by the semantics of the suppressed node, it is not so much a cube as it is a single point? It is hard to tell from the CUDD API whether the idea of a cube only really applies to BDDs - and if it also applies to ZDDs then how so.

Edit: See #571

[SSoelvsten]

The implementation of bdd_cube can also be merged with the implementation of #556 ; it is at that point merely an alias for bdd_and.