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.

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

v2.0.0-rc.1

New Features

• bdd_printdot(f, out) and zdd_printdot(A, out)
  These now take 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.
• exec_policy now also includes heuristical variables for Nested Sweeping and Quantification
  • exec_policy::quantify::transposition_growth: The maximum size the BDD may grow to repeat the initial transposition step.
  • exec_policy::quantify::transposition_max: The maximal number of sweeps. This value may be further decreased based on internal heuristics.
• bdd_optmin(f, c)
  New function to derive the assignment in f that is minimal with respect to a linear cost function c.

Optimisations

• Based on our experiments for v2.0.0-beta.3, the threshold to use levelized random access has been increased to half of what the replaced priority queue would use.
• Levelized Random Access now only depends on whether a BDD is indexable and not canonical.
• Added levelized random access to quantification. This improves performance, depending on the instance solved, by 0% to 40%.

Bug Fixes

• Multiple fixes (and extensions) to the statistics for Nested Sweeping.

Breaking Changes

• 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 getters in exec_policy are generalized as a .get to match the .set (and to remove headaches in clashing definitions).
• The exec_policy::quantify enum has been moved into exec_policy::quantify::algorithm. Simultaneously, it now only has two options: Nested and Singleton. This removes Partial completely. The previous meaning of Nested is intact by setting exec_policy::quantify::transposition_max to 0.
• Replaced the old adiar::bool_op in favour of an adiar::predicate<bool, bool>.

Contributors

• Steffan Sølvsten ( @SSoelvsten )
• Erik Funder Carstensen ( @halvko )

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 )

v2.0.0-beta.5

New Features

• Functional Bridge:
  Fully generalized and committed to the use of functions to bridge between Adiar and the user's code (as was started in v2.0-beta.2). To this end, Adiar now provides the types predicate<...> and generator<...> 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.
• 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.
• bdd_top(), bdd_bot(), 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.

Optimisations

• bdd_satmin and bdd_satmax
  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.

Breaking Changes

• The function overloads with an auxiliary file as an input, e.g. bdd_restrict, zdd_onset, bdd_varprofile, have been removed in favour of the new functional input instead.
• The enums memory_mode, access_mode, and quantify_mode have been removed in favour of using the new Execution Policy.
• Removed the functions bdd_counter and zdd_sized_set. They may be added anew, assuming someone sends in a feature request.
• Fixed inconsistency of 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.
• Removed the map_pair class introduced in v2.0-beta.2 as it has become redundant with the simpler function interface.

Contributors

• Steffan Sølvsten ( @SSoelvsten )

v2.0.0-beta.4.4

Optimisations

• Nested Sweeping
  Implements the Repeated Partial Quantification as an alternative to Nested Sweeping or Singleton Quantification. This algorithm is a generalization of Singleton Quantification such that multiple variables can be quantified within the same sweep. When using the auto heuristics, we use this new algorithm to transpose the input until Nested Sweeping is (or very much might) be the better option.

Bug Fixes

• Fixes the fact that some Clang compilers break the memory computations of the auxiliary data structures due to (questionably) undefined behaviour.

Other

• Changes to the way Adiar does its assertions to improve the possibility to debug, test, and maintain.

Contributors

• Steffan Sølvsten ( @SSoelvsten )

Also, thanks to @nhusung for helping me track down the bug due to undefined behaviour.

v2.0.0-beta.4.3

Optimisations

• Nested Sweeping
  Ensure transposition for the generator-based quantification actually is run on a variable that exists in the decision diagram.

Contributors

• Steffan Sølvsten ( @SSoelvsten )

v2.0.0-beta.4.2

Optimisations

• Nested Sweeping
  Add to skip some of the expensive parts of the Reduce sweeps. This can improve performance at the cost of increasing the size of intermediate results. This can be controlled at compile-time (pruning conditional statements) or heuristically at run-time. Currently, the heuristic is to only skip in the outer-most Reduce if reduction prunes less than 5%.

Contributors

• Steffan Sølvsten ( @SSoelvsten )

v2.0.0-beta.4.1

Optimisations

• Nested Sweeping
  If no requests for the inner sweep actually manipulate the sub-graph, then the entire sweep can be skipped (improving performance). For quantification, this happens when all to-be quantified nodes on a level either suddenly become suppressed or there is at least one terminal child.

Contributors

• Steffan Sølvsten ( @SSoelvsten )

v2.0.0-beta.4.0

New Features

• zdd_project(...)
  Added new overloads using (stateful) label generator functions and iterators.
• adiar_set_domain(...)
  Add overload to set domain given a generator function, or an iterator.
• bdd_satmin(...), bdd_satmax(...), zdd_minelem, and zdd_maxelem(...)
  Add overload with a callback function to be compatible with all desired output data structures.

Optimisations

• Nested Sweeping
  Implemented this framework to add support for an I/O-efficient simulation of BDD operations that (may) recurse on intermediate results. The multi-variable quantification operations, i.e. bdd_exists, bdd_forall, and zdd_project, use this to decrease their memory usage and their running time.

Breaking Changes

• bdd_exists, bdd_forall, and zdd_project
  Removed the overload for multi-variable quantification when given a file with labels.
• 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.
  • Semantics has been changed if the global domain has been set. If so, then it will return the assignment to the variables in the domain rather than specifically the levels present in the BDD.
• Every deprecated function from v1.x has been removed.
• 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,

Contributors

• Steffan Sølvsten ( @SSoelvsten )