In most BDD packages, the quantification algorithm takes the domain also as a symbolic representation, i.e. as another BDD/ZDD. This is quite simple, since we already have the generators in the API ( #147 ). What we merely have to do is to wrap a level_info_stream that pulls bottom-up into a generator function and then passes it further along.
Throw an exception if the second argument is not a BDD cube ( #533 ) .
Throw an exception if the second argument is not a ZDD point ( #571 ).
Of course, remember a few unit tests to check it truly works as intended - including the exceptions.
In most BDD packages, the quantification algorithm takes the domain also as a symbolic representation, i.e. as another BDD/ZDD. This is quite simple, since we already have the generators in the API ( #147 ). What we merely have to do is to wrap a
level_info_streamthat pulls bottom-up into a generator function and then passes it further along.bdd_restrict(f, c)( using Generalise API to use Assignment Functions / Generators #452 )Here, there should be an initial check that
cis a cube. Otherwise, the restrict from Coudert's and Madre's BDD functions #432 should be used.bdd_exists(f, g)( using Add Generator Function and Iterators to Quantify Algorithms #516 )bdd_forall(f, g)( using Add Generator Function and Iterators to Quantify Algorithms #516 )bdd_satmin( using Add Domain tobdd_satmin,bdd_satmax, ... #665 )bdd_satmax(using Add Domain tobdd_satmin,bdd_satmax, ... #665 )Throw an exception if the second argument is not a BDD cube ( #533 ) .
zdd_project(A, D)( using Add Generator Function and Iterators to Quantify Algorithms #516 )zdd_change( using Generalise API to use Label Generators / Iterators #532 )zdd_onset( using Generalise API to use Label Generators / Iterators #532 )zdd_offset( using Generalise API to use Label Generators / Iterators #532 )Throw an exception if the second argument is not a ZDD point ( #571 ).
Of course, remember a few unit tests to check it truly works as intended - including the exceptions.