BuDDy: bdd_veccompose

BDD bdd_veccompose	(	BDD	g,
		bddPair *	pair
	)

Simultaneous functional composition.

Uses the pairs of variables and BDDs in pair to make the simultaneous substitution: $[g_1/V_1, \ldots, g_n/V_n]$ . In this way one or more BDDs may be substituted in one step. The BDDs in pair may depend on the variables they are substituting. bdd_compose may be used instead of bdd_replace but is not as efficient when $g_i$ is a single variable, the same applies to bdd_restrict. Note that simultaneous substitution is not necessarily the same as repeated substitution. Example:

$(x_1 \lor x_2)[x_3/x_1,x_4/x_3] = (x_3 \lor x_2) \neq ((x_1 \lor x_2)[x_3/x_1])[x_4/x_3] = (x_4 \lor x_2)$

Returns:: The composed BDD.

See also:: bdd_compose, bdd_replace, bdd_restrict