Module Katbb_lib.Idd_compiler
Compilation
val compile_bexp : mgr:Idds.Bdd.manager -> map_var:(string -> int) -> Ast.bexp -> Idds.Bdd.t
compile_bexp ~mgr ~map_var bexp
is the BDD representingbexp
wheremap_var
maps test names to their respective DD variable indices;map_var
is required to be injective (or else the result is undefined).
val compile_exp : mgr:Idds.Idd.manager -> map_var:(string -> int) -> Ast.exp -> Idds.Idd.t
compile_exp ~mgr ~map_var exp
is the IDD representingexp
wheremap_var
maps test names to their respective DD variable indices;map_var
is required to be injective (or else the result is undefined).
Algebraic structures used for compilation
val bdd_ba : Idds.Bdd.manager -> Idds.Bdd.t Kat.Hom.ba
BDDs form a Boolean algebra.
val idd_kat : Idds.Idd.manager -> (Idds.Idd.t, Idds.Bdd.t) Kat.Hom.kat
IDDs form a KAT.