Question

Can somebody provide me rewrite rules for universal quantification(Forall Algo?

Answer 1

For leaf nodes L and any BDDs φ and e (where e is a conjunction of variables), the following holds:

•     Forall(L,φ) = φ
•     Forall(e,L) = L
•     Forall(e,φ) = (xφ ? Forall(e,φ1) : Forall(e,φ0) )  : if D(xφ)>D(xe)
•     Forall(e,φ) = Apply(&,Forall(e1,φ1) : Forall(e1,φ0) ) : if D(xφ)=D(xe)
•     Forall(e,φ) = Forall(e1,φ)  : if D(xφ)=D(xe)

where in the last three cases, we have φ = (xφ ? φ1 : φ0) and e = (xe ? e1 : e0).