[Buddy-users] Use of bdd_veccompose

[Jimmy <jim...@an...>]

Hi,

I've recently come across a problem where I'd like to replace some BDD
variables with some formulae (for example, replace variable 0 with "1 OR
2" and variable 2 with "4 OR 7"), and it looks like bdd_veccompose is
the function I want to use. However I can't seem to work out how to use
it.

It takes a bddPair, and from what I can understand a bddPair is strictly
from variables to variables, not from variables to arbitrary BDDs. I
tried playing around with a trivial example to see if I could ignore
this, and add a pair entry from bdd_ithvar(0) to
bdd_or(bdd_ithvar(1),bdd_ithvar(2)), but this complains about unknown
variables. The documentation of bdd_setpairs also seems unclear to me,
taking integers (rather than BDDs) for arguments, but the description
indicating that the arrays can contain BDDs.

Am I on the right track, and if not, what should I be using instead? The
alternative that comes to mind would be replacing the variables with
fresh ones and then doing a series of bdd_compose calls, but this
doesn't sound particularly good.

Thanks,

Jimmy