0.5.0

This release introduces several new methods related to more advanced BDD operations. It also deprecates a few methods, but these are replaced with new ones using the same API, so this is only a change of method name. The old methods will stay available until the 1.0.0.

• Adds Bdd::if_then_else operator implemented using Bdd::ternary_op.
• Adds new "low level" apply operators: Bdd::binary_op_with_exists, Bdd::binary_op_with_for_all and Bdd::binary_op_nested (which is a generalisation of the exists and for_all variants).
• Deprecates Bdd::var_project and Bdd::project in favour of Bdd::var_exists and Bdd::exists.
• Adds Bdd::var_for_all and Bdd::for_all.
• New faster implementations for Bdd::exists, Bdd::for_all and Bdd::restrict based on the new apply operators.
• Adds Bdd::to_cnf and Bdd::to_dnf.
• New faster implementations for BddVariableSet::mk_cnf and BddVariableSet::mk_dnf.
• Adds unsafe Bdd::set_num_vars and Bdd::rename_variable methods for explicit manipulation of the underlying BDD. The methods are unsafe because they have a very "low level" effect, but otherwise will always only produce valid BDDs.
• Adds BddVariableSet::mk_sat_up_to_k and BddVariableSet::mk_sat_exactly_k for building BDDs that are satisfied for valuations with up to/exactly k valid literals.
• BddVariableSetBuilder is now clone-able. Because why even wasn't it before?

0.4.2

This version mostly introduces additional low level helper methods. This should not break anything, and it also shouldn't really introduce anything that you need for "normal" use cases.

• Added Bdd::check_binary_op and Bdd::check_fused_binary_flip_op methods. These operations perform a "dry run" of a particular BDD operation, such that from the result we learn (a) if the resulting BDD would have been empty; (b) approximate number of "steps" needed to compute this BDD. Importantly, this should be faster than running the operation in question (as fewer data structures are needed). This method is useful when comparing the complexity of two operations.
• Added Bdd::binary_op_with_limit and Bdd::fused_binary_flip_op_with_limit methods. These methods execute a standard BDD operation, but safely fail (with None) if the number of nodes in the resulting Bdd exceeds a certain threshold. Using this approach, you can implement an imperfect memory limit for BDD operations. For example, if you suspect that a particular operation might "explode", but you wan't to avoid killing your program because of it, you can first test it with some reasonable size limit (e.g. 2*max(left.size(), right.size())). Also, by setting limit=1, you can implement a very fast test for emptiness of the resulting BDD (even faster than check_binary_op), as the operation will return None as soon as any new BDD node is created.
• Added Bdd::support_set which computes the set of BddVariable objects that actually appear in the decision nodes of the BDD.
• Added Bdd::size_per_variable which computes a map that breaks down how individual BDD variables contribute to the size of the BDD.
• A bugfix and a faster algorithm for computing Bdd::necessary_clause.

0.4.1

This is just a minor release that adds a utility method for computing the most specific conjunctive clause that is satisfied by all BDD valuations.

0.4.0

This release has several new minor performance and quality-of-life improvements. Fortunately, none of them should break any existing code.

High level project changes:

• Updated CI workers to Rust 1.59.0.
• Project now uses Rust edition 2021 instead of 2018.
• We now depend on num-bigint for arbitrary precision integers. This library was chosen because it does not depend on existing C code, so it should be still possible to effortlessly compile lib-bdd to, e.g., web assembly or some other less common target without major issues. However, in the future, we may put this behind a feature flag if desired.
• We now provide Python bindings as part of the biodivine_aeon package available here. In the future, we may also release lib-bdd as a separate library. But for now it is hard to ensure compatibility between objects that are technically the same in Rust, but Python sees them as coming from different libraries. This means we cannot provide Python bindings for multiple interdependent libraries as separate projects, because the objects would be incompatible in Python. So for now we are bundling all our Rust code as part of one Python package.

API changes:

• Added Bdd::restrict and Bdd::var_restrict as convenient shortcuts for select + project operations. In the future, we may consider more performant specialized implementation of this.
• Functions Bdd::write_as_string and Bdd::read_as_string are now public.
• Added Bdd::ternary_op and Bdd::fused_ternary_op as a counterpart to Bdd::binary_op and Bdd::fused_binary_flip_op. These are particularly useful in operations where multiple conditions are involved but the result is expected to be much smaller compared to the intermediate results (or empty). So they do not provide any asymptotic gains, but can reduce the constant factor overhead in many algorithms. Typical usage example is something like repeated evaluation of x = (a & b) & !c (possibly with some variable flips), where at least two arguments change so often that pre-computing either operation does not make sense. These operations are typical for reachability queries in Boolean transition systems.
• We now support exact cardinality computation using num-bigint and Bdd::exact_cardinality. Should work the same as the existing f64 version, just precisely.

0.3.0

This release introduces several minor usability and documentation improvements. A small number of these changes are potentially breaking (marked below), but should be trivial to migrate.

Project changes:

• Migrated from Travis to Github Actions for continuous integration.
• Added a dependency on rand due to the newly introduced features.
• [breaking] Removed the (mostly useless) shields_up feature flag.

New APIs:

• IntoBdd trait which allows conversion of a type to a Bdd assuming BddVariableSet is provided.
• The bdd! macro now supports BddVariable and &str as literals (using the IntoBdd trait) if a BddVariableSet is given as a first argument.
• New generic BddVariableSetBuilder::make allows creating arbitrary number of Bdd variables and binding them to local variables in the same statement.
• BddPartialValuation for representing Bdd clauses.
• BddPathIterator for iterating through Bdd clauses.
• New ValuationsOfClauseIterator replaces BddValuationIterator with a more flexible API.
• Bdd::sat_clauses utility method for creating new path iterators.
• Bdd::is_valuation and Bdd::is_clause checks.
• Bdd::random_valuation, Bdd::random_clause, Bdd::var_pick_random, and Bdd::pick_random for randomly picking BDD representatives.
• Introspection of Bdd valuations and paths using Bdd::first/last_valuation, Bdd::first/last_clause, Bdd::most_positive/negative_valuation, and Bdd::most_fixed/free_clause.
• Added BddVariableSet::mk_conjunctive_clause, BddVariableSet::mk_disjunctive_clause, BddVariableSet::mk_cnf, and BddVariableSet::mk_dnf to simplify creation of CNF/DNF formulas.

Other changes:

• [breaking] BddVariableSet::new and BddVariableSetBuilder::make_variables now accept a slice instead of a Vec.
• Rewrite of BddSatisfyingValuations iterator and related methods to delegate to BddPathIterator and ValuationsOfClauseIterator.
• BddValuationIterator is deprecated in favour of ValuationsOfClauseIterator.
• Added new tutorial modules concerning latest API and advanced usage, plus updated old modules with new idioms.

0.2.1

• Fix a bug where Bdd.cardinality() could cycle forever if the Bdd is big enough (it contains several sub-paths with infinite cardinality).

0.2.0

New features:

• Generalised binary_op and fused_binary_flip_op for implementing advanced custom Bdd operations.
• Added var_project/var_select/var_pick and project/select/pick for working with Bdd as relations (#6).
• Display for Bdd uses default text format.
• BddSatisfyingValuations iterator over all BddValuations that satisfy given Bdd.
• Better API for working with BddValuations (#1 and #7).
• Some small utility methods, like BddVariableSet.mk_literal.

Breaking changes:

• Some &Vec<T> arguments were changed to &[T] as suggested by clippy.

Other changes:

• Stricter CI scripts and git hooks.
• Fix all clippy warnings and errors.

0.1.0

First release! Basic boolean ops, serialisation and boolean expression evaluation.