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 of2018
. - 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 compilelib-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 releaselib-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
andBdd::var_restrict
as convenient shortcuts forselect + project
operations. In the future, we may consider more performant specialized implementation of this. - Functions
Bdd::write_as_string
andBdd::read_as_string
are now public. - Added
Bdd::ternary_op
andBdd::fused_ternary_op
as a counterpart toBdd::binary_op
andBdd::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 ofx = (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
andBdd::exact_cardinality
. Should work the same as the existingf64
version, just precisely.