This pull request introduces the apply_{forall,exist,unique} functions for BooleanFunctionQuant, which computes apply followed by quantification.
Introduced BooleanOperator to specify the operation to apply.
Added the default implementation for all DD variants.
Implemented a specialized variant, both single and multi-threaded, of the apply_quant for BDDs.
Added tests for the introduced functions. The single threaded variant requires multi-threaded to be removed from the default features of oxidd to run the tests.
This should not strictly belong in this pull request, but when trying to do some benchmarking it turned out that the NoApplyCache variant did not compile.
TODO:
[x] Extend the interfaces for Python and C++ .
[ ] There are no benchmarks added to show that the implemented procedure is actually more optimal than the naive version. This could be considered future work.
This pull request introduces the
apply_{forall,exist,unique}functions forBooleanFunctionQuant, which computes apply followed by quantification.BooleanOperatorto specify the operation to apply.multi-threadedto be removed from the default features of oxidd to run the tests.NoApplyCachevariant did not compile.TODO: