v2.0.0

Major rewrite of the internal logic of Adiar to pay off technical debt and to support more complex BDD operations. These changes also address major quality-of-life issues in the API of v1.x. Finally, these changes brings Adiar much closer to support other types of decision diagrams (e.g. QMDDs) and many other features.

With this rewrite in-hand, Adiar now includes a much more complex (and faster) implementation of Multi-variable Quantification. Furthermore, this rewrite also supported the addition of Levelized Random Access to improve the performance of some of its operations.

New Features

• Functional Bridge:
  Adiar now uses generic and versatile functions to bridge between Adiar and the user's code. To this end, Adiar provides the predicate<...> and generator<...> types to pass information into Adiar and consumer<...> to pass information back out again. All functions of v1.x that used some file, e.g. bdd_restrict, zdd_onset, bdd_varprofile etc. all now provide one (or more) of these functions instead. For example, bdd_exists is now overloaded with the following alternatives

  • bdd_exists(f, x): quantify the variable x (also part of v1.x).
  • bdd_exists(f, pred): quantify all variables i in f where pred(i) evaluates to true.
  • bdd_exists(f, gen): quantify all variables i generated by gen(). Here it is important that gen() provides the variables in descending order.
  • bdd_exists(f, begin, end): quantify all variables i from begin to end (assuming these are sorted in descending order).

• Execution Policy:
  Each algorithm (when relevant) has been overloaded with an exec_policy as its first argument. This class provides a thread-safe way of passing options into an algorithm, e.g. whether the algorithm should use internal or external memory data structures. This replaces the use of the globally set enum values, e.g. memory_mode.

• adiar_set_domain(...)

  • Overloaded to allow creating the domain 0, 1, ..., n-1 when given the number of variables n.
  • Overloaded to set domain given a generator function, or an iterator.

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

Binary Decision Diagrams

• bdd_top() and bdd_bot()
  Provide a uniform interface for getting the top and the bot value of the lattice. This provides a more uniform and interchangeable interface between BDDs and ZDDs where you do not need to think about the reduction rules.

• 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_const(...) and bdd_isconst(f)
  Added as aliases for bdd_terminal(...) and bdd_isterminal(f), respectively.

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

• bdd_restrict(f, x, v), bdd_low(f) and bdd_high(f)
  Added overload with a single variable. The new functions, bdd_low(f) and bdd_high(f), are aliases for setting the top variable to the desired value.

• bdd_iscube(f) and bdd_cube(...)
  The builder function is an alias for bdd_and whereas the predicate is an O(1) operation to recognise this type of diagram.

• 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.

• bdd_satmin(f, ...) and bdd_satmax(f, ...)
  Add overload with a callback function or iterators to be compatible with any data structure of your choice.

• bdd_optmin(f, c)
  New function to derive the assignment in f that is minimal with respect to a linear cost function c.

• bdd_printdot(f, out)
  Now takes a third optional Boolean argument, include_id. If true, then the output includes the level-specific identifiers (which are useful for debugging). By default, this is false and outputs a decision diagram as in most literature.

Zero-suppressed Decision Diagrams

• zdd_top(...), and zdd_bot(...):
  Provide a uniform interface for getting the top and the bot value of the lattice. This provides a more uniform and interchangeable interface between BDDs and ZDDs where you do not need to think about the reduction rules.

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

• zdd_onset(A, ...), and zdd_offset(A, ...)
  Added overload with a single variable. By default, the variable is zdd_topvar(A).

• zdd_ispoint(A) and zdd_point(...)
  The builder function is an alias for zdd_vars whereas the predicate is an O(1) operation to recognise this type of diagram.

• zdd_minelem(A, ...), and zdd_maxelem(A, ...)
  Add overload with a callback function or iterators to be compatible with any data structure of your choice.

• zdd_printdot(f, out)
  Now takes a third optional Boolean argument, include_id. If true, then the output includes the level-specific identifiers (which are useful for debugging). By default, this is false and outputs a decision diagram as in most literature.

Optimisations

• The algorithms bdd_apply, zdd_binop, their derivatives, and bdd_exists, bdd_forall, and zdd_project now use a level-by-level random access on one of the input (if possible). This circumvents using an entire priority queue, thereby drastically improving performance in some cases. This is especially beneficial when applying an operator to a very large decision diagram together with a narrow one.

  With exec_policy::access one can turn this optimisation off and/or force it to always be used.

• The functions bdd_equal(f,g) and zdd_equal(A,B) terminate in constant time, if the width of the two decision diagrams are not the same.

• Added proper support for quantification of multiple variable. This is done with the new Nested Sweeping framework to add support for an I/O-efficient simulation of BDD operations that (may) recurse on intermediate results. This provides a completely new multi-variable quantification operations that is similar to the one in other BDD packages

  With exec_policy::quantify::algorithm, one can pick between this and the previous approach of quantifying one variable at a time.

• bdd_apply(f,g,op) and zdd_binop(A,B,op) now precompute whether the operator op is shortcutting, idempotent or negating for either Boolean value. The commutative operators, e.g. and, or, and xor, are also pre-compiled with these predicates to further optimise conditional if-statements.

• bdd_satmin(f), bdd_satmax(f), zdd_minelem(A), and zdd_maxelem(A)
  Stores the intermediate result in an internal memory stack (since it can at most be 8 MiB in size) rather than writing it out to disk. This should improve their performance slightly.

Bug Fixes

• The result of adiar_stats() is now fixed such that the values for reduce and substitute are correct.
• Many small fixes to make Adiar compile with GCC, Clang, and MSVC on Linux, Mac, and Windows. Simultaneously, we have now set up continuous integration, such that we can truly ensure we support all platforms.

Breaking Changes

There has been a major rewrite of the internal logic of Adiar to pay off technical debt and to get Adiar ready for an I/O-efficient implementation of the Nested Sweeping framework used for multi-variable quantification. At the same time, this also brings Adiar much closer to support other types of decision diagrams (e.g. QMDDs) and to store BDDs on disk and loading them again later.

• All internal logic in <adiar/internal/...> has been moved into its nested namespace adiar::internal. If you use anything from this namespace (e.g. the node and the node_writer classes) then you are not guaranteed non-breaking changes.

• Files, streams and their writers have been moved, rewritten, and renamed. Since newly added predicates and generator functions superseed any use of adiar::file<...>, all file-based overloads have been removed.

Furthermore, the entire API has been overhuled to have a consistent naming scheme. For example, the function is_true(const bdd &) has been renamed to bdd_istrue(const bdd&). This makes them consistent with the rest of the API. The domain and statistics functions have also been renamed for consistency.

Other Breaking Changes

• bdd_satmin(f) and bdd_satmax(f), resp. zdd_minelem(A) and zdd_maxelem(A):

  • The return type when called without a callback function has been turned into a bdd, resp. zdd. This ought to make their return type more usable in a symbolic context.
  • 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.

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

• Removed the functions bdd_counter and zdd_sized_set. They may be added anew as a more generic implementation of Pseudo Boolean Constaints.

• The semantics of the zdd_ithvar function has been changed to be more akin to the BDD semantics. That is, zdd_ithvar(i) is the set of all bitvectors where i is true. Symmetrically, the zdd_nithvar function has been added. The original semantics of zdd_ithvar is still provided with the zdd_singleton function.

• Canonicity of a BDD and ZDD is now a function rather than a member variable. The value is derived from the two underlying features of being indexable and sorted.

• The old adiar::bool_op is now replaced with a future-proof adiar::predicate<bool, bool>.

• The enum memory_mode has been removed in favour of using an Execution Policy.

• The two-level granularity of statistics has been removed. If you want to compile Adiar with statistics you just have to set the CMake variable ADIAR_STATS to ON,

• Every deprecated function from v1.x has been removed.

Contributors

• Steffan Sølvsten ( @SSoelvsten )
• Casper Moldrup Rysgaard ( @Crowton )
• Erik Funder Carstensen ( @halvko )

A huge thanks to Anna Blume Jakobsen ( @AnnaBlume99 ), Andrew Miner ( @asminer ), and Jaco van de Pol ( @jacopol ), for their valuable feedback and suggestions for the design and features of the public API.

Finally, also thanks to Ayoub Aboutarbouch ( @itsmeYO92 ), Maxim Smolskiy ( @MaximSmolskiy ), Nils Husung ( @nhusung ), and Sai Rugveth Vankayala ( @rugveth1210 ) for their small fixes and clean-ups.

License

Adiar 2.0.0 is distributed under the MIT license. But, notice that it depends on the TPIE library which is licensed under LGPL v3. So, by extension any binary file of Adiar is covered by the very same license.