v2.0.0-beta.6

Extending many of the previous clean-up and refactorings to remaining parts of the library. The refactoring also includes some clean up of the random access version of the product construction algorithm introduced in v2.0-beta.3.

New Features

• bdd_and(...) and bdd_or(...)
  These BDD builder functions now support negated variables. This can either be parsed as pairs with a negation flag, i.e. {x, true}, or by parsing the negated label, i.e. -x.

• bdd_satmin, bdd_satmax, zdd_minelem, and zdd_maxelem
  Added overload with output iterators.

• bdd_const(...) and bdd_isconst(f)
  Added as aliases for bdd_terminal(...) and bdd_isterminal(f), respectively.

• bdd_topvar(f) and zdd_topvar(A)
  Added functions to get root variable. Until the addition of a non-identity variable ordering, this is equivalent to bdd_minvar(...) and zdd_minvar(...)

• bdd_restrict(f, ...), zdd_onset(A, ...), and zdd_offset(A, ...)
  Added overload with a single variable. For ZDDs, the default variable is zdd_topvar(A). For BDDs, bdd_low(f) and bdd_high(f) sets the top variable to the desired value.

• bdd_iscube(f) and bdd_cube(...), and zdd_ispoint(A) and zdd_point(...)
  The builder functions are aliases for bdd_and and zdd_vars. The predicates are new and run in constant-time.

• bdd_isvar(f), bdd_isithvar(f), and bdd_isnithvar(f)
  Predicates for whether a BDD is a single variable. These are resolved in constant-time.

• <adiar/version.h>
  Header file containing compile-time and inlinable integer/string variables with the current version of Adiar.

• Extended statistics with information from Nested Sweeping framework and Quantification algorithm

Optimisations

• zdd_minelem and zdd_maxelem
  Reuses the optimisation introduced for bdd_satmin and bdd_satmax (in v2.0-beta.5)

• bdd_equal(f, g) and zdd_equal(A, B)
  Added constant time fail-fast if the width of the two BDDs do not match.

• Decreased bdd::max_label and zdd::max_label by two to then double bdd::max_id and zdd::max_id This way, we again support BDDs and ZDDs of up to 12 TiB.

Bug Fixes

• Fixed internal::levelized_file<...>::copy() does not copy over the constant-space meta information.

Breaking Changes

• bdd_satmin and bdd_satmax
  Similar to other BDD packages, these operations now only report the labels of the nodes visited on the path through the BDD. That is, the output is now independent of the global variable domain and the BDD's levels.

  Furthermore, the consumer function now takes the label and its value as a single pair rather than two values.

• bdd_varprofile(...) and zdd_varprofile(...)
  These have been renamed to bdd_support(...) and zdd_support(...). This improves its discoverability and better reflects its content.

Contributors

• Steffan Sølvsten ( @SSoelvsten )