Overload API with Symbolic Sets of Variables

[SSoelvsten]

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.

• [ ] bdd_restrict(f, c) ( using #452 ) Here, there should be an initial check that c is a cube. Otherwise, the restrict from #432 should be used.
• [ ] bdd_exists(f, g) ( using #516 )
• [ ] bdd_forall(f, g) ( using #516 )
• [x] bdd_satmin ( using #665 )
• [x] bdd_satmax (using #665 )

Throw an exception if the second argument is not a BDD cube ( #533 ) .

• [ ] zdd_project(A, D) ( using #516 )
• [ ] zdd_change ( using #532 )
• [ ] zdd_onset ( using #532 )
• [ ] zdd_offset ( using #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.