bdd_appex

BDD bdd_appex ( BDD  l, BDD  r, int  opr, BDD  var   ) Apply operation and existential quantification. Applies the binary operator opr to the arguments l and r and then performs an existential quantification of the variables from the variable set var. This is done in a bottom up manner such that both the apply and quantification is done on the lower nodes before stepping up to the higher nodes. This makes the bdd_appex function much more efficient than an apply operation followed by a quantification. If the operator is a conjunction then this is similar to the relational product of the two BDDs. See also: bdd_appall, bdd_appuni, bdd_apply, bdd_exist, bdd_forall, bdd_unique, bdd_makeset Returns: The result of the operation.

---