Overload API with Symbolic Sets of Variables
SSoelvsten opened this issue · 0 comments
SSoelvsten commented
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 thatc
is a cube. Otherwise, the restrict from #432 should be used. -
bdd_exists(f, g)
( using #516 ) -
bdd_forall(f, g)
( using #516 ) -
bdd_satmin
( using #665 ) -
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.