Module Idds.Idd
Types
type 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.
val manager : ?bdd_mgr:Bdd.manager -> unit -> manager
val get_bdd_manager : manager -> Bdd.manager
Constructors
val ident : t
The identity relation.
val empty : t
The empty relation.
val 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
val 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 }
val 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,x
i:=b
) | x \in B^n }
val branch : manager -> Var.t -> t -> t -> t
branch mgr var hi lo
is the diagram that behaves likehi
whenvar = true
, and likelo
whenvar = false
.