Module `Idds.Idd`Source

Identity Suppressed Decision Diagrams (IDDs).

Sourcetype t = private Dd.t

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.

Sourcetype manager

Sourceval manager : ?bdd_mgr:Bdd.manager -> unit -> manager

Sourceval get_bdd_manager : manager -> Bdd.manager

Sourceval ident : t

The identity relation.

Sourceval empty : t

The empty relation.

Sourceval of_bdd : Bdd.t -> t

if bdd contains no output variables then Bdd.eval bdd ~env = Idd.(eval (of_bdd bdd) ~env); otherwise, behavior is undefined

Sourceval test : manager -> int -> bool -> t

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 }

Sourceval set : manager -> int -> bool -> t

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 }

Sourceval branch : manager -> Var.t -> t -> t -> t

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

Sourceval apply : manager -> (bool -> bool -> bool) -> t -> t -> t

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

Sourceval seq : manager -> t -> t -> t

Sequential composition

Sourceval union : manager -> t -> t -> t

(Relational) union

Sourceval star : manager -> t -> t

(Relational) transitive-reflexive closure

Sourceval equal : t -> t -> bool

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.

Sourceval subseteq : manager -> t -> t -> bool

relational containment

Sourceval eval : t -> (Var.t -> bool) -> int -> bool

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

package idds