sig
  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 : Bdd.Decompose.typ array;
    leveltyp : Bdd.Decompose.typ array;
  }
  val make_info :
    ('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
    ('f, 'g, 'h, 'i) Bdd.Cond.t -> Bdd.Decompose.info
  val split_level : Cudd.Bdd.vt -> int -> (Cudd.Bdd.vt * Cudd.Bdd.vt) list
  val splitpermutation_of_envcond :
    ('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
    ('f, 'g, 'h, 'i) Bdd.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) Bdd.Cond.t ->
    'd Cudd.Bdd.t -> 'd Cudd.Bdd.t * 'd Cudd.Bdd.t
  val decompose_bdd_boolcond :
    ('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
    ('f, 'g, 'h, 'i) Bdd.Cond.t ->
    Cudd.Bdd.vt -> (Cudd.Bdd.vt * Cudd.Bdd.vt) list
  val decompose_bdd_condbool :
    ('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
    ('f, 'g, 'h, 'i) Bdd.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) Bdd.Env.t0 ->
    ('i, 'j, 'k, 'a) Bdd.Cond.t -> 'b -> (int, 'b) Bdd.Normalform.tree
  val decompose_bdd_treecondbool :
    ('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
    ('f, 'g, 'h, 'i) Bdd.Cond.t ->
    'i Cudd.Bdd.t -> (int, 'i Cudd.Bdd.t) Bdd.Normalform.tree
  val decompose_vdd_treecondbool :
    ?careset:Cudd.Bdd.vt ->
    ('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
    ('f, 'g, 'h, Cudd.Man.v) Bdd.Cond.t ->
    'i Cudd.Vdd.t -> (int, 'i Cudd.Vdd.t) Bdd.Normalform.tree
  val decompose_tbdd_tvdd_treecondbool :
    ?careset:Cudd.Bdd.vt ->
    ('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
    ('f, 'g, 'h, Cudd.Man.v) Bdd.Cond.t ->
    Cudd.Bdd.vt array * 'i Cudd.Vdd.t array ->
    (int, Cudd.Bdd.vt array * 'i Cudd.Vdd.t array) Bdd.Normalform.tree
  val conjunction_of_minterm :
    ?first:int ->
    ?last:int ->
    (int * bool -> 'a) ->
    Cudd.Man.tbool array -> 'a Bdd.Normalform.conjunction
  val dnf_of_bdd :
    ?first:int ->
    ?last:int -> (int * bool -> 'a) -> 'b Cudd.Bdd.t -> 'a Bdd.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) Bdd.Cond.t -> 'd Cudd.Bdd.t -> int
  val bdd_support_cond :
    ('a, 'b, 'c, 'd) Bdd.Cond.t -> 'd Cudd.Bdd.t -> 'd Cudd.Bdd.t
  val vdd_support_cond :
    ('a, 'b, 'c, Cudd.Man.v) Bdd.Cond.t -> 'd Cudd.Vdd.t -> Cudd.Bdd.vt
  val tbdd_tvdd_support_cond :
    ('a, 'b, 'c, Cudd.Man.v) Bdd.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
end