v2.1.0

Addition of the BDD operations needed for model checking!

New Features

Binary Decision Diagrams

• f + g operator:

  Alias for bdd_or(f,g).

• f - g operator:

  Alias for bdd_diff(f,g).

• f * g operator:

  Alias for bdd_and(f,g).

• bdd_satmin(f) and bdd_satmax(f):

  This is now overloaded to provide the variables that (at least) ought to be included in the result. In model checking, this is needed to obtain a single (symbolic) state from a set of (symbolic) states.

  • bdd_satmin(f, gen, size): find the lexicographically smallest assignment with the size number of variables provided by the generator, gen.

  • bdd_satmin(f, cbegin, cend): find the lexicographically smallest assignment of f where the variables between cbegin and cend should be included. Notice, that cbegin and cend are read-only; if the writeable begin and end are used, then the previous behaviour of an output range is used.

  • bdd_satmin(f, c): find the lexicographically smallest assignment of f with the variables in the BDD cube c.

• bdd_replace(f, m)

  Rename variables in f according to the mapping function m. In model checking, this is used to switch from unprimed to primed variables and back again.

  NOTE: If m does not map the variables of f monotonically, then an exception is thrown; non-monotone mappings are planned for later.

• bdd_relprod(s, r, pred)

  Apply the relational product on states, s, and relation, r, while quantifying the variables for which the given predicate evaluates to true.

• bdd_relnext(s, r, m)

  Compute a step forwards from states s according to relation r. The (partial) variable mapping m maps variables back from primed to unprimed states; variables not mapped by m are existentially quantified.

• bdd_relprev(s, r, m)

  Compute a step backwards from states s according to relation r. The (partial) variable mapping m maps variables from unprimed to primed states; variables not mapped by m are existentially quantified.

Zero-suppressed Decision Diagrams

• f + g operator:

  Alias for zdd_union(f,g).

• f * g operator:

  Alias for zdd_intsec(f,g).

Optimisations

• Moved the logic for on-the-fly BDD negation from the generic file stream class into the one specifically for BDD nodes. This removes (unused) branches within the other streams. Furthermore, the logic to negate each BDD node has been optimised to remove another branch statement. This improves performance somewhere between 0% and 2%.

• The newly added bdd_replace(f, m) optimises CPU and space usage depending on f and how m maps the variables of f.

  • If f is an unreduced rvalue, then variable renaming is incorporated into the Reduce algorithm (only calling m once per variable in f).
  • If m(x) = x is the identity function (on the support of f) then f is returned using no additional space.
  • If m(x) = x+c for some constant c then BDD nodes in f are (similar to negation) remapped on-the-fly. This also uses no additional space and only adds an insignificant overhead.
  • Otherwise, all BDD nodes of f are mapped using linear time, I/Os, and space.

• The newly added bdd_replace(f, m), bdd_relnext(s, r, m), and bdd_relprev(s, r, m) are overloaded with an optional additional argument that is the type of m. This immediately identifies which case above can be applied (instead of spending time inferring it).

• The bdd_exists(f, ...) and bdd_forall(f, ...) functions now skip the initial transposition of f if it is an unreduced rvalue.

Bug Fixes

• Fixed compilation error on ARM64 Linux due to missing signedness.

• Fixed overflow error when a single BDD's width outgrows 32 bits (96 GiB)

• Fixed Outer Reduce in Nested Sweeping framework crashes due to assuming its priority queues are (like the regular Reduce) only inducing a 1-level cut on the input.

• Fixed "Not enough phase 1 memory for 128 KB items and an open stream!" error messages when running bdd_exists(f, ...) and bdd_forall(f, ...) with exclusively external memory data structures.

• Fixed that TPIE leaves a log file in the default temporary directory when another has been specified.

Other Changes

• The maximum number of BDD variables has been decreased to 2097149 (21 bytes for the label). This is done to guarantee that a single integer of each level can easily fit into memory.

  This has the added benefit, that the maximum supported BDD size is increased to the absurd size of 96 TiB .

• Disabled TPIE from outputting its debug log to a disk on the file if Adiar is compiled for production. This drastically saves on disk space (some benchmarks ran out of disk not due to large BDDs but due to several TiB of debug logging).

Deprecation

• Iterator-based outputs have had their begin and end iterator pairs replaced with a single output iterator. This affects the bdd_support, bdd_satmin, bdd_satmax, zdd_support, zdd_minelem, and zdd_maxelem functions.

Contributors

• Steffan Sølvsten ( @SSoelvsten )

Thanks for the support and advice from Jaco van de Pol ( @jacopol ) . Also, thanks to Nils Husung ( @nhusung ) for fixing compilation on ARM64 machines and fixing TPIE leaving log files in the default temporary directory.