SE547: BDDs: Binary Decision Diagrams [11/22]

Binary Decision Diagrams are a graphical representation of the grammar:

s, t, u ::=
    0
    1
    x t, u

A couple of improvements to Binary Decision Diagrams:

a) What should we do about x t, t? [Reduced BDDs.]

b) There are two representations of x y: what are they? What should we do about this? [Ordered BDDs.]