sig
  type leaf = Arith.expr
  type t
  type id_unop
  type id_binop
  type id_combinop
  type mtbdd = Leaf of leaf | Ite of int * t * t
  val leafbackground : leaf
  module Hash :
    sig
      type key = leaf
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val length : 'a t -> int
    end
  val hasht : int Hash.t
  module Assoc :
    sig
      type key = int
      type +'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val add : key -> 'a -> 'a t -> 'a t
      val find : key -> 'a t -> 'a
      val remove : key -> 'a t -> 'a t
      val mem : key -> 'a t -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val map : ('a -> 'b) -> 'a t -> 'b t
      val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
      val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
    end
  val assoct : leaf Assoc.t ref
  val leaf_of_id : int -> leaf
  val id_of_leaf : leaf -> int
  val remove_leaf : leaf -> unit
  val iter_leaf : (int -> leaf -> unit) -> unit
  external to_idd : t -> Idd.t = "%identity"
  external of_idd : Idd.t -> t = "%identity"
  external manager : t -> Manager.t = "camlidl_cudd_bdd_manager"
  external is_cst : t -> bool = "camlidl_cudd_bdd_is_cst"
  external topvar : t -> int = "camlidl_cudd_bdd_topvar"
  external dthen : t -> t = "camlidl_cudd_rdd_dthen"
  external delse : t -> t = "camlidl_cudd_rdd_delse"
  external cofactors : int -> t -> t * t = "camlidl_cudd_rdd_cofactors"
  external cofactor : t -> Bdd.t -> t = "camlidl_cudd_rdd_cofactor"
  val dval : t -> leaf
  val inspect : t -> mtbdd
  external support : t -> Bdd.t = "camlidl_cudd_bdd_support"
  external supportsize : t -> int = "camlidl_cudd_bdd_supportsize"
  external is_var_in : int -> t -> bool = "camlidl_cudd_bdd_is_var_in"
  external vectorsupport : t array -> Bdd.t
    = "camlidl_cudd_bdd_vectorsupport"
  external vectorsupport2 : Bdd.t array -> t array -> Bdd.t
    = "camlidl_cudd_rdd_vectorsupport2"
  val cst : Manager.t -> leaf -> t
  external ite : Bdd.t -> t -> t -> t = "camlidl_cudd_rdd_ite"
  external compose : int -> Bdd.t -> t -> t = "camlidl_cudd_rdd_compose"
  external vectorcompose : Bdd.t array -> t -> t
    = "camlidl_cudd_rdd_vectorcompose"
  external is_equal : t -> t -> bool = "camlidl_cudd_bdd_is_equal"
  external is_equal_when : t -> t -> Bdd.t -> bool
    = "camlidl_cudd_bdd_is_equal_when"
  val is_eval_cst : t -> Bdd.t -> leaf option
  val is_ite_cst : Bdd.t -> t -> t -> leaf option
  external size : t -> int = "camlidl_cudd_bdd_size"
  external nbpaths : t -> float = "camlidl_cudd_bdd_nbpaths"
  external nbnonzeropaths : t -> float = "camlidl_cudd_rdd_nbnonzeropaths"
  external nbminterms : int -> t -> float = "camlidl_cudd_bdd_nbminterms"
  external density : int -> t -> float = "camlidl_cudd_bdd_density"
  external nbleaves : t -> int = "camlidl_cudd_rdd_nbleaves"
  external varmap : t -> t = "camlidl_cudd_rdd_varmap"
  external permute : int array -> t -> t = "camlidl_cudd_rdd_permute"
  external iter_node : (t -> unit) -> t -> unit = "camlidl_cudd_iter_node"
  val iter_cube : (Manager.tbool array -> leaf -> unit) -> t -> unit
  external guard_of_node : t -> t -> Bdd.t = "camlidl_cudd_rdd_guard_of_node"
  external guard_of_nonbackground : t -> Bdd.t
    = "camlidl_cudd_rdd_guard_of_nonbackground"
  external nodes_below_level : t -> int option -> t array
    = "camlidl_cudd_rdd_nodes_below_level"
  val leaves : t -> leaf array
  val guard_of_leaf : t -> leaf -> Bdd.t
  val guardleafs : t -> (Bdd.t * leaf) array
  external constrain : t -> Bdd.t -> t = "camlidl_cudd_rdd_constrain"
  external tdconstrain : t -> Bdd.t -> t = "camlidl_cudd_rdd_tdconstrain"
  external restrict : t -> Bdd.t -> t = "camlidl_cudd_rdd_restrict"
  external tdrestrict : t -> Bdd.t -> t = "camlidl_cudd_rdd_tdrestrict"
  external to_bdd : t -> Bdd.t = "camlidl_cudd_rdd_to_bdd"
  val alloc_unop : (leaf -> leaf) -> id_unop
  val alloc_binop : (leaf -> leaf -> leaf) -> id_binop
  val alloc_combinop : (leaf -> leaf -> leaf) -> id_combinop
  external apply_unop : id_unop -> t -> t = "camlidl_cudd_idd_apply_unop"
  external apply_binop : id_binop -> t -> t -> t
    = "camlidl_cudd_idd_apply_binop"
  external apply_combinop : id_combinop -> t -> t -> t
    = "camlidl_cudd_idd_apply_combinop"
  external transfer : t -> Manager.t -> t = "camlidl_cudd_rdd_transfer"
  external _print : t -> unit = "camlidl_cudd_print"
  val print__minterm : Format.formatter -> t -> unit
  val print_minterm :
    (int -> string) -> (leaf -> string) -> Format.formatter -> t -> unit
  val print :
    (int -> string) -> (leaf -> string) -> Format.formatter -> t -> unit
end