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
andBdd::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
andBdd::fused_binary_flip_op_with_limit
methods. These methods execute a standard BDD operation, but safely fail (withNone
) if the number of nodes in the resultingBdd
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 settinglimit=1
, you can implement a very fast test for emptiness of the resulting BDD (even faster thancheck_binary_op
), as the operation will returnNone
as soon as any new BDD node is created. - Added
Bdd::support_set
which computes the set ofBddVariable
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
.