Module Idds.Bdd
Types
type t
= private Dd.t
A BDD is just a DD with two additional structural constraints:
- Ordered: the variables along any root-leaf path of a BDD increase strictly monotonically.
- Reduced: The
hi
andlo
subtrees of any branch are distinct.
val manager : ?dd_mgr:Dd.manager -> unit -> manager
val get_dd_manager : manager -> Dd.manager
Constructors
Boolean operations
val ite : manager -> Var.t -> t -> t -> t
ite mgr i u v
behaves likeu
when variablei
is true, and likev
otherwise.
val test : manager -> Var.t -> bool -> t
test mgr var b
is the diagram that behaves likeb
whenvar = true
and likenot b
whenvar = false
module Make : functor () Boolean.Algebra with type t = t
BDDs form a boolean algebra.