Apply operation and unique quantification. Applies the binary operator opr to the arguments l and r and then performs a unique 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_appuni function much more efficient than an apply operation followed by a quantification.
|