bddapron 2.3.2 · OCaml Package

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 =

| Bool
| Cond
| Other

type info = {

mutable minlevelbool : int;
mutable maxlevelbool : int;
mutable minlevelcond : int;
mutable maxlevelcond : int;
varlevel : int array;
levelvar : int array;
vartyp : typ array;
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

package bddapron