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 usingBdd::ternary_op
. - Adds new "low level" apply operators:
Bdd::binary_op_with_exists
,Bdd::binary_op_with_for_all
andBdd::binary_op_nested
(which is a generalisation of theexists
andfor_all
variants). - Deprecates
Bdd::var_project
andBdd::project
in favour ofBdd::var_exists
andBdd::exists
. - Adds
Bdd::var_for_all
andBdd::for_all
. - New faster implementations for
Bdd::exists
,Bdd::for_all
andBdd::restrict
based on the new apply operators. - Adds
Bdd::to_cnf
andBdd::to_dnf
. - New faster implementations for
BddVariableSet::mk_cnf
andBddVariableSet::mk_dnf
. - Adds unsafe
Bdd::set_num_vars
andBdd::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
andBddVariableSet::mk_sat_exactly_k
for building BDDs that are satisfied for valuations with up to/exactlyk
valid literals. BddVariableSetBuilder
is now clone-able. Because why even wasn't it before?