We use Lazy BDDS: ternary trees (instead of binary) where the additional node encodes a lazy union, as in "COVARIANCE AND CONTRAVARIANCE: A FRESH LOOK AT AN OLD ISSUE", with some additional optimisations for intersections and differences to avoid materialising unions.