sig
  type t
  type add = Leaf of float | Ite of int * Cudd.Add.t * Cudd.Add.t
  external manager : Cudd.Add.t -> Cudd.Man.dt = "camlidl_cudd_bdd_manager"
  external is_cst : Cudd.Add.t -> bool = "camlidl_cudd_bdd_is_cst"
  external topvar : Cudd.Add.t -> int = "camlidl_cudd_bdd_topvar"
  external dthen : Cudd.Add.t -> Cudd.Add.t = "camlidl_cudd_add_dthen"
  external delse : Cudd.Add.t -> Cudd.Add.t = "camlidl_cudd_add_delse"
  external dval : Cudd.Add.t -> float = "camlidl_cudd_avdd_dval"
  external cofactors : int -> Cudd.Add.t -> Cudd.Add.t * Cudd.Add.t
    = "camlidl_cudd_add_cofactors"
  external cofactor : Cudd.Add.t -> Cudd.Bdd.dt -> Cudd.Add.t
    = "camlidl_cudd_add_cofactor"
  external inspect : Cudd.Add.t -> Cudd.Add.add = "camlidl_cudd_avdd_inspect"
  external support : Cudd.Add.t -> Cudd.Bdd.dt = "camlidl_cudd_bdd_support"
  external supportsize : Cudd.Add.t -> int = "camlidl_cudd_bdd_supportsize"
  external is_var_in : int -> Cudd.Add.t -> bool
    = "camlidl_cudd_bdd_is_var_in"
  external vectorsupport : Cudd.Add.t array -> Cudd.Bdd.dt
    = "camlidl_cudd_bdd_vectorsupport"
  external vectorsupport2 :
    Cudd.Bdd.dt array -> Cudd.Add.t array -> Cudd.Bdd.dt
    = "camlidl_cudd_add_vectorsupport2"
  external cst : Cudd.Man.dt -> float -> Cudd.Add.t = "camlidl_cudd_avdd_cst"
  val background : Cudd.Man.dt -> Cudd.Add.t
  external ite : Cudd.Bdd.dt -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
    = "camlidl_cudd_add_ite"
  external ite_cst :
    Cudd.Bdd.dt -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t option
    = "camlidl_cudd_add_ite_cst"
  external eval_cst : Cudd.Add.t -> Cudd.Bdd.dt -> Cudd.Add.t option
    = "camlidl_cudd_add_eval_cst"
  external compose : int -> Cudd.Bdd.dt -> Cudd.Add.t -> Cudd.Add.t
    = "camlidl_cudd_add_compose"
  val vectorcompose :
    ?memo:Cudd.Memo.t -> Cudd.Bdd.dt array -> Cudd.Add.t -> Cudd.Add.t
  external varmap : Cudd.Add.t -> Cudd.Add.t = "camlidl_cudd_add_varmap"
  val permute : ?memo:Cudd.Memo.t -> Cudd.Add.t -> int array -> Cudd.Add.t
  external is_equal : Cudd.Add.t -> Cudd.Add.t -> bool
    = "camlidl_cudd_bdd_is_equal"
  external is_equal_when : Cudd.Add.t -> Cudd.Add.t -> Cudd.Bdd.dt -> bool
    = "camlidl_cudd_bdd_is_equal_when"
  external is_eval_cst : Cudd.Add.t -> Cudd.Bdd.dt -> float option
    = "camlidl_cudd_avdd_is_eval_cst"
  external is_ite_cst :
    Cudd.Bdd.dt -> Cudd.Add.t -> Cudd.Add.t -> float option
    = "camlidl_cudd_avdd_is_ite_cst"
  external size : Cudd.Add.t -> int = "camlidl_cudd_bdd_size"
  external nbpaths : Cudd.Add.t -> float = "camlidl_cudd_bdd_nbpaths"
  external nbnonzeropaths : Cudd.Add.t -> float
    = "camlidl_cudd_bdd_nbtruepaths"
  external nbminterms : int -> Cudd.Add.t -> float
    = "camlidl_cudd_bdd_nbminterms"
  external density : int -> Cudd.Add.t -> float = "camlidl_cudd_bdd_density"
  external nbleaves : Cudd.Add.t -> int = "camlidl_cudd_add_nbleaves"
  external iter_cube :
    (Cudd.Man.tbool array -> float -> unit) -> Cudd.Add.t -> unit
    = "camlidl_cudd_avdd_iter_cube"
  external iter_node : (Cudd.Add.t -> unit) -> Cudd.Add.t -> unit
    = "camlidl_cudd_iter_node"
  external guard_of_node : Cudd.Add.t -> Cudd.Add.t -> Cudd.Bdd.dt
    = "camlidl_cudd_add_guard_of_node"
  external guard_of_nonbackground : Cudd.Add.t -> Cudd.Bdd.dt
    = "camlidl_cudd_add_guard_of_nonbackground"
  external nodes_below_level :
    Cudd.Add.t -> int option -> int -> Cudd.Add.t array
    = "camlidl_cudd_avdd_nodes_below_level"
  external guard_of_leaf : Cudd.Add.t -> float -> Cudd.Bdd.dt
    = "camlidl_cudd_avdd_guard_of_leaf"
  external leaves : Cudd.Add.t -> float array = "camlidl_cudd_avdd_leaves"
  external pick_leaf : Cudd.Add.t -> float = "camlidl_cudd_avdd_pick_leaf"
  val guardleafs : Cudd.Add.t -> (Cudd.Bdd.dt * float) array
  external constrain : Cudd.Add.t -> Cudd.Bdd.dt -> Cudd.Add.t
    = "camlidl_cudd_add_constrain"
  external tdconstrain : Cudd.Add.t -> Cudd.Bdd.dt -> Cudd.Add.t
    = "camlidl_cudd_add_tdconstrain"
  external restrict : Cudd.Add.t -> Cudd.Bdd.dt -> Cudd.Add.t
    = "camlidl_cudd_add_restrict"
  external tdrestrict : Cudd.Add.t -> Cudd.Bdd.dt -> Cudd.Add.t
    = "camlidl_cudd_add_tdrestrict"
  external of_bdd : Cudd.Bdd.dt -> Cudd.Add.t = "camlidl_cudd_add_of_bdd"
  external to_bdd : Cudd.Add.t -> Cudd.Bdd.dt = "camlidl_cudd_add_to_bdd"
  external to_bdd_threshold : float -> Cudd.Add.t -> Cudd.Add.t
    = "camlidl_cudd_add_to_bdd_threshold"
  external to_bdd_strictthreshold : float -> Cudd.Add.t -> Cudd.Add.t
    = "camlidl_cudd_add_to_bdd_strictthreshold"
  external to_bdd_interval : float -> float -> Cudd.Add.t -> Cudd.Add.t
    = "camlidl_cudd_add_to_bdd_interval"
  external exist : Cudd.Bdd.dt -> Cudd.Add.t -> Cudd.Add.t
    = "camlidl_cudd_add_exist"
  external forall : Cudd.Bdd.dt -> Cudd.Add.t -> Cudd.Add.t
    = "camlidl_cudd_add_forall"
  external is_leq : Cudd.Add.t -> Cudd.Add.t -> bool
    = "camlidl_cudd_add_is_leq"
  external add : Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
    = "camlidl_cudd_add_add"
  external sub : Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
    = "camlidl_cudd_add_sub"
  external mul : Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
    = "camlidl_cudd_add_mul"
  external div : Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
    = "camlidl_cudd_add_div"
  external min : Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
    = "camlidl_cudd_add_min"
  external max : Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
    = "camlidl_cudd_add_max"
  external agreement : Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
    = "camlidl_cudd_add_agreement"
  external diff : Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
    = "camlidl_cudd_add_diff"
  external threshold : Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
    = "camlidl_cudd_add_threshold"
  external setNZ : Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
    = "camlidl_cudd_add_setNZ"
  external log : Cudd.Add.t -> Cudd.Add.t = "camlidl_cudd_add_log"
  external matrix_multiply :
    int array -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
    = "camlidl_cudd_add_matrix_multiply"
  external times_plus : int array -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
    = "camlidl_cudd_add_times_plus"
  external triangle : int array -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
    = "camlidl_cudd_add_triangle"
  val mapleaf1 :
    default:Cudd.Add.t ->
    (Cudd.Bdd.dt -> float -> float) -> Cudd.Add.t -> Cudd.Add.t
  val mapleaf2 :
    default:Cudd.Add.t ->
    (Cudd.Bdd.dt -> float -> float -> float) ->
    Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
  type op1 = (float, float) Cudd.Custom.op1
  type op2 = (float, float, float) Cudd.Custom.op2
  type op3 = (float, float, float, float) Cudd.Custom.op3
  type opN = {
    commonN : Cudd.Custom.common;
    closureN : Cudd.Bdd.dt array -> Cudd.Add.t array -> Cudd.Add.t option;
    arityNbdd : int;
  }
  type opG = {
    commonG : Cudd.Custom.common;
    arityGbdd : int;
    closureG : Cudd.Bdd.dt array -> Cudd.Add.t array -> Cudd.Add.t option;
    oclosureBeforeRec :
      (int * bool ->
       Cudd.Bdd.dt array ->
       Cudd.Add.t array -> Cudd.Bdd.dt array * Cudd.Add.t array)
      option;
    oclosureIte : (int -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t) option;
  }
  type test2 = (float, float) Cudd.Custom.test2
  type exist = float Cudd.Custom.exist
  type existand = float Cudd.Custom.existand
  type existop1 = (float, float) Cudd.Custom.existop1
  type existandop1 = (float, float) Cudd.Custom.existandop1
  val make_op1 : ?memo:Cudd.Memo.t -> (float -> float) -> Cudd.Add.op1
  val make_op2 :
    ?memo:Cudd.Memo.t ->
    ?commutative:bool ->
    ?idempotent:bool ->
    ?special:(Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t option) ->
    (float -> float -> float) -> Cudd.Add.op2
  val make_op3 :
    ?memo:Cudd.Memo.t ->
    ?special:(Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t option) ->
    (float -> float -> float -> float) -> Cudd.Add.op3
  val make_opN :
    ?memo:Cudd.Memo.t ->
    int ->
    int ->
    (Cudd.Bdd.dt array -> Cudd.Add.t array -> Cudd.Add.t option) ->
    Cudd.Add.opN
  val make_opG :
    ?memo:Cudd.Memo.t ->
    ?beforeRec:(int * bool ->
                Cudd.Bdd.dt array ->
                Cudd.Add.t array -> Cudd.Bdd.dt array * Cudd.Add.t array) ->
    ?ite:(int -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t) ->
    int ->
    int ->
    (Cudd.Bdd.dt array -> Cudd.Add.t array -> Cudd.Add.t option) ->
    Cudd.Add.opG
  val make_test2 :
    ?memo:Cudd.Memo.t ->
    ?symetric:bool ->
    ?reflexive:bool ->
    ?special:(Cudd.Add.t -> Cudd.Add.t -> bool option) ->
    (float -> float -> bool) -> Cudd.Add.test2
  val make_exist : ?memo:Cudd.Memo.t -> Cudd.Add.op2 -> Cudd.Add.exist
  val make_existand :
    ?memo:Cudd.Memo.t -> bottom:float -> Cudd.Add.op2 -> Cudd.Add.existand
  val make_existop1 :
    ?memo:Cudd.Memo.t ->
    op1:Cudd.Add.op1 -> Cudd.Add.op2 -> Cudd.Add.existop1
  val make_existandop1 :
    ?memo:Cudd.Memo.t ->
    op1:Cudd.Add.op1 -> bottom:float -> Cudd.Add.op2 -> Cudd.Add.existandop1
  val clear_op1 : Cudd.Add.op1 -> unit
  val clear_op2 : Cudd.Add.op2 -> unit
  val clear_op3 : Cudd.Add.op3 -> unit
  val clear_opN : Cudd.Add.opN -> unit
  val clear_opG : Cudd.Add.opG -> unit
  val clear_test2 : Cudd.Add.test2 -> unit
  val clear_exist : Cudd.Add.exist -> unit
  val clear_existand : Cudd.Add.existand -> unit
  val clear_existop1 : Cudd.Add.existop1 -> unit
  val clear_existandop1 : Cudd.Add.existandop1 -> unit
  val apply_op1 : Cudd.Add.op1 -> Cudd.Add.t -> Cudd.Add.t
  val apply_op2 : Cudd.Add.op2 -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
  val apply_op3 : Cudd.Add.op3 -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
  val apply_opN :
    Cudd.Add.opN -> Cudd.Bdd.dt array -> Cudd.Add.t array -> Cudd.Add.t
  val apply_opG :
    Cudd.Add.opG -> Cudd.Bdd.dt array -> Cudd.Add.t array -> Cudd.Add.t
  val apply_test2 : Cudd.Add.test2 -> Cudd.Add.t -> Cudd.Add.t -> bool
  val apply_exist :
    Cudd.Add.exist -> supp:Cudd.Bdd.dt -> Cudd.Add.t -> Cudd.Add.t
  val apply_existand :
    Cudd.Add.existand ->
    supp:Cudd.Bdd.dt -> Cudd.Bdd.dt -> Cudd.Add.t -> Cudd.Add.t
  val apply_existop1 :
    Cudd.Add.existop1 -> supp:Cudd.Bdd.dt -> Cudd.Add.t -> Cudd.Add.t
  val apply_existandop1 :
    Cudd.Add.existandop1 ->
    supp:Cudd.Bdd.dt -> Cudd.Bdd.dt -> Cudd.Add.t -> Cudd.Add.t
  val map_op1 :
    ?memo:Cudd.Memo.t -> (float -> float) -> Cudd.Add.t -> Cudd.Add.t
  val map_op2 :
    ?memo:Cudd.Memo.t ->
    ?commutative:bool ->
    ?idempotent:bool ->
    ?special:(Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t option) ->
    (float -> float -> float) -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
  val map_op3 :
    ?memo:Cudd.Memo.t ->
    ?special:(Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t option) ->
    (float -> float -> float -> float) ->
    Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t -> Cudd.Add.t
  val map_opN :
    ?memo:Cudd.Memo.t ->
    (Cudd.Bdd.dt array -> Cudd.Add.t array -> Cudd.Add.t option) ->
    Cudd.Bdd.dt array -> Cudd.Add.t array -> Cudd.Add.t
  val map_test2 :
    ?memo:Cudd.Memo.t ->
    ?symetric:bool ->
    ?reflexive:bool ->
    ?special:(Cudd.Add.t -> Cudd.Add.t -> bool option) ->
    (float -> float -> bool) -> Cudd.Add.t -> Cudd.Add.t -> bool
  external transfer : Cudd.Add.t -> Cudd.Man.d Cudd.Man.t -> Cudd.Add.t
    = "camlidl_cudd_add_transfer"
  external _print : Cudd.Add.t -> unit = "camlidl_cudd_print"
  val print__minterm : Format.formatter -> Cudd.Add.t -> unit
  val print_minterm :
    (Format.formatter -> int -> unit) ->
    (Format.formatter -> float -> unit) ->
    Format.formatter -> Cudd.Add.t -> unit
  val print :
    (Format.formatter -> int -> unit) ->
    (Format.formatter -> float -> unit) ->
    Format.formatter -> Cudd.Add.t -> unit
end