sig
  type +'a t
  type 'a vdd = Leaf of '| Ite of int * 'Cudd.Vdd.t * 'Cudd.Vdd.t
  external manager : 'Cudd.Vdd.t -> Cudd.Man.v Cudd.Man.t
    = "camlidl_cudd_bdd_manager"
  external is_cst : 'Cudd.Vdd.t -> bool = "camlidl_cudd_bdd_is_cst"
  external topvar : 'Cudd.Vdd.t -> int = "camlidl_cudd_bdd_topvar"
  external dthen : 'Cudd.Vdd.t -> 'Cudd.Vdd.t = "camlidl_cudd_add_dthen"
  external delse : 'Cudd.Vdd.t -> 'Cudd.Vdd.t = "camlidl_cudd_add_delse"
  external cofactors : int -> 'Cudd.Vdd.t -> 'Cudd.Vdd.t * 'Cudd.Vdd.t
    = "camlidl_cudd_add_cofactors"
  external cofactor : 'Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'Cudd.Vdd.t
    = "camlidl_cudd_add_cofactor"
  external dval : 'Cudd.Vdd.t -> 'a = "camlidl_cudd_avdd_dval"
  external inspect : 'Cudd.Vdd.t -> 'Cudd.Vdd.vdd
    = "camlidl_cudd_avdd_inspect"
  external support : 'Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t
    = "camlidl_cudd_bdd_support"
  external supportsize : 'Cudd.Vdd.t -> int
    = "camlidl_cudd_bdd_supportsize"
  external is_var_in : int -> 'Cudd.Vdd.t -> bool
    = "camlidl_cudd_bdd_is_var_in"
  external vectorsupport : 'Cudd.Vdd.t array -> Cudd.Man.v Cudd.Bdd.t
    = "camlidl_cudd_bdd_vectorsupport"
  external vectorsupport2 :
    Cudd.Man.v Cudd.Bdd.t array ->
    'Cudd.Vdd.t array -> Cudd.Man.v Cudd.Bdd.t
    = "camlidl_cudd_add_vectorsupport2"
  external cst : Cudd.Man.v Cudd.Man.t -> '-> 'Cudd.Vdd.t
    = "camlidl_cudd_avdd_cst"
  val _background : Cudd.Man.v Cudd.Man.t -> 'Cudd.Vdd.t
  external ite :
    Cudd.Man.v Cudd.Bdd.t -> 'Cudd.Vdd.t -> 'Cudd.Vdd.t -> 'Cudd.Vdd.t
    = "camlidl_cudd_add_ite"
  external ite_cst :
    Cudd.Man.v Cudd.Bdd.t ->
    'Cudd.Vdd.t -> 'Cudd.Vdd.t -> 'Cudd.Vdd.t option
    = "camlidl_cudd_add_ite_cst"
  external eval_cst :
    'Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'Cudd.Vdd.t option
    = "camlidl_cudd_add_eval_cst"
  external compose : int -> Cudd.Bdd.vt -> 'Cudd.Vdd.t -> 'Cudd.Vdd.t
    = "camlidl_cudd_add_compose"
  val vectorcompose :
    ?memo:Cudd.Memo.t -> Cudd.Bdd.vt array -> 'Cudd.Vdd.t -> 'Cudd.Vdd.t
  external is_equal : 'Cudd.Vdd.t -> 'Cudd.Vdd.t -> bool
    = "camlidl_cudd_bdd_is_equal"
  external is_equal_when :
    'Cudd.Vdd.t -> 'Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> bool
    = "camlidl_cudd_bdd_is_equal_when"
  external is_eval_cst : 'Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a option
    = "camlidl_cudd_avdd_is_eval_cst"
  external is_ite_cst :
    Cudd.Man.v Cudd.Bdd.t -> 'Cudd.Vdd.t -> 'Cudd.Vdd.t -> 'a option
    = "camlidl_cudd_avdd_is_ite_cst"
  external size : 'Cudd.Vdd.t -> int = "camlidl_cudd_bdd_size"
  external nbpaths : 'Cudd.Vdd.t -> float = "camlidl_cudd_bdd_nbpaths"
  external nbnonzeropaths : 'Cudd.Vdd.t -> float
    = "camlidl_cudd_bdd_nbtruepaths"
  external nbminterms : int -> 'Cudd.Vdd.t -> float
    = "camlidl_cudd_bdd_nbminterms"
  external density : int -> 'Cudd.Vdd.t -> float
    = "camlidl_cudd_bdd_density"
  external nbleaves : 'Cudd.Vdd.t -> int = "camlidl_cudd_add_nbleaves"
  external varmap : 'Cudd.Vdd.t -> 'Cudd.Vdd.t
    = "camlidl_cudd_add_varmap"
  val permute :
    ?memo:Cudd.Memo.t -> 'Cudd.Vdd.t -> int array -> 'Cudd.Vdd.t
  external iter_cube :
    (Cudd.Man.tbool array -> '-> unit) -> 'Cudd.Vdd.t -> unit
    = "camlidl_cudd_avdd_iter_cube"
  external iter_node : ('Cudd.Vdd.t -> unit) -> 'Cudd.Vdd.t -> unit
    = "camlidl_cudd_iter_node"
  external guard_of_node :
    'Cudd.Vdd.t -> 'Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t
    = "camlidl_cudd_add_guard_of_node"
  external guard_of_nonbackground : 'Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t
    = "camlidl_cudd_add_guard_of_nonbackground"
  val nodes_below_level :
    ?max:int -> 'Cudd.Vdd.t -> int option -> 'Cudd.Vdd.t array
  external guard_of_leaf : 'Cudd.Vdd.t -> '-> Cudd.Man.v Cudd.Bdd.t
    = "camlidl_cudd_avdd_guard_of_leaf"
  external leaves : 'Cudd.Vdd.t -> 'a array = "camlidl_cudd_avdd_leaves"
  external pick_leaf : 'Cudd.Vdd.t -> 'a = "camlidl_cudd_avdd_pick_leaf"
  val guardleafs : 'Cudd.Vdd.t -> (Cudd.Man.v Cudd.Bdd.t * 'a) array
  external constrain :
    'Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'Cudd.Vdd.t
    = "camlidl_cudd_add_constrain"
  external tdconstrain :
    'Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'Cudd.Vdd.t
    = "camlidl_cudd_add_tdconstrain"
  external restrict : 'Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'Cudd.Vdd.t
    = "camlidl_cudd_add_restrict"
  external tdrestrict :
    'Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'Cudd.Vdd.t
    = "camlidl_cudd_add_tdrestrict"
  external transfer : 'Cudd.Vdd.t -> Cudd.Man.v Cudd.Man.t -> 'Cudd.Vdd.t
    = "camlidl_cudd_add_transfer"
  val print__minterm :
    (Format.formatter -> '-> unit) ->
    Format.formatter -> 'Cudd.Vdd.t -> unit
  val print_minterm :
    (Format.formatter -> int -> unit) ->
    (Format.formatter -> '-> unit) ->
    Format.formatter -> 'Cudd.Vdd.t -> unit
  val print :
    (Format.formatter -> Cudd.Man.v Cudd.Bdd.t -> unit) ->
    (Format.formatter -> '-> unit) ->
    Format.formatter -> 'Cudd.Vdd.t -> unit
end