package bddapron

  1. Overview
  2. Docs
type vdd = bool Cudd.Vdd.t
val vdd_of_bdd : Cudd.Bdd.vt -> bool Cudd.Vdd.t
val bdd_of_vdd : bool Cudd.Vdd.t -> Cudd.Bdd.vt
type typ =
  1. | Bool
  2. | Cond
  3. | Other
type info = {
  1. mutable minlevelbool : int;
  2. mutable maxlevelbool : int;
  3. mutable minlevelcond : int;
  4. mutable maxlevelcond : int;
  5. varlevel : int array;
  6. levelvar : int array;
  7. vartyp : typ array;
  8. leveltyp : typ array;
}
val make_info : ('a, 'b, 'c, 'd, 'e) Env.t0 -> ('f, 'g, 'h, 'i) Cond.t -> info
val split_level : Cudd.Bdd.vt -> int -> (Cudd.Bdd.vt * Cudd.Bdd.vt) list
val splitpermutation_of_envcond : ('a, 'b, 'c, 'd, 'e) Env.t0 -> ('f, 'g, 'h, 'i) Cond.t -> [ `BoolCond | `CondBool ] -> int * (int array * int array) option
val split_bdd : ?memo1:Cudd.Memo.t -> ?memo2:Cudd.Memo.t -> (int * (int array * int array) option) -> Cudd.Bdd.vt -> (Cudd.Bdd.vt * Cudd.Bdd.vt) list
val cube_split : ('a, 'b, 'c, 'd) Cond.t -> 'd Cudd.Bdd.t -> 'd Cudd.Bdd.t * 'd Cudd.Bdd.t
val decompose_bdd_boolcond : ('a, 'b, 'c, 'd, 'e) Env.t0 -> ('f, 'g, 'h, 'i) Cond.t -> Cudd.Bdd.vt -> (Cudd.Bdd.vt * Cudd.Bdd.vt) list
val decompose_bdd_condbool : ('a, 'b, 'c, 'd, 'e) Env.t0 -> ('f, 'g, 'h, 'i) Cond.t -> Cudd.Bdd.vt -> (Cudd.Bdd.vt * Cudd.Bdd.vt) list
val decompose_dd_treecondbool : ?careset:'a Cudd.Bdd.t -> topvar:('b -> int) -> support:('b -> 'c Cudd.Bdd.t) -> cofactor:('b -> 'a Cudd.Bdd.t -> 'b) -> ('d, 'e, 'f, 'g, 'h) Env.t0 -> ('i, 'j, 'k, 'a) Cond.t -> 'b -> (int, 'b) Normalform.tree
val decompose_bdd_treecondbool : ('a, 'b, 'c, 'd, 'e) Env.t0 -> ('f, 'g, 'h, 'i) Cond.t -> 'i Cudd.Bdd.t -> (int, 'i Cudd.Bdd.t) Normalform.tree
val decompose_vdd_treecondbool : ?careset:Cudd.Bdd.vt -> ('a, 'b, 'c, 'd, 'e) Env.t0 -> ('f, 'g, 'h, Cudd.Man.v) Cond.t -> 'i Cudd.Vdd.t -> (int, 'i Cudd.Vdd.t) Normalform.tree
val decompose_tbdd_tvdd_treecondbool : ?careset:Cudd.Bdd.vt -> ('a, 'b, 'c, 'd, 'e) Env.t0 -> ('f, 'g, 'h, Cudd.Man.v) Cond.t -> (Cudd.Bdd.vt array * 'i Cudd.Vdd.t array) -> (int, Cudd.Bdd.vt array * 'i Cudd.Vdd.t array) Normalform.tree
val conjunction_of_minterm : ?first:int -> ?last:int -> ((int * bool) -> 'a) -> Cudd.Man.tbool array -> 'a Normalform.conjunction
val dnf_of_bdd : ?first:int -> ?last:int -> ((int * bool) -> 'a) -> 'b Cudd.Bdd.t -> 'a Normalform.dnf
val descend : cudd:'c Cudd.Man.t -> maxdepth:int -> nocare:('a -> bool) -> cube_of_down:('a -> 'c Cudd.Bdd.t) -> cofactor:('a -> 'c Cudd.Bdd.t -> 'a) -> select:('a -> int) -> terminal: (depth:int -> newcube:'c Cudd.Bdd.t -> cube:'c Cudd.Bdd.t -> down:'a -> 'b option) -> ite: (depth:int -> newcube:'c Cudd.Bdd.t -> cond:int -> dthen:'b option -> delse:'b option -> 'b option) -> down:'a -> 'b option
val select_cond : 'd Cudd.Bdd.t -> int
val select_cond_bdd : ('a, 'b, 'c, 'd) Cond.t -> 'd Cudd.Bdd.t -> int
val bdd_support_cond : ('a, 'b, 'c, 'd) Cond.t -> 'd Cudd.Bdd.t -> 'd Cudd.Bdd.t
val vdd_support_cond : ('a, 'b, 'c, Cudd.Man.v) Cond.t -> 'd Cudd.Vdd.t -> Cudd.Bdd.vt
val tbdd_tvdd_support_cond : ('a, 'b, 'c, Cudd.Man.v) Cond.t -> (Cudd.Bdd.vt array * 'd Cudd.Vdd.t array) -> Cudd.Bdd.vt
val tbdd_tvdd_cofactor : (Cudd.Bdd.vt array * 'a Cudd.Vdd.t array) -> Cudd.Bdd.vt -> Cudd.Bdd.vt array * 'a Cudd.Vdd.t array
OCaml

Innovation. Community. Security.