Recent Releases of adiar

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

- C++
Published by SSoelvsten over 1 year ago

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

- C++
Published by SSoelvsten about 2 years ago

adiar - 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 )

- C++
Published by SSoelvsten about 2 years ago

adiar - 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.
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 )

- C++
Published by SSoelvsten over 2 years ago

adiar - v2.0.0-beta.5

New Features

Functional Bridge: Fully generalised 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 )

- C++
Published by SSoelvsten over 2 years ago

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

- C++
Published by SSoelvsten almost 3 years ago

adiar - 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 )

- C++
Published by SSoelvsten almost 3 years ago

adiar - 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 )

- C++
Published by SSoelvsten almost 3 years ago

adiar - 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 )

- C++
Published by SSoelvsten almost 3 years ago

adiar - 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 )

- C++
Published by SSoelvsten almost 3 years ago

adiar - v2.0.0-beta.3

New Features

adiar_set_domain(...) Overloaded to allow creating the domain 0, 1, ..., n-1 when given the number of variables n.

Optimisations

access_mode enum If set to AUTO or to RA then bdd_apply, zdd_binop, and their derivatives will use random access on one of the inputs (if possible). This circumvents using an entire priority queue, thereby improving performance on average by 7%. This is especially beneficial when applying an operator to a very large decision diagram together with a narrow one.

Breaking Changes

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(i) function has been added. The original semantics of zdd_ithvar is still provided with the zdd_singleton function.

Contributors

Casper Moldrup Rysgaard ( @Crowton )
Steffan Sølvsten ( @SSoelvsten )

- C++
Published by SSoelvsten about 3 years ago

adiar - v2.0.0-beta.2

Following up on the prior major rewrite and updating the interface for nested sweeping.

New Features

Added new overloads for bdd_exists, bdd_forall and zdd_project using 1 label predicates, 2 label generator functions, and [3] iterators. For example, bdd_exists is now overloaded with the following alternatives
- 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).

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

Turned assignment into a class similar to the changes with v2.0.0-beta.1
Generalized assignment into a var_map class with an enum for its second value. This is used for inheritance to the (new) evaluation class used for outputs of bdd_satmin and bdd_satmax. This will probably again be broken later, as their default output is turned into a bdd.

Contributors

Steffan Sølvsten ( @SSoelvsten )

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

- C++
Published by SSoelvsten about 3 years ago

adiar - v2.0.0-beta.1

Major rewrite of the internal logic of Adiar to pay off technical debt and to get Adiar ready for implementing the I/O-efficient version of the much more complex BDD operations (e.g. 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.

Breaking Changes

Fundamental data types in have been moved to each their own file (most of which are placed in the ).
- The fundamental data types have been converted from C-like structs with manipulating functions to C++ (immutable) classes. That is, the entire interface for node, arc etc. have completely changed. Most of these functions have been deprecated to make transitioning easier.
Files, streams and their writers have also been moved to leaving only to expose the public parts of the API.
Files have been rewritten and renamed.
- If you have been using a label_file or an assignment_file you should now use the shared_file<T> template instead. To read from it use the file_stream<T> and to write use the file_writer<T>.
- The node_file class is replaced with the adiar::internal::sharedlevelizedfile<node>. You can read from it with the adiar::internal::node_stream and write to it with the adiar::internal::node_writer as before. But, we highly encourage you to transition over to using the adiar::bdd_builder and adiar::zdd_builder instead.
All internal logic in 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.

That is, there are only breaking changes if you have been interacting with Adiar's files directly, e.g. you have used the bdd_restrict, bdd_exists, bdd_forall functions or have created BDDs by hand with the node_writer.

Contributors

Steffan Sølvsten ( @SSoelvsten )

- C++
Published by SSoelvsten over 3 years ago

adiar - v1.2.2

Bug Fixes

zdd_project(A, dom) An accidental swapping of arguments for a helper function resulted in the generated recursion requests are for the wrong elements and hence the wrong ZDD was constructed.
Fixes C++ and CMake such that Adiar compiles and runs on Mac computers with default Clang.

Contributors

Steffan Sølvsten ( @SSoelvsten )

- C++
Published by SSoelvsten over 3 years ago

adiar - v1.2.1

Bug Fixes

adiar_printstats() Makes sure to print levelized priority queue statistics, when only the unbucketed priority queue has been used.

Deprecations

adiar/bdd.h
- output_dot(bdd f, std::string file_name) -> bdd_printdot(bdd f, std::string file_name)
adiar/zdd.h
- output_dot(zdd A, std::string file_name) -> zdd_printdot(zdd A, std::string file_name)

Binary Decision Diagrams

bdd_satcount(bdd f) If the global domain is set, then that value will take precedence over the number of levels in f (assuming f has fewer levels than the domain claims to exist).
bdd_printdot(bdd f, std::ostream out) Added to allow more flexibility when outputting DOT files.

Zero-suppressed Decision Diagrams

zdd_printdot(zdd A, std::ostream out) Added to allow more flexibility when outputting DOT files.

Documentation

Instead of separate Markdown files, the documentation is generated directly from the C++ codebase with Doxygen. You can generate the documentation (assuming Doxygen is intalled) with the docs Makefile target.

Contributors

Steffan Sølvsten ( @SSoelvsten )

License

Adiar uses the TPIE library which is licensed under LGPL v3, and so by extension any binary file with Adiar is covered by the very same license.

- C++
Published by SSoelvsten over 3 years ago

adiar - 1.2.0

Drastically improves performance for small instances by using purely internal memory data structures.

Performance

Below is the running time for the N-Queens for v1.0, v1.1, and v1.2. As is evident, it is an improvement all across the board. Furthermore, the change in v1.1 that improved running time for large instances but severely crippled the small ones has been mitigated.

| N | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | 16 | |------------------|--------------|--------------|--------------|---------------|--------------|---------------|-----------------|---------------|-----------------|-------------------| | v1.0 (s) | 7.4s |8.2s | 7.8s | 9.4s | 28.5s | 28.5s | 119s | 660s | 3944s | 31017s | | v1.1 (s) |19.3s | 25.6s | 32.2s | 39.5s | 48.7s | 58.4s | 751s | 1296s | 4270s | 24544s | | v1.2 (s) |0.1s | 0.2s | 0.4s | 0.8s | 3.1s |14.8s | 82.7s | 502s | 3337s | 23127s |

Domain

The global domain over which one works can now be set as a label_file in a global variable.

adiar_set_domain(label_file dom) Set the global domain variable.
adiar_has_domain() Whether a global domain already is set.
adiar_get_domain() Obtain the current label_file that acts as the global domain (assuming adiar_has_domain() evaluates to true).

Binary Decision Diagrams

New Features

bdd_builder A new class to replace using the node_writer directly. This allows you to much more naturally construct BDDs bottom-up by hiding away several details. Furthermore, it makes use of exceptions rather than immediately terminating assertions.
bdd_from(zdd A) Converts from a ZDD to a BDD using the global domain.
bdd_equal(bdd f, bdd g) Alternative to using the == operator.
bdd_unequal(bdd f, bdd g) Alternative to using the != operator.
bdd_varprofile(bdd f) Obtain a label_file containing all of the variables present in a BDD.

Bug Fixes

bdd_nithvar(label_t i) and bdd_ithvar(label_t i) Is now marked as canonical and so can be used with the linear-scan equality checking.
Fixed the reduction phase may use 2 MiB more memory than is available.

Zero-suppressed Decision Diagrams

New Features

zdd_builder A new class to replace using the node_writer directly. This allows you to much more naturally construct ZDDs bottom-up by hiding away several details. Furthermore, it makes use of exceptions rather than immediately terminating assertions.
zdd_complement(zdd A) Complementation within the global domain.
zdd_from(bdd f) Converts from a BDD to a ZDD using the global domain.
zdd_varprofile(zdd A) Obtain a label_file containing all of the variables present in a ZDD.

Bug Fixes

zdd_ithvar(label_t i) Is now marked as canonical and so can be used with the linear-scan equality checking.
Fixed the reduction phase may use 2 MiB more memory than is available.
DOT files are now properly produced with the terminals printed as Ø and {Ø}.

Statistics

New Features

Statistics have been heavily extended with information on how often each type of auxiliary data structures (internal or external) have been used.
All statistics variables are now fixed-precision numbers (using the CNL library) making sure there are no overflows in the provided numbers.
adiar_statsreset() Reset all statistics values back to 0.

Bug Fixes

Fixed fine grained statistics (ADIARSTATSEXTRA) are turned on when only coarse-grained statistics (ADIAR_STATS) was desired.

Deprecations

The word sink has been replaced with the word terminal that is more commonly used in the context of decision diagrams.

adiar/data.h
- create_sink_uid(bool val) -> create_terminal_uid(bool val)
- create_sink_ptr(bool val) -> create_terminal_ptr(bool val)
- create_sink(bool val) -> create_terminal(bool val)
adiar/bdd.h
- is_sink(bdd f) -> is_terminal(bdd f)
- bdd_sink(bool val) -> bdd_terminal(bool val)
adiar/zdd.h
- is_sink(zdd A) -> is_terminal(zdd A)
- zdd_sink(bool val) -> zdd_terminal(bool val)

Breaking Changes

The terminal predicates is_any, is_true and is_false with the prior is_sink(zdd A, pred) functions were too complicated. The above performance improvements allows us for a much simpler (and faster) implementation. Deprecation was not possible due to name conflicts with their replacements below. Considering the niche usage of this, it does not seem to warrant an increment in version number.

adiar/data.h
- is_sink(ptr_t p), is_true(ptr_t p), and is_false(ptr_t p).
adiar/bdd.h
- is_sink(bdd f), is_true(bdd f) and is_false(bdd f).
adiar/zdd.h
- is_sink(zdd A), is_null(zdd A) and is_empty(zdd A).

Contributors

Steffan Sølvsten ( @SSoelvsten )
Anna Blume Jakobsen ( @AnnaBlume99 )
Jaco van de Pol ( @jacopol )

Also thanks to Erik Funder Carstensen ( @halvko ) for fixing a few compiler warning in statistics.

License

Adiar uses the TPIE library which is licensed under LGPL v3, and so by extension any binary file with Adiar is covered by the very same license.

- C++
Published by SSoelvsten almost 4 years ago

adiar - 1.1.0

Major refactor and rewrite of the codebase to also support zero-suppressed decision diagrams!

Binary Decision Diagrams

bdd_eval(bdd f, assignment_func x) Alternative to using an assignment_file you can provide any function that given the variable label outputs the boolean value assigned to it.

Zero-suppressed Decision Diagrams

Adds support for zero-suppressed decision diagrams with the zdd class. All operations on ZDDs are based on the family of sets semantics as in the original paper by Minato.

Constructors

zdd zdd_sink(bool v) and zdd_empty() and zdd_null() as alternatives
zdd zdd_ithvar(label_t i)
zdd zdd_vars(label_file vars) to construct an and chain.
zdd zdd_singletons(label_file vars) to construct an *or chain.
zdd zdd_powerset(label_file vars) to construct a don't care chain.
zdd zdd_sized_set<pred_t>(label_file vars, k, pred) to construct the sets of variables in vars whose size satisfies the given predicate in relation to k.

Basic Manipulation

zdd zdd_binop(zdd A, zdd B, bool_op op) to apply a binary operator to two families of sets
zdd zdd_change(zdd A, label_file vars) to compute the symmetric difference.
zdd zdd_complement(zdd A, label_file dom) to construct the complement.
zdd zdd_expand(zdd A, label_file vars) to expand the domain with new variables.
zdd zdd_offset(zdd A, label_file vars) to compute the subset without the given variables.
zdd zdd_onset(zdd A, label_file vars) to compute the subset with the given variables.
zdd zdd_project(zdd A, label_file is) to project onto a (smaller) domain.

Counting Operations

uint64_t zdd_nodecount(zdd A) to obtain the number of (non-leaf) nodes.
uint64_t zdd_varcount(zdd A) to obtain the number of levels present (i.e. variables).
uint64_t bdd_size(bdd A) to compute the number of elements in the family of sets.

Predicates

bool zdd_equal(zdd A, zdd B) to check for set equality.
bool zdd_unequal(zdd A, zdd B) to check set inequality.
bool zdd_subseteq(zdd A, zdd B) to check for weak subset inclusion.
bool zdd_subset(zdd A, zdd B) to check for strict subset inclusion.
bool zdd_disjoint(zdd A, zdd B) to check for the sets being disjoint.

Set Elements

bool zdd_contains(zdd A, label_file a) to compute whether the set of variables a is in A
std::optional<label_file> zdd_minelem(zdd A) to obtain the a in A that is lexicographically smallest.
std::optional<label_file> zdd_maxelem(zdd A) to obtain the a in A that is lexicographically largest.

Other Functions

output_dot(bdd f, std::string filename) to output a visualizable _.dot file.
zdd zdd_from(bdd f, label_file dom) and bdd bdd_from(zdd f, label_file dom) to convert between BDDs and ZDDs interpreted in the given domain.

Statistics

Compile Adiar with ADIAR_STATS or ADIAR_STATS_EXTRA to gather statistics about the execution of the internal algorithms. With ADIAR_STATS you only gather statistics that introduce a small constant time overhead to every operation. ADIAR_STATS_EXTRA also gathers much more detailed information, such as the bucket-hits of the levelized priority queue, which does introduce a linear-time overhead to every operation.

stats_t adiar_stats() to obtain a copy of the raw data values.
void adiar_printstat(std::ostream) to print all statistics to an output stream.

Performance

We have (yet) not done a proper comparison concerning changes in performance. But, our initial tests throughout development hint at a 4% performance decrease where we can regain about 2% of it with some extra templating.

Contributors

Steffan Sølvsten ( @SSoelvsten )
Jaco van de Pol ( @jacopol )

Also thanks to Jakob Schneider Villumsen ( @jaschdoc ) for his additions to the setup of the git repository.

License

Adiar uses the TPIE library which is licensed under LGPL v3, and so by extension any binary file with Adiar is covered by the very same license.

- C++
Published by SSoelvsten over 4 years ago

adiar - 1.0.1

Bug fixes

2ab5b185461c3fe83c422823b8ab26ccf100fb6d : Fix tuples in bdd_apply have their ties on std::min or std::max not broken correctly. This resulted in that the same recursion request could potentially be handled multiple times independently, since all its "calls" ended up interleaving with other tied requests in the priority queues.
f80a924f3196d3d53ef4371048c40df0be9f6b23 : Slightly improve performance of some bool_ops. Most likely this is negligible.
d222569f390c5156e92436dffe5c0aa56e3c320e: Fix bdd_counter returns trivially false cases as true.
8fcc04ed4dd5f3a332ffdc01f6be0e7fb5108165 : Now Adiar compiles with C++17 regardless of its parent project. This allows the user to omit the use of set_target_properties(<target> PROPERTIES CXX_STANDARD 17) in their own CMake settings.

Changes

aac630fb2ef309df3622bf4d7740f7cfa827091d : adiar_init now takes its memory argument in bytes rather than in MiB.
Equality Checking (==) is improved in its performance from its prior O(N² log N²) time comparison. See pull request #127 for all changes, though most important to highlight are the following two commits:
- cee73b37425826dfbc0ea24d7e7548bd93c7d6f9 : If both given BDDs are canonical (as defined in the documentation) and have the same value in their negation flag, then equality checking is done with a simple (and much faster) linear scan.
- c2812a9166f75e562159bebf34eefc668431a772 : In all other cases the prior time-forward processing algorithm is used. But this one has been improved to be an O(N log N) time comparison algorithm. That is, equality checking is not only a constant improvement computing ~(f ^ g) == bdd_true() but it is provably faster (both in terms of time and I/Os).

Performance

Apply

We can compare the performance we recorded for our BDD benchmarks run on the CSCAA Grendel-S cluster last winter for v1.0.0 to the ones we are currently running for v1.0.1. Shown below we have the relative performance difference for the N-Queens example.

| N | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | 16 | 17 | |----|-------------|-------------|-------------|-------------|-------------|-----------|-----------|-----------|-----------|-----------|------------| | % | -44.70% | -33.92% | -16.94% | -18.81% | -26.65% | -2.04% | -3.20% | -4.56% | -3.51% | -6.55% | -5.52% |

Negative numbers are good.

Equality Checking

We have no numbers to compare to, but the new Picotrav benchmark added to our BDD benchmarks provide an insight into its performance.

The largest circuits we have verified were the mem_ctrl ones. Here, every BDD was on average 499 MiB in size, i.e. on average about 1 GiB of BDD nodes were compared. These were compared in 0.2 GiB/S.
The voter benchmark has a single output gate, where each BDD takes up 5.74 MiB. One version requires us to use the O(N log N) time-forwarded algorithm and the other the much faster O(N) linear scan algorithm. Our experiments show that the linear scan is about 10 times faster than the time-forwarded comparison, and (depending on your SSD speed) you can compare 1.86 GiB/s for equality.

Contributors

Steffan Sølvsten ( @SSoelvsten )
Jaco van de Pol ( @jacopol )

License

Adiar uses the TPIE library which is licensed under LGPL v3, and so by extension any binary file with Adiar is covered by the very same license.

- C++
Published by SSoelvsten over 4 years ago

adiar - 1.0.0

Initial release of Adiar!

BDD functions

bdd class to hide away management of files and running the reduce algorithm. This takes care of reference counting and optimal garbage collection.

Constructors

bdd_sink(bool v) or use the alternatives: bdd_true() and bdd_false()
bdd_ithvar(label_t i)
bdd_nithvar(label_t i)
bdd_and(label_file ls) to construct an and chain.
bdd_or(label_file ls) to construct an or chain.
bdd_counter(label_t min_label, label_t max_label, label_t threshold) to construct whether exactly threshold many variables in the given interval are true.

Furthermore, the node_writer class is also provided as a means to construct a BDD manually bottom-up.

Basic Manipulation

bdd_apply(bdd f, bdd g, bool_op op) to combine two BDDs with a binary operator (also includes aliases for every possible op)
bdd_ite(bdd f, bdd g, bdd h) to compute the if-then-else
bdd_not(bdd f) to negate a bdd
bdd_restrict(bdd f, assignment_file as) to fix the value of one or more variables
bdd_exists(bdd f, label_t i) bdd_forall(bdd f, label_t i) to existentially or forall quantify a single variable. Overloading also allows quantifying multiple labels. But, these are still quantified one by one!

Counting Operations

bdd_nodecount(bdd f) to obtain the number of (non-leaf) nodes.
bdd_varcount(bdd f) the number of levels present (i.e. variables).
bdd_pathcount(bdd f) the number of unique paths to the true sink.
bdd_satcount(bdd f, size_t varcount) the number of satisfying assignments.

Other Functions

bdd_eval(bdd f, assignment_file x) to compute f(x).
bdd_satmin(bdd f), resp. bdd_satmax(bdd f) to find the lexicographical smallest, resp. largest, satisfying assignment.
output_dot(bdd f, std::string filename) to output a visualizable .dot file.

Contributors

Steffan Sølvsten( @SSoelvsten )
Jaco van de Pol ( @jacopol )
Anna Blume Jakobsen ( @AnnaBlume99 )
Mathias Weller Berg Thomasen ( @MathiasWeller42 )

Thanks to the following people for helping with bugfixes and guidance on I/O algorithms, TPIE and C++.

Asger Hautop Drewsen ( @Tyilo )
Lars Arge
Mathias Rav ( @Mortal )

License

Adiar uses the TPIE library which is licensed under LGPL v3, and so by extension any binary file of Adiar is covered by the very same license.

- C++
Published by SSoelvsten about 5 years ago