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 representing bexp where map_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 representing exp where map_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.