An IDD is just a DD with two additional structural constraints that ensure canonicity: two IDDs encode the same function iff they are the same IDD.

The identity relation.

The empty relation.

For i < n, eval (test i b) env n = env (Var.inp i) = b && eval ident env n rel n (test i b) = { (x,x) | x \in B^n, x_i = b }

For i < n, eval (set i b) env n = eval ident env' n, where env' x = if x = Var.inp i then b else env x rel n (set i b) = { (x,xi:=b) | x \in B^n }

branch mgr var hi lo is the diagram that behaves like hi when var = true, and like lo when var = false.

apply mgr op t0 t1 is t such that Bool.equal (op (eval t0 env n) (eval t1 env n)) (eval t env n)

Sequential composition

(Relational) union

(Relational) transitive-reflexive closure

O(1) structural equality.

PRECONDITION: The result of equal u v is only defined when u and v were built using the same manager. Otherwise, the result is arbitrary.

relational containment

eval tree env n evaluates idd tree in environment env where the variable indices are 0,...,n-1