Add `bdd_isvar` and `zdd_isvar`

[SSoelvsten]

Similar to bdd_istrue and other predicates, one would also want to have a predicate whether something is a mere variable, i.e. whether something is equivalent to the result of bdd_ithvar (and bdd_nithvar).

BDD Tasks:

• bdd_isvar: Trivially check whether the BDD has exactly two arcs to terminals; this is only possible, if there is a single internal node.
• bdd_isithvar: If bdd_isvar is true, load the single node and check its shape.
• bdd_isnithvar: If bdd_isvar is true, load the single node and check its shape.

With #433 , the bdd_isithvar and bdd_isnithvar collapses to checking the complement flag rather than the BDD node.

ZDD Tasks:

• zdd_isvar: Check the ZDD is a chain with a single variable set to true (or set to false, i.e. skipped). Early termination cases:
  • Width should be 1.
  • Number of arcs to false should be 0 or 1.
  • Number of arcs to true should be 1 or 2.
  • The number of levels should match the size of the domain (or be one short of it).
• zdd_isithvar: Extend the above checking of a chain where one has to be true. Early termination cases:
  • Width should be 1.
  • Number of arcs to false should be 1.
  • Number of arcs to true should be 1 or 2.
  • The number of levels should match the size of the domain.
• zdd_isnithvar: Extend the above checking of a chain where one has to be false (skipped). Early termination cases:
  • Width should be 1.
  • Number of arcs to false should be 0.
  • Number of arcs to true should be 2.
  • The number of levels should be one short of the size of the domain.

Yet, question then still is whether the levels that are there actually match with the domain. Hence, we still need to use an O(N) time scan of all ZDD nodes afterwards.

Notes:

Additional context
Requested on email by Anna Blume Jakobsen, based on her prior experience using BDDs in her BSc and MSc projects and student programmer tasks.