sig
  type 'a unique
  type 'a t = 'Cudd.Mtbdd.unique Cudd.Vdd.t
  type 'a table = 'Cudd.Mtbdd.unique Cudd.PWeakke.t
  val print_table :
    ?first:(unit, Format.formatter, unit) Pervasives.format ->
    ?sep:(unit, Format.formatter, unit) Pervasives.format ->
    ?last:(unit, Format.formatter, unit) Pervasives.format ->
    (Format.formatter -> '-> unit) ->
    Format.formatter -> 'Cudd.Mtbdd.table -> unit
  val make_table :
    hash:('-> int) -> equal:('-> '-> bool) -> 'Cudd.Mtbdd.table
  val unique : 'Cudd.Mtbdd.table -> '-> 'Cudd.Mtbdd.unique
  val get : 'Cudd.Mtbdd.unique -> 'a
  type 'a mtbdd =
      Leaf of 'Cudd.Mtbdd.unique
    | Ite of int * 'Cudd.Mtbdd.t * 'Cudd.Mtbdd.t
  external manager : 'Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Man.t
    = "camlidl_cudd_bdd_manager"
  external is_cst : 'Cudd.Mtbdd.t -> bool = "camlidl_cudd_bdd_is_cst"
  external topvar : 'Cudd.Mtbdd.t -> int = "camlidl_cudd_bdd_topvar"
  external dthen : 'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.t
    = "camlidl_cudd_add_dthen"
  external delse : 'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.t
    = "camlidl_cudd_add_delse"
  external cofactors :
    int -> 'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.t * 'Cudd.Mtbdd.t
    = "camlidl_cudd_add_cofactors"
  external cofactor :
    'Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'Cudd.Mtbdd.t
    = "camlidl_cudd_add_cofactor"
  val dval_u : 'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.unique
  val dval : 'Cudd.Mtbdd.t -> 'a
  val inspect : 'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.mtbdd
  external support : 'Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t
    = "camlidl_cudd_bdd_support"
  external supportsize : 'Cudd.Mtbdd.t -> int
    = "camlidl_cudd_bdd_supportsize"
  external is_var_in : int -> 'Cudd.Mtbdd.t -> bool
    = "camlidl_cudd_bdd_is_var_in"
  external vectorsupport : 'Cudd.Mtbdd.t array -> Cudd.Man.v Cudd.Bdd.t
    = "camlidl_cudd_bdd_vectorsupport"
  external vectorsupport2 :
    Cudd.Man.v Cudd.Bdd.t array ->
    'Cudd.Mtbdd.t array -> Cudd.Man.v Cudd.Bdd.t
    = "camlidl_cudd_add_vectorsupport2"
  val cst_u :
    Cudd.Man.v Cudd.Man.t -> 'Cudd.Mtbdd.unique -> 'Cudd.Mtbdd.t
  val cst :
    Cudd.Man.v Cudd.Man.t -> 'Cudd.Mtbdd.table -> '-> 'Cudd.Mtbdd.t
  external ite :
    Cudd.Man.v Cudd.Bdd.t ->
    'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.t
    = "camlidl_cudd_add_ite"
  external ite_cst :
    Cudd.Man.v Cudd.Bdd.t ->
    'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.t option
    = "camlidl_cudd_add_ite_cst"
  external eval_cst :
    'Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'Cudd.Mtbdd.t option
    = "camlidl_cudd_add_eval_cst"
  external compose :
    int -> Cudd.Man.v Cudd.Bdd.t -> 'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.t
    = "camlidl_cudd_add_compose"
  val vectorcompose :
    ?memo:Cudd.Memo.t ->
    Cudd.Man.v Cudd.Bdd.t array -> 'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.t
  external is_equal : 'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.t -> bool
    = "camlidl_cudd_bdd_is_equal"
  external is_equal_when :
    'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> bool
    = "camlidl_cudd_bdd_is_equal_when"
  val is_eval_cst_u :
    'Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'Cudd.Mtbdd.unique option
  val is_ite_cst_u :
    Cudd.Man.v Cudd.Bdd.t ->
    'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.unique option
  val is_eval_cst : 'Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a option
  val is_ite_cst :
    Cudd.Man.v Cudd.Bdd.t -> 'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.t -> 'a option
  external size : 'Cudd.Mtbdd.t -> int = "camlidl_cudd_bdd_size"
  external nbpaths : 'Cudd.Mtbdd.t -> float = "camlidl_cudd_bdd_nbpaths"
  external nbnonzeropaths : 'Cudd.Mtbdd.t -> float
    = "camlidl_cudd_bdd_nbtruepaths"
  external nbminterms : int -> 'Cudd.Mtbdd.t -> float
    = "camlidl_cudd_bdd_nbminterms"
  external density : int -> 'Cudd.Mtbdd.t -> float
    = "camlidl_cudd_bdd_density"
  external nbleaves : 'Cudd.Mtbdd.t -> int = "camlidl_cudd_add_nbleaves"
  external varmap : 'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.t
    = "camlidl_cudd_add_varmap"
  val permute :
    ?memo:Cudd.Memo.t -> 'Cudd.Mtbdd.t -> int array -> 'Cudd.Mtbdd.t
  val iter_cube_u :
    (Cudd.Man.tbool array -> 'Cudd.Mtbdd.unique -> unit) ->
    'Cudd.Mtbdd.t -> unit
  val iter_cube :
    (Cudd.Man.tbool array -> '-> unit) -> 'Cudd.Mtbdd.t -> unit
  external iter_node : ('Cudd.Mtbdd.t -> unit) -> 'Cudd.Mtbdd.t -> unit
    = "camlidl_cudd_iter_node"
  external guard_of_node :
    'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t
    = "camlidl_cudd_add_guard_of_node"
  external guard_of_nonbackground : 'Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t
    = "camlidl_cudd_add_guard_of_nonbackground"
  val nodes_below_level :
    ?max:int -> 'Cudd.Mtbdd.t -> int option -> 'Cudd.Mtbdd.t array
  val guard_of_leaf_u :
    'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.unique -> Cudd.Man.v Cudd.Bdd.t
  val guard_of_leaf :
    'Cudd.Mtbdd.table -> 'Cudd.Mtbdd.t -> '-> Cudd.Man.v Cudd.Bdd.t
  val leaves_u : 'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.unique array
  val leaves : 'Cudd.Mtbdd.t -> 'a array
  val pick_leaf_u : 'Cudd.Mtbdd.t -> 'Cudd.Mtbdd.unique
  val pick_leaf : 'Cudd.Mtbdd.t -> 'a
  val guardleafs_u :
    'Cudd.Mtbdd.t -> (Cudd.Man.v Cudd.Bdd.t * 'Cudd.Mtbdd.unique) array
  val guardleafs : 'Cudd.Mtbdd.t -> (Cudd.Man.v Cudd.Bdd.t * 'a) array
  external constrain :
    'Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'Cudd.Mtbdd.t
    = "camlidl_cudd_add_constrain"
  external tdconstrain :
    'Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'Cudd.Mtbdd.t
    = "camlidl_cudd_add_tdconstrain"
  external restrict :
    'Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'Cudd.Mtbdd.t
    = "camlidl_cudd_add_restrict"
  external tdrestrict :
    'Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'Cudd.Mtbdd.t
    = "camlidl_cudd_add_tdrestrict"
  external transfer :
    'Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Man.t -> 'Cudd.Mtbdd.t
    = "camlidl_cudd_add_transfer"
  val print__minterm :
    (Format.formatter -> '-> unit) ->
    Format.formatter -> 'Cudd.Mtbdd.t -> unit
  val print_minterm :
    (Format.formatter -> int -> unit) ->
    (Format.formatter -> '-> unit) ->
    Format.formatter -> 'Cudd.Mtbdd.t -> unit
  val print :
    (Format.formatter -> Cudd.Man.v Cudd.Bdd.t -> unit) ->
    (Format.formatter -> '-> unit) ->
    Format.formatter -> 'Cudd.Mtbdd.t -> unit
end