sig
  module Hash :
    sig
      type t
      external _create : int -> int -> Cudd.Hash.t
        = "camlidl_cudd_hash__create"
      val table : Cudd.Hash.t Weak.t Pervasives.ref
      val create : ?size:int -> int -> Cudd.Hash.t
      external arity : Cudd.Hash.t -> int = "camlidl_cudd_hash_arity"
      external clear : Cudd.Hash.t -> unit = "camlidl_cudd_hash_clear"
      val clear_all : unit -> unit
    end
  module Cache :
    sig
      type t
      external _create : int -> int -> int -> Cudd.Cache.t
        = "camlidl_cudd_cache__create"
      val create : ?size:int -> ?maxsize:int -> arity:int -> Cudd.Cache.t
      val create1 : ?size:int -> ?maxsize:int -> unit -> Cudd.Cache.t
      val create2 : ?size:int -> ?maxsize:int -> unit -> Cudd.Cache.t
      val create3 : ?size:int -> ?maxsize:int -> unit -> Cudd.Cache.t
      external arity : Cudd.Cache.t -> int = "camlidl_cudd_cache_arity"
      external clear : Cudd.Cache.t -> unit = "camlidl_cudd_cache_clear"
    end
  module Memo :
    sig
      type memo_discr = Global | Cache | Hash
      type t = Global | Cache of Cudd.Cache.t | Hash of Cudd.Hash.t
      val clear : Cudd.Memo.t -> unit
    end
  module Man :
    sig
      type d
      type v
      type 'a t
      type reorder =
          REORDER_SAME
        | REORDER_NONE
        | REORDER_RANDOM
        | REORDER_RANDOM_PIVOT
        | REORDER_SIFT
        | REORDER_SIFT_CONVERGE
        | REORDER_SYMM_SIFT
        | REORDER_SYMM_SIFT_CONV
        | REORDER_WINDOW2
        | REORDER_WINDOW3
        | REORDER_WINDOW4
        | REORDER_WINDOW2_CONV
        | REORDER_WINDOW3_CONV
        | REORDER_WINDOW4_CONV
        | REORDER_GROUP_SIFT
        | REORDER_GROUP_SIFT_CONV
        | REORDER_ANNEALING
        | REORDER_GENETIC
        | REORDER_LINEAR
        | REORDER_LINEAR_CONVERGE
        | REORDER_LAZY_SIFT
        | REORDER_EXACT
      type aggregation =
          NO_CHECK
        | GROUP_CHECK
        | GROUP_CHECK2
        | GROUP_CHECK3
        | GROUP_CHECK4
        | GROUP_CHECK5
        | GROUP_CHECK6
        | GROUP_CHECK7
        | GROUP_CHECK8
        | GROUP_CHECK9
      type lazygroup =
          LAZY_NONE
        | LAZY_SOFT_GROUP
        | LAZY_HARD_GROUP
        | LAZY_UNGROUP
      type vartype = VAR_PRIMARY_INPUT | VAR_PRESENT_STATE | VAR_NEXT_STATE
      type mtr = MTR_DEFAULT | MTR_FIXED
      type error =
          NO_ERROR
        | MEMORY_OUT
        | TOO_MANY_NODES
        | MAX_MEM_EXCEEDED
        | INVALID_ARG
        | INTERNAL_ERROR
      type dt = Cudd.Man.d Cudd.Man.t
      type vt = Cudd.Man.v Cudd.Man.t
      type tbool = False | True | Top
      val string_of_reorder : Cudd.Man.reorder -> string
      val string_of_error : Cudd.Man.error -> string
      val print_limit : int Pervasives.ref
      external set_gc : int -> (unit -> unit) -> (unit -> unit) -> unit
        = "camlidl_cudd_set_gc"
      external srandom : int -> unit = "camlidl_cudd_man_srandom"
      external _make :
        bool -> int -> int -> int -> int -> int -> 'a Cudd.Man.t
        = "camlidl_cudd_man__make_bytecode" "camlidl_cudd_man__make"
      val make_d :
        ?numVars:int ->
        ?numVarsZ:int ->
        ?numSlots:int ->
        ?cacheSize:int -> ?maxMemory:int -> unit -> Cudd.Man.d Cudd.Man.t
      val make_v :
        ?numVars:int ->
        ?numVarsZ:int ->
        ?numSlots:int ->
        ?cacheSize:int -> ?maxMemory:int -> unit -> Cudd.Man.v Cudd.Man.t
      external debugcheck : 'a Cudd.Man.t -> bool
        = "camlidl_cudd_man_debugcheck"
      external check_keys : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_check_keys"
      external level_of_var : 'a Cudd.Man.t -> int -> int
        = "camlidl_cudd_man_level_of_var"
      external var_of_level : 'a Cudd.Man.t -> int -> int
        = "camlidl_cudd_man_var_of_level"
      external reduce_heap : 'a Cudd.Man.t -> Cudd.Man.reorder -> int -> unit
        = "camlidl_cudd_man_reduce_heap"
      external shuffle_heap : 'a Cudd.Man.t -> int array -> unit
        = "camlidl_cudd_man_shuffle_heap"
      external garbage_collect : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_garbage_collect"
      external flush : 'a Cudd.Man.t -> unit = "camlidl_cudd_man_cache_flush"
      external enable_autodyn : 'a Cudd.Man.t -> Cudd.Man.reorder -> unit
        = "camlidl_cudd_man_enable_autodyn"
      external disable_autodyn : 'a Cudd.Man.t -> unit
        = "camlidl_cudd_man_disable_autodyn"
      external autodyn_status : 'a Cudd.Man.t -> Cudd.Man.reorder option
        = "camlidl_cudd_man_autodyn_status"
      external group : 'a Cudd.Man.t -> int -> int -> Cudd.Man.mtr -> unit
        = "camlidl_cudd_man_group"
      external ungroupall : 'a Cudd.Man.t -> unit
        = "camlidl_cudd_man_ungroupall"
      external set_varmap : 'a Cudd.Man.t -> int array -> unit
        = "camlidl_cudd_man_set_varmap"
      external get_background : Cudd.Man.dt -> float
        = "camlidl_cudd_man_get_background"
      external set_background : Cudd.Man.dt -> float -> unit
        = "camlidl_cudd_man_set_background"
      external get_epsilon : Cudd.Man.dt -> float
        = "camlidl_cudd_man_get_epsilon"
      external set_epsilon : Cudd.Man.dt -> float -> unit
        = "camlidl_cudd_man_set_epsilon"
      external get_min_hit : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_min_hit"
      external set_min_hit : 'a Cudd.Man.t -> int -> unit
        = "camlidl_cudd_man_set_min_hit"
      external get_max_cache_hard : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_max_cache_hard"
      external set_max_cache_hard : 'a Cudd.Man.t -> int -> unit
        = "camlidl_cudd_man_set_max_cache_hard"
      external get_looseupto : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_looseupto"
      external set_looseupto : 'a Cudd.Man.t -> int -> unit
        = "camlidl_cudd_man_set_looseupto"
      external get_max_live : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_max_live"
      external set_max_live : 'a Cudd.Man.t -> int -> unit
        = "camlidl_cudd_man_set_max_live"
      external get_max_mem : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_max_mem"
      external set_max_mem : 'a Cudd.Man.t -> int -> unit
        = "camlidl_cudd_man_set_max_mem"
      external get_sift_max_swap : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_sift_max_swap"
      external set_sift_max_swap : 'a Cudd.Man.t -> int -> unit
        = "camlidl_cudd_man_set_sift_max_swap"
      external get_sift_max_var : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_sift_max_var"
      external set_sift_max_var : 'a Cudd.Man.t -> int -> unit
        = "camlidl_cudd_man_set_sift_max_var"
      external get_groupcheck : 'a Cudd.Man.t -> Cudd.Man.aggregation
        = "camlidl_cudd_man_get_groupcheck"
      external set_groupcheck : 'a Cudd.Man.t -> Cudd.Man.aggregation -> unit
        = "camlidl_cudd_man_set_groupcheck"
      external get_arcviolation : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_arcviolation"
      external set_arcviolation : 'a Cudd.Man.t -> int -> unit
        = "camlidl_cudd_man_set_arcviolation"
      external get_crossovers : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_crossovers"
      external set_crossovers : 'a Cudd.Man.t -> int -> unit
        = "camlidl_cudd_man_set_crossovers"
      external get_population : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_population"
      external set_population : 'a Cudd.Man.t -> int -> unit
        = "camlidl_cudd_man_set_population"
      external get_recomb : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_recomb"
      external set_recomb : 'a Cudd.Man.t -> int -> unit
        = "camlidl_cudd_man_set_recomb"
      external get_symmviolation : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_symmviolation"
      external set_symmviolation : 'a Cudd.Man.t -> int -> unit
        = "camlidl_cudd_man_set_symmviolation"
      external get_max_growth : 'a Cudd.Man.t -> float
        = "camlidl_cudd_man_get_max_growth"
      external set_max_growth : 'a Cudd.Man.t -> int -> unit
        = "camlidl_cudd_man_set_max_growth"
      external get_max_growth_alt : 'a Cudd.Man.t -> float
        = "camlidl_cudd_man_get_max_growth_alt"
      external set_max_growth_alt : 'a Cudd.Man.t -> float -> unit
        = "camlidl_cudd_man_set_max_growth_alt"
      external get_reordering_cycle : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_reordering_cycle"
      external set_reordering_cycle : 'a Cudd.Man.t -> int -> unit
        = "camlidl_cudd_man_set_reordering_cycle"
      external get_next_autodyn : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_next_autodyn"
      external set_next_autodyn : 'a Cudd.Man.t -> int -> unit
        = "camlidl_cudd_man_set_next_autodyn"
      external get_cache_hits : 'a Cudd.Man.t -> float
        = "camlidl_cudd_man_get_cache_hits"
      external get_cache_lookups : 'a Cudd.Man.t -> float
        = "camlidl_cudd_man_get_cache_lookups"
      external get_cache_slots : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_cache_slots"
      external get_cache_used_slots : 'a Cudd.Man.t -> float
        = "camlidl_cudd_man_get_cache_used_slots"
      external get_dead : 'a Cudd.Man.t -> int = "camlidl_cudd_man_get_dead"
      external get_error : 'a Cudd.Man.t -> Cudd.Man.error
        = "camlidl_cudd_man_get_error"
      external get_gc_time : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_gc_time"
      external get_gc_nb : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_gc_nb"
      external get_keys : 'a Cudd.Man.t -> int = "camlidl_cudd_man_get_keys"
      external get_linear : 'a Cudd.Man.t -> int -> int -> int
        = "camlidl_cudd_man_get_linear"
      external get_max_cache : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_max_cache"
      external get_min_dead : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_min_dead"
      external get_node_count : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_node_count"
      external get_node_count_peak : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_node_count_peak"
      external get_reordering_time : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_reordering_time"
      external get_reordering_nb : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_reordering_nb"
      external get_bddvar_nb : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_bddvar_nb"
      external get_zddvar_nb : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_zddvar_nb"
      external get_slots : 'a Cudd.Man.t -> int
        = "camlidl_cudd_man_get_slots"
      external get_used_slots : 'a Cudd.Man.t -> float
        = "camlidl_cudd_man_get_used_slots"
      external get_swap_nb : 'a Cudd.Man.t -> float
        = "camlidl_cudd_man_get_swap_nb"
      external print_info : 'a Cudd.Man.t -> unit
        = "camlidl_cudd_man_print_info"
    end
  module Bdd :
    sig
      type 'a t
      type 'a bdd = Bool of bool | Ite of int * 'a Cudd.Bdd.t * 'a Cudd.Bdd.t
      type dt = Cudd.Man.d Cudd.Bdd.t
      type vt = Cudd.Man.v Cudd.Bdd.t
      external manager : 'a Cudd.Bdd.t -> 'a Cudd.Man.t
        = "camlidl_cudd_bdd_manager"
      external is_cst : 'a Cudd.Bdd.t -> bool = "camlidl_cudd_bdd_is_cst"
      external is_complement : 'a Cudd.Bdd.t -> bool
        = "camlidl_cudd_bdd_is_complement"
      external topvar : 'a Cudd.Bdd.t -> int = "camlidl_cudd_bdd_topvar"
      external dthen : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_dthen"
      external delse : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_delse"
      external cofactors :
        int -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t * 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_cofactors"
      external cofactor : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_cofactor"
      external inspect : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.bdd
        = "camlidl_cudd_bdd_inspect"
      external support : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_support"
      external supportsize : 'a Cudd.Bdd.t -> int
        = "camlidl_cudd_bdd_supportsize"
      external is_var_in : int -> 'a Cudd.Bdd.t -> bool
        = "camlidl_cudd_bdd_is_var_in"
      external vectorsupport : 'a Cudd.Bdd.t array -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_vectorsupport"
      external support_inter :
        'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_support_inter"
      external support_union :
        'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_dand"
      external support_diff : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_cofactor"
      external list_of_support : 'a Cudd.Bdd.t -> int list
        = "camlidl_cudd_list_of_support"
      external dtrue : 'a Cudd.Man.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_dtrue"
      external dfalse : 'a Cudd.Man.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_dfalse"
      external ithvar : 'a Cudd.Man.t -> int -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_ithvar"
      external newvar : 'a Cudd.Man.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_newvar"
      external newvar_at_level : 'a Cudd.Man.t -> int -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_newvar_at_level"
      external is_true : 'a Cudd.Bdd.t -> bool = "camlidl_cudd_bdd_is_true"
      external is_false : 'a Cudd.Bdd.t -> bool = "camlidl_cudd_bdd_is_false"
      external is_equal : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> bool
        = "camlidl_cudd_bdd_is_equal"
      external is_leq : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> bool
        = "camlidl_cudd_bdd_is_leq"
      external is_inter_empty : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> bool
        = "camlidl_cudd_bdd_is_inter_empty"
      external is_equal_when :
        'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> bool
        = "camlidl_cudd_bdd_is_equal_when"
      external is_leq_when :
        'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> bool
        = "camlidl_cudd_bdd_is_leq_when"
      val is_included_in : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> bool
      external is_ite_cst :
        'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> bool option
        = "camlidl_cudd_bdd_is_ite_cst"
      external is_var_dependent : int -> 'a Cudd.Bdd.t -> bool
        = "camlidl_cudd_bdd_is_var_dependent"
      external is_var_essential : int -> bool -> 'a Cudd.Bdd.t -> bool
        = "camlidl_cudd_bdd_is_var_essential"
      external size : 'a Cudd.Bdd.t -> int = "camlidl_cudd_bdd_size"
      external nbpaths : 'a Cudd.Bdd.t -> float = "camlidl_cudd_bdd_nbpaths"
      external nbtruepaths : 'a Cudd.Bdd.t -> float
        = "camlidl_cudd_bdd_nbtruepaths"
      external nbminterms : int -> 'a Cudd.Bdd.t -> float
        = "camlidl_cudd_bdd_nbminterms"
      external density : int -> 'a Cudd.Bdd.t -> float
        = "camlidl_cudd_bdd_density"
      external dnot : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_dnot"
      external dand : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_dand"
      external dor : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_dor"
      external xor : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_xor"
      external nand : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_nand"
      external nor : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_nor"
      external nxor : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_nxor"
      val eq : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
      external ite :
        'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_ite"
      external ite_cst :
        'a Cudd.Bdd.t ->
        'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t option
        = "camlidl_cudd_bdd_ite_cst"
      external compose :
        int -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_compose"
      val vectorcompose :
        ?memo:Cudd.Memo.t ->
        'a Cudd.Bdd.t array -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
      external intersect : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_intersect"
      external varmap : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_varmap"
      val permute :
        ?memo:Cudd.Memo.t -> 'a Cudd.Bdd.t -> int array -> 'a Cudd.Bdd.t
      external iter_node : ('a Cudd.Bdd.t -> unit) -> 'a Cudd.Bdd.t -> unit
        = "camlidl_cudd_iter_node"
      external iter_cube :
        (Cudd.Man.tbool array -> unit) -> 'a Cudd.Bdd.t -> unit
        = "camlidl_cudd_bdd_iter_cube"
      external iter_prime :
        (Cudd.Man.tbool array -> unit) ->
        'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> unit
        = "camlidl_cudd_bdd_iter_prime"
      external exist : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_exist"
      external forall : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_forall"
      external existand :
        'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_existand"
      external existxor :
        'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_existxor"
      external booleandiff : 'a Cudd.Bdd.t -> int -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_booleandiff"
      external cube_of_bdd : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_cube_of_bdd"
      external cube_of_minterm :
        'a Cudd.Man.t -> Cudd.Man.tbool array -> 'a Cudd.Bdd.t
        = "camlidl_cudd_cube_of_minterm"
      external list_of_cube : 'a Cudd.Bdd.t -> (int * bool) list
        = "camlidl_cudd_list_of_cube"
      external cube_union : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_cube_union"
      external pick_minterm : 'a Cudd.Bdd.t -> Cudd.Man.tbool array
        = "camlidl_cudd_pick_minterm"
      external pick_cube_on_support :
        'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_pick_cube_on_support"
      external pick_cubes_on_support :
        'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> int -> 'a Cudd.Bdd.t array
        = "camlidl_cudd_pick_cubes_on_support"
      external constrain : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_constrain"
      external tdconstrain : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_tdconstrain"
      external restrict : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_restrict"
      external tdrestrict : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_tdrestrict"
      external minimize : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_minimize"
      external licompaction : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_licompaction"
      external squeeze : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_squeeze"
      external clippingand :
        'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> int -> bool -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_clippingand"
      external clippingexistand :
        'a Cudd.Bdd.t ->
        'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> int -> bool -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_clippingexistand"
      external underapprox :
        int -> int -> bool -> float -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_underapprox"
      external overapprox :
        int -> int -> bool -> float -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_overapprox"
      external remapunderapprox :
        int -> int -> float -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_remapunderapprox"
      external remapoverapprox :
        int -> int -> float -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_remapoverapprox"
      external biasedunderapprox :
        int ->
        int ->
        float -> float -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_biasedunderapprox_bytecode"
        "camlidl_cudd_bdd_biasedunderapprox"
      external biasedoverapprox :
        int ->
        int ->
        float -> float -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_biasedoverapprox_bytecode"
        "camlidl_cudd_bdd_biasedoverapprox"
      external subsetcompress : int -> int -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_subsetcompress"
      external supersetcompress :
        int -> int -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_supersetcompress"
      external subsetHB : int -> int -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_subsetHB"
      external supersetHB : int -> int -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_supersetHB"
      external subsetSP :
        int -> int -> bool -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_subsetSP"
      external supersetSP :
        int -> int -> bool -> 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t
        = "camlidl_cudd_bdd_supersetSP"
      external approxconjdecomp :
        'a Cudd.Bdd.t -> ('a Cudd.Bdd.t * 'a Cudd.Bdd.t) option
        = "camlidl_cudd_bdd_approxconjdecomp"
      external approxdisjdecomp :
        'a Cudd.Bdd.t -> ('a Cudd.Bdd.t * 'a Cudd.Bdd.t) option
        = "camlidl_cudd_bdd_approxdisjdecomp"
      external iterconjdecomp :
        'a Cudd.Bdd.t -> ('a Cudd.Bdd.t * 'a Cudd.Bdd.t) option
        = "camlidl_cudd_bdd_iterconjdecomp"
      external iterdisjdecomp :
        'a Cudd.Bdd.t -> ('a Cudd.Bdd.t * 'a Cudd.Bdd.t) option
        = "camlidl_cudd_bdd_iterdisjdecomp"
      external genconjdecomp :
        'a Cudd.Bdd.t -> ('a Cudd.Bdd.t * 'a Cudd.Bdd.t) option
        = "camlidl_cudd_bdd_genconjdecomp"
      external gendisjdecomp :
        'a Cudd.Bdd.t -> ('a Cudd.Bdd.t * 'a Cudd.Bdd.t) option
        = "camlidl_cudd_bdd_gendisjdecomp"
      external varconjdecomp :
        'a Cudd.Bdd.t -> ('a Cudd.Bdd.t * 'a Cudd.Bdd.t) option
        = "camlidl_cudd_bdd_varconjdecomp"
      external vardisjdecomp :
        'a Cudd.Bdd.t -> ('a Cudd.Bdd.t * 'a Cudd.Bdd.t) option
        = "camlidl_cudd_bdd_vardisjdecomp"
      external transfer : 'a Cudd.Bdd.t -> 'b Cudd.Man.t -> 'b Cudd.Bdd.t
        = "camlidl_cudd_bdd_transfer"
      external correlation : 'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> float
        = "camlidl_cudd_bdd_correlation"
      external correlationweights :
        'a Cudd.Bdd.t -> 'a Cudd.Bdd.t -> float array -> float
        = "camlidl_cudd_bdd_correlationweights"
      external _print : 'a Cudd.Bdd.t -> unit = "camlidl_cudd_print"
      val print__minterm : Format.formatter -> 'a Cudd.Bdd.t -> unit
      val print_minterm :
        (Format.formatter -> int -> unit) ->
        Format.formatter -> 'a Cudd.Bdd.t -> unit
      val print :
        (Format.formatter -> int -> unit) ->
        Format.formatter -> 'a Cudd.Bdd.t -> unit
      val print_list :
        (Format.formatter -> int -> unit) ->
        Format.formatter -> (int * bool) list -> unit
    end
  module Vdd :
    sig
      type +'a t
      type 'a vdd = Leaf of 'a | Ite of int * 'a Cudd.Vdd.t * 'a Cudd.Vdd.t
      external manager : 'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Man.t
        = "camlidl_cudd_bdd_manager"
      external is_cst : 'a Cudd.Vdd.t -> bool = "camlidl_cudd_bdd_is_cst"
      external topvar : 'a Cudd.Vdd.t -> int = "camlidl_cudd_bdd_topvar"
      external dthen : 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t
        = "camlidl_cudd_add_dthen"
      external delse : 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t
        = "camlidl_cudd_add_delse"
      external cofactors :
        int -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t * 'a Cudd.Vdd.t
        = "camlidl_cudd_add_cofactors"
      external cofactor :
        'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Vdd.t
        = "camlidl_cudd_add_cofactor"
      external dval : 'a Cudd.Vdd.t -> 'a = "camlidl_cudd_avdd_dval"
      external inspect : 'a Cudd.Vdd.t -> 'a Cudd.Vdd.vdd
        = "camlidl_cudd_avdd_inspect"
      external support : 'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t
        = "camlidl_cudd_bdd_support"
      external supportsize : 'a Cudd.Vdd.t -> int
        = "camlidl_cudd_bdd_supportsize"
      external is_var_in : int -> 'a Cudd.Vdd.t -> bool
        = "camlidl_cudd_bdd_is_var_in"
      external vectorsupport : 'a Cudd.Vdd.t array -> Cudd.Man.v Cudd.Bdd.t
        = "camlidl_cudd_bdd_vectorsupport"
      external vectorsupport2 :
        Cudd.Man.v Cudd.Bdd.t array ->
        'a Cudd.Vdd.t array -> Cudd.Man.v Cudd.Bdd.t
        = "camlidl_cudd_add_vectorsupport2"
      external cst : Cudd.Man.v Cudd.Man.t -> 'a -> 'a Cudd.Vdd.t
        = "camlidl_cudd_avdd_cst"
      val _background : Cudd.Man.v Cudd.Man.t -> 'a Cudd.Vdd.t
      external ite :
        Cudd.Man.v Cudd.Bdd.t ->
        'a Cudd.Vdd.t -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t
        = "camlidl_cudd_add_ite"
      external ite_cst :
        Cudd.Man.v Cudd.Bdd.t ->
        'a Cudd.Vdd.t -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t option
        = "camlidl_cudd_add_ite_cst"
      external eval_cst :
        'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Vdd.t option
        = "camlidl_cudd_add_eval_cst"
      external compose : int -> Cudd.Bdd.vt -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t
        = "camlidl_cudd_add_compose"
      val vectorcompose :
        ?memo:Cudd.Memo.t ->
        Cudd.Bdd.vt array -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t
      external is_equal : 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t -> bool
        = "camlidl_cudd_bdd_is_equal"
      external is_equal_when :
        'a Cudd.Vdd.t -> 'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> bool
        = "camlidl_cudd_bdd_is_equal_when"
      external is_eval_cst :
        'a 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 -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t -> 'a option
        = "camlidl_cudd_avdd_is_ite_cst"
      external size : 'a Cudd.Vdd.t -> int = "camlidl_cudd_bdd_size"
      external nbpaths : 'a Cudd.Vdd.t -> float = "camlidl_cudd_bdd_nbpaths"
      external nbnonzeropaths : 'a Cudd.Vdd.t -> float
        = "camlidl_cudd_bdd_nbtruepaths"
      external nbminterms : int -> 'a Cudd.Vdd.t -> float
        = "camlidl_cudd_bdd_nbminterms"
      external density : int -> 'a Cudd.Vdd.t -> float
        = "camlidl_cudd_bdd_density"
      external nbleaves : 'a Cudd.Vdd.t -> int = "camlidl_cudd_add_nbleaves"
      external varmap : 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t
        = "camlidl_cudd_add_varmap"
      val permute :
        ?memo:Cudd.Memo.t -> 'a Cudd.Vdd.t -> int array -> 'a Cudd.Vdd.t
      external iter_cube :
        (Cudd.Man.tbool array -> 'a -> unit) -> 'a Cudd.Vdd.t -> unit
        = "camlidl_cudd_avdd_iter_cube"
      external iter_node : ('a Cudd.Vdd.t -> unit) -> 'a Cudd.Vdd.t -> unit
        = "camlidl_cudd_iter_node"
      external guard_of_node :
        'a Cudd.Vdd.t -> 'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t
        = "camlidl_cudd_add_guard_of_node"
      external guard_of_nonbackground :
        'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t
        = "camlidl_cudd_add_guard_of_nonbackground"
      val nodes_below_level :
        ?max:int -> 'a Cudd.Vdd.t -> int option -> 'a Cudd.Vdd.t array
      external guard_of_leaf : 'a Cudd.Vdd.t -> 'a -> Cudd.Man.v Cudd.Bdd.t
        = "camlidl_cudd_avdd_guard_of_leaf"
      external leaves : 'a Cudd.Vdd.t -> 'a array
        = "camlidl_cudd_avdd_leaves"
      external pick_leaf : 'a Cudd.Vdd.t -> 'a
        = "camlidl_cudd_avdd_pick_leaf"
      val guardleafs : 'a Cudd.Vdd.t -> (Cudd.Man.v Cudd.Bdd.t * 'a) array
      external constrain :
        'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Vdd.t
        = "camlidl_cudd_add_constrain"
      external tdconstrain :
        'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Vdd.t
        = "camlidl_cudd_add_tdconstrain"
      external restrict :
        'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Vdd.t
        = "camlidl_cudd_add_restrict"
      external tdrestrict :
        'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Vdd.t
        = "camlidl_cudd_add_tdrestrict"
      external transfer :
        'a Cudd.Vdd.t -> Cudd.Man.v Cudd.Man.t -> 'a Cudd.Vdd.t
        = "camlidl_cudd_add_transfer"
      val print__minterm :
        (Format.formatter -> 'a -> unit) ->
        Format.formatter -> 'a Cudd.Vdd.t -> unit
      val print_minterm :
        (Format.formatter -> int -> unit) ->
        (Format.formatter -> 'a -> unit) ->
        Format.formatter -> 'a Cudd.Vdd.t -> unit
      val print :
        (Format.formatter -> Cudd.Man.v Cudd.Bdd.t -> unit) ->
        (Format.formatter -> 'a -> unit) ->
        Format.formatter -> 'a Cudd.Vdd.t -> unit
    end
  module Custom :
    sig
      type pid
      and mlvalue
      type common = {
        pid : Cudd.Custom.pid;
        arity : int;
        memo : Cudd.Memo.t;
      }
      type ('a, 'b) op1 = {
        common1 : Cudd.Custom.common;
        closure1 : 'a -> 'b;
      }
      type ('a, 'b, 'c) op2 = {
        common2 : Cudd.Custom.common;
        closure2 : 'a -> 'b -> 'c;
        ospecial2 :
          ('a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t option) option;
        commutative : bool;
        idempotent : bool;
      }
      type ('a, 'b) test2 = {
        common2t : Cudd.Custom.common;
        closure2t : 'a -> 'b -> bool;
        ospecial2t : ('a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> bool option) option;
        symetric : bool;
        reflexive : bool;
      }
      type ('a, 'b, 'c, 'd) op3 = {
        common3 : Cudd.Custom.common;
        closure3 : 'a -> 'b -> 'c -> 'd;
        ospecial3 :
          ('a Cudd.Vdd.t ->
           'b Cudd.Vdd.t -> 'c Cudd.Vdd.t -> 'd Cudd.Vdd.t option)
          option;
      }
      type ('a, 'b) opN = {
        commonN : Cudd.Custom.common;
        arityNbdd : int;
        closureN :
          Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t option;
      }
      type ('a, 'b) opG = {
        commonG : Cudd.Custom.common;
        arityGbdd : int;
        closureG :
          Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t option;
        oclosureBeforeRec :
          (int * bool ->
           Cudd.Bdd.vt array ->
           'a Cudd.Vdd.t array -> Cudd.Bdd.vt array * 'a Cudd.Vdd.t array)
          option;
        oclosureIte :
          (int -> 'b Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'b Cudd.Vdd.t) option;
      }
      type 'a exist = {
        commonexist : Cudd.Custom.common;
        combineexist : ('a, 'a, 'a) Cudd.Custom.op2;
      }
      type 'a existand = {
        commonexistand : Cudd.Custom.common;
        combineexistand : ('a, 'a, 'a) Cudd.Custom.op2;
        bottomexistand : 'a;
      }
      type ('a, 'b) existop1 = {
        commonexistop1 : Cudd.Custom.common;
        combineexistop1 : ('b, 'b, 'b) Cudd.Custom.op2;
        existop1 : ('a, 'b) Cudd.Custom.op1;
      }
      type ('a, 'b) existandop1 = {
        commonexistandop1 : Cudd.Custom.common;
        combineexistandop1 : ('b, 'b, 'b) Cudd.Custom.op2;
        existandop1 : ('a, 'b) Cudd.Custom.op1;
        bottomexistandop1 : 'b;
      }
      external newpid : unit -> Cudd.Custom.pid = "camlidl_custom_newpid"
      external apply_op1 :
        ('a, 'b) Cudd.Custom.op1 -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t
        = "camlidl_custom_apply_op1"
      external apply_op2 :
        ('a, 'b, 'c) Cudd.Custom.op2 ->
        'a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t
        = "camlidl_custom_apply_op2"
      external apply_test2 :
        ('a, 'b) Cudd.Custom.test2 -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> bool
        = "camlidl_custom_apply_test2"
      external apply_op3 :
        ('a, 'b, 'c, 'd) Cudd.Custom.op3 ->
        'a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t -> 'd Cudd.Vdd.t
        = "camlidl_custom_apply_op3"
      external apply_opN :
        ('a, 'b) Cudd.Custom.opN ->
        Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t
        = "camlidl_cudd_apply_opN"
      external apply_opG :
        ('a, 'b) Cudd.Custom.opG ->
        Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t
        = "camlidl_cudd_apply_opG"
      external _apply_exist :
        'a Cudd.Custom.exist -> Cudd.Bdd.vt -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t
        = "camlidl_custom__apply_exist"
      external _apply_existand :
        'a Cudd.Custom.existand ->
        Cudd.Bdd.vt -> Cudd.Bdd.vt -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t
        = "camlidl_custom__apply_existand"
      external _apply_existop1 :
        ('a, 'b) Cudd.Custom.existop1 ->
        Cudd.Bdd.vt -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t
        = "camlidl_custom__apply_existop1"
      external _apply_existandop1 :
        ('a, 'b) Cudd.Custom.existandop1 ->
        Cudd.Bdd.vt -> Cudd.Bdd.vt -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t
        = "camlidl_custom__apply_existandop1"
    end
  module Weakke :
    sig
      type 'a t
      type 'a hashtbl = 'a Cudd.Weakke.t
      type 'a compare = { hash : 'a -> int; equal : 'a -> 'a -> bool; }
      val create : int -> 'a Cudd.Weakke.t
      val clear : 'a Cudd.Weakke.t -> unit
      val merge : 'a Cudd.Weakke.t -> 'a -> 'a
      val merge_map : 'a Cudd.Weakke.t -> 'a -> ('a -> 'a) -> 'a
      val add : 'a Cudd.Weakke.t -> 'a -> unit
      val remove : 'a Cudd.Weakke.t -> 'a -> unit
      val find : 'a Cudd.Weakke.t -> 'a -> 'a
      val find_all : 'a Cudd.Weakke.t -> 'a -> 'a list
      val mem : 'a Cudd.Weakke.t -> 'a -> bool
      val iter : ('a -> 'b) -> 'a Cudd.Weakke.t -> unit
      val fold : ('a -> 'b -> 'b) -> 'a Cudd.Weakke.t -> 'b -> 'b
      val count : 'a Cudd.Weakke.t -> int
      val stats : 'a Cudd.Weakke.t -> int * int * int * int * int * int
      val print :
        ?first:(unit, Format.formatter, unit) Pervasives.format ->
        ?sep:(unit, Format.formatter, unit) Pervasives.format ->
        ?last:(unit, Format.formatter, unit) Pervasives.format ->
        (Format.formatter -> 'a -> unit) ->
        Format.formatter -> 'a Cudd.Weakke.t -> unit
      module type S =
        sig
          type data
          type t
          val create : int -> Cudd.Weakke.S.t
          val clear : Cudd.Weakke.S.t -> unit
          val merge :
            Cudd.Weakke.S.t -> Cudd.Weakke.S.data -> Cudd.Weakke.S.data
          val merge_map :
            Cudd.Weakke.S.t ->
            Cudd.Weakke.S.data ->
            (Cudd.Weakke.S.data -> Cudd.Weakke.S.data) -> Cudd.Weakke.S.data
          val add : Cudd.Weakke.S.t -> Cudd.Weakke.S.data -> unit
          val remove : Cudd.Weakke.S.t -> Cudd.Weakke.S.data -> unit
          val find :
            Cudd.Weakke.S.t -> Cudd.Weakke.S.data -> Cudd.Weakke.S.data
          val find_all :
            Cudd.Weakke.S.t -> Cudd.Weakke.S.data -> Cudd.Weakke.S.data list
          val mem : Cudd.Weakke.S.t -> Cudd.Weakke.S.data -> bool
          val iter : (Cudd.Weakke.S.data -> unit) -> Cudd.Weakke.S.t -> unit
          val fold :
            (Cudd.Weakke.S.data -> 'a -> 'a) -> Cudd.Weakke.S.t -> 'a -> 'a
          val count : Cudd.Weakke.S.t -> int
          val stats : Cudd.Weakke.S.t -> int * int * int * int * int * int
          val print :
            ?first:(unit, Format.formatter, unit) Pervasives.format ->
            ?sep:(unit, Format.formatter, unit) Pervasives.format ->
            ?last:(unit, Format.formatter, unit) Pervasives.format ->
            (Format.formatter -> Cudd.Weakke.S.data -> unit) ->
            Format.formatter -> Cudd.Weakke.S.t -> unit
        end
      module Make :
        functor (H : Hashtbl.HashedType) ->
          sig
            type data = H.t
            type t
            val create : int -> t
            val clear : t -> unit
            val merge : t -> data -> data
            val merge_map : t -> data -> (data -> data) -> data
            val add : t -> data -> unit
            val remove : t -> data -> unit
            val find : t -> data -> data
            val find_all : t -> data -> data list
            val mem : t -> data -> bool
            val iter : (data -> unit) -> t -> unit
            val fold : (data -> 'a -> 'a) -> t -> 'a -> 'a
            val count : t -> int
            val stats : t -> int * int * int * int * int * int
            val print :
              ?first:(unit, Format.formatter, unit) format ->
              ?sep:(unit, Format.formatter, unit) format ->
              ?last:(unit, Format.formatter, unit) format ->
              (Format.formatter -> data -> unit) ->
              Format.formatter -> t -> unit
          end
      module Compare :
        sig
          val add : 'a Cudd.Weakke.compare -> 'a Cudd.Weakke.t -> 'a -> unit
          val find_or :
            'a Cudd.Weakke.compare ->
            'a Cudd.Weakke.t -> 'a -> (int -> int -> 'a) -> 'a
          val merge : 'a Cudd.Weakke.compare -> 'a Cudd.Weakke.t -> 'a -> 'a
          val merge_map :
            'a Cudd.Weakke.compare ->
            'a Cudd.Weakke.t -> 'a -> ('a -> 'a) -> 'a
          val find : 'a Cudd.Weakke.compare -> 'a Cudd.Weakke.t -> 'a -> 'a
          val find_shadow :
            'a Cudd.Weakke.compare ->
            'a Cudd.Weakke.t -> 'a -> ('a Weak.t -> int -> 'b) -> 'b -> 'b
          val remove :
            'a Cudd.Weakke.compare -> 'a Cudd.Weakke.t -> 'a -> unit
          val mem : 'a Cudd.Weakke.compare -> 'a Cudd.Weakke.t -> 'a -> bool
          val find_all :
            'a Cudd.Weakke.compare -> 'a Cudd.Weakke.t -> 'a -> 'a list
        end
    end
  module PWeakke :
    sig
      type 'a compare =
        'a Cudd.Weakke.compare = {
        hash : 'a -> int;
        equal : 'a -> 'a -> bool;
      }
      type 'a t = {
        compare : 'a Cudd.PWeakke.compare;
        hashtbl : 'a Cudd.Weakke.t;
      }
      val create :
        ('a -> int) -> ('a -> 'a -> bool) -> int -> 'a Cudd.PWeakke.t
      val clear : 'a Cudd.PWeakke.t -> unit
      val merge : 'a Cudd.PWeakke.t -> 'a -> 'a
      val merge_map : 'a Cudd.PWeakke.t -> 'a -> ('a -> 'a) -> 'a
      val add : 'a Cudd.PWeakke.t -> 'a -> unit
      val remove : 'a Cudd.PWeakke.t -> 'a -> unit
      val find : 'a Cudd.PWeakke.t -> 'a -> 'a
      val find_all : 'a Cudd.PWeakke.t -> 'a -> 'a list
      val mem : 'a Cudd.PWeakke.t -> 'a -> bool
      val iter : ('a -> 'b) -> 'a Cudd.PWeakke.t -> unit
      val fold : ('a -> 'b -> 'b) -> 'a Cudd.PWeakke.t -> 'b -> 'b
      val count : 'a Cudd.PWeakke.t -> int
      val stats : 'a Cudd.PWeakke.t -> int * int * int * int * int * int
      val print :
        ?first:(unit, Format.formatter, unit) Pervasives.format ->
        ?sep:(unit, Format.formatter, unit) Pervasives.format ->
        ?last:(unit, Format.formatter, unit) Pervasives.format ->
        (Format.formatter -> 'a -> unit) ->
        Format.formatter -> 'a Cudd.PWeakke.t -> unit
    end
  module Mtbdd :
    sig
      type 'a unique
      type 'a t = 'a Cudd.Mtbdd.unique Cudd.Vdd.t
      type 'a table = 'a 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 -> 'a -> unit) ->
        Format.formatter -> 'a Cudd.Mtbdd.table -> unit
      val make_table :
        hash:('a -> int) -> equal:('a -> 'a -> bool) -> 'a Cudd.Mtbdd.table
      val unique : 'a Cudd.Mtbdd.table -> 'a -> 'a Cudd.Mtbdd.unique
      val get : 'a Cudd.Mtbdd.unique -> 'a
      type 'a mtbdd =
          Leaf of 'a Cudd.Mtbdd.unique
        | Ite of int * 'a Cudd.Mtbdd.t * 'a Cudd.Mtbdd.t
      external manager : 'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Man.t
        = "camlidl_cudd_bdd_manager"
      external is_cst : 'a Cudd.Mtbdd.t -> bool = "camlidl_cudd_bdd_is_cst"
      external topvar : 'a Cudd.Mtbdd.t -> int = "camlidl_cudd_bdd_topvar"
      external dthen : 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t
        = "camlidl_cudd_add_dthen"
      external delse : 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t
        = "camlidl_cudd_add_delse"
      external cofactors :
        int -> 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t * 'a Cudd.Mtbdd.t
        = "camlidl_cudd_add_cofactors"
      external cofactor :
        'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbdd.t
        = "camlidl_cudd_add_cofactor"
      val dval_u : 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.unique
      val dval : 'a Cudd.Mtbdd.t -> 'a
      val inspect : 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.mtbdd
      external support : 'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t
        = "camlidl_cudd_bdd_support"
      external supportsize : 'a Cudd.Mtbdd.t -> int
        = "camlidl_cudd_bdd_supportsize"
      external is_var_in : int -> 'a Cudd.Mtbdd.t -> bool
        = "camlidl_cudd_bdd_is_var_in"
      external vectorsupport : 'a Cudd.Mtbdd.t array -> Cudd.Man.v Cudd.Bdd.t
        = "camlidl_cudd_bdd_vectorsupport"
      external vectorsupport2 :
        Cudd.Man.v Cudd.Bdd.t array ->
        'a Cudd.Mtbdd.t array -> Cudd.Man.v Cudd.Bdd.t
        = "camlidl_cudd_add_vectorsupport2"
      val cst_u :
        Cudd.Man.v Cudd.Man.t -> 'a Cudd.Mtbdd.unique -> 'a Cudd.Mtbdd.t
      val cst :
        Cudd.Man.v Cudd.Man.t -> 'a Cudd.Mtbdd.table -> 'a -> 'a Cudd.Mtbdd.t
      external ite :
        Cudd.Man.v Cudd.Bdd.t ->
        'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t
        = "camlidl_cudd_add_ite"
      external ite_cst :
        Cudd.Man.v Cudd.Bdd.t ->
        'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t option
        = "camlidl_cudd_add_ite_cst"
      external eval_cst :
        'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbdd.t option
        = "camlidl_cudd_add_eval_cst"
      external compose :
        int -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t
        = "camlidl_cudd_add_compose"
      val vectorcompose :
        ?memo:Cudd.Memo.t ->
        Cudd.Man.v Cudd.Bdd.t array -> 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t
      external is_equal : 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t -> bool
        = "camlidl_cudd_bdd_is_equal"
      external is_equal_when :
        'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> bool
        = "camlidl_cudd_bdd_is_equal_when"
      val is_eval_cst_u :
        'a Cudd.Mtbdd.t ->
        Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbdd.unique option
      val is_ite_cst_u :
        Cudd.Man.v Cudd.Bdd.t ->
        'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.unique option
      val is_eval_cst : 'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a option
      val is_ite_cst :
        Cudd.Man.v Cudd.Bdd.t ->
        'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t -> 'a option
      external size : 'a Cudd.Mtbdd.t -> int = "camlidl_cudd_bdd_size"
      external nbpaths : 'a Cudd.Mtbdd.t -> float
        = "camlidl_cudd_bdd_nbpaths"
      external nbnonzeropaths : 'a Cudd.Mtbdd.t -> float
        = "camlidl_cudd_bdd_nbtruepaths"
      external nbminterms : int -> 'a Cudd.Mtbdd.t -> float
        = "camlidl_cudd_bdd_nbminterms"
      external density : int -> 'a Cudd.Mtbdd.t -> float
        = "camlidl_cudd_bdd_density"
      external nbleaves : 'a Cudd.Mtbdd.t -> int
        = "camlidl_cudd_add_nbleaves"
      external varmap : 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t
        = "camlidl_cudd_add_varmap"
      val permute :
        ?memo:Cudd.Memo.t -> 'a Cudd.Mtbdd.t -> int array -> 'a Cudd.Mtbdd.t
      val iter_cube_u :
        (Cudd.Man.tbool array -> 'a Cudd.Mtbdd.unique -> unit) ->
        'a Cudd.Mtbdd.t -> unit
      val iter_cube :
        (Cudd.Man.tbool array -> 'a -> unit) -> 'a Cudd.Mtbdd.t -> unit
      external iter_node :
        ('a Cudd.Mtbdd.t -> unit) -> 'a Cudd.Mtbdd.t -> unit
        = "camlidl_cudd_iter_node"
      external guard_of_node :
        'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t
        = "camlidl_cudd_add_guard_of_node"
      external guard_of_nonbackground :
        'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t
        = "camlidl_cudd_add_guard_of_nonbackground"
      val nodes_below_level :
        ?max:int -> 'a Cudd.Mtbdd.t -> int option -> 'a Cudd.Mtbdd.t array
      val guard_of_leaf_u :
        'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.unique -> Cudd.Man.v Cudd.Bdd.t
      val guard_of_leaf :
        'a Cudd.Mtbdd.table -> 'a Cudd.Mtbdd.t -> 'a -> Cudd.Man.v Cudd.Bdd.t
      val leaves_u : 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.unique array
      val leaves : 'a Cudd.Mtbdd.t -> 'a array
      val pick_leaf_u : 'a Cudd.Mtbdd.t -> 'a Cudd.Mtbdd.unique
      val pick_leaf : 'a Cudd.Mtbdd.t -> 'a
      val guardleafs_u :
        'a Cudd.Mtbdd.t ->
        (Cudd.Man.v Cudd.Bdd.t * 'a Cudd.Mtbdd.unique) array
      val guardleafs : 'a Cudd.Mtbdd.t -> (Cudd.Man.v Cudd.Bdd.t * 'a) array
      external constrain :
        'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbdd.t
        = "camlidl_cudd_add_constrain"
      external tdconstrain :
        'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbdd.t
        = "camlidl_cudd_add_tdconstrain"
      external restrict :
        'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbdd.t
        = "camlidl_cudd_add_restrict"
      external tdrestrict :
        'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbdd.t
        = "camlidl_cudd_add_tdrestrict"
      external transfer :
        'a Cudd.Mtbdd.t -> Cudd.Man.v Cudd.Man.t -> 'a Cudd.Mtbdd.t
        = "camlidl_cudd_add_transfer"
      val print__minterm :
        (Format.formatter -> 'a -> unit) ->
        Format.formatter -> 'a Cudd.Mtbdd.t -> unit
      val print_minterm :
        (Format.formatter -> int -> unit) ->
        (Format.formatter -> 'a -> unit) ->
        Format.formatter -> 'a Cudd.Mtbdd.t -> unit
      val print :
        (Format.formatter -> Cudd.Man.v Cudd.Bdd.t -> unit) ->
        (Format.formatter -> 'a -> unit) ->
        Format.formatter -> 'a Cudd.Mtbdd.t -> unit
    end
  module Mtbddc :
    sig
      type 'a capsule = private { content : 'a; }
      type 'a unique
      type 'a t = 'a Cudd.Mtbddc.unique Cudd.Vdd.t
      type 'a table = 'a Cudd.Mtbddc.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 -> 'a -> unit) ->
        Format.formatter -> 'a Cudd.Mtbddc.table -> unit
      val make_table :
        hash:('a -> int) -> equal:('a -> 'a -> bool) -> 'a Cudd.Mtbddc.table
      val unique : 'a Cudd.Mtbddc.table -> 'a -> 'a Cudd.Mtbddc.unique
      val get : 'a Cudd.Mtbddc.unique -> 'a
      type 'a mtbdd =
          Leaf of 'a Cudd.Mtbddc.unique
        | Ite of int * 'a Cudd.Mtbddc.t * 'a Cudd.Mtbddc.t
      external manager : 'a Cudd.Mtbddc.t -> Cudd.Man.v Cudd.Man.t
        = "camlidl_cudd_bdd_manager"
      external is_cst : 'a Cudd.Mtbddc.t -> bool = "camlidl_cudd_bdd_is_cst"
      external topvar : 'a Cudd.Mtbddc.t -> int = "camlidl_cudd_bdd_topvar"
      external dthen : 'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.t
        = "camlidl_cudd_add_dthen"
      external delse : 'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.t
        = "camlidl_cudd_add_delse"
      external cofactors :
        int -> 'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.t * 'a Cudd.Mtbddc.t
        = "camlidl_cudd_add_cofactors"
      external cofactor :
        'a Cudd.Mtbddc.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbddc.t
        = "camlidl_cudd_add_cofactor"
      val dval_u : 'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.unique
      val dval : 'a Cudd.Mtbddc.t -> 'a
      val inspect : 'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.mtbdd
      external support : 'a Cudd.Mtbddc.t -> Cudd.Man.v Cudd.Bdd.t
        = "camlidl_cudd_bdd_support"
      external supportsize : 'a Cudd.Mtbddc.t -> int
        = "camlidl_cudd_bdd_supportsize"
      external is_var_in : int -> 'a Cudd.Mtbddc.t -> bool
        = "camlidl_cudd_bdd_is_var_in"
      external vectorsupport :
        'a Cudd.Mtbddc.t array -> Cudd.Man.v Cudd.Bdd.t
        = "camlidl_cudd_bdd_vectorsupport"
      external vectorsupport2 :
        Cudd.Man.v Cudd.Bdd.t array ->
        'a Cudd.Mtbddc.t array -> Cudd.Man.v Cudd.Bdd.t
        = "camlidl_cudd_add_vectorsupport2"
      val cst_u :
        Cudd.Man.v Cudd.Man.t -> 'a Cudd.Mtbddc.unique -> 'a Cudd.Mtbddc.t
      val cst :
        Cudd.Man.v Cudd.Man.t ->
        'a Cudd.Mtbddc.table -> 'a -> 'a Cudd.Mtbddc.t
      external ite :
        Cudd.Man.v Cudd.Bdd.t ->
        'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.t
        = "camlidl_cudd_add_ite"
      external ite_cst :
        Cudd.Man.v Cudd.Bdd.t ->
        'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.t option
        = "camlidl_cudd_add_ite_cst"
      external eval_cst :
        'a Cudd.Mtbddc.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbddc.t option
        = "camlidl_cudd_add_eval_cst"
      external compose :
        int -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.t
        = "camlidl_cudd_add_compose"
      external vectorcompose :
        Cudd.Man.v Cudd.Bdd.t array -> 'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.t
        = "camlidl_cudd_add_vectorcompose"
      external is_equal : 'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.t -> bool
        = "camlidl_cudd_bdd_is_equal"
      external is_equal_when :
        'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.t -> Cudd.Man.v Cudd.Bdd.t -> bool
        = "camlidl_cudd_bdd_is_equal_when"
      val is_eval_cst_u :
        'a Cudd.Mtbddc.t ->
        Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbddc.unique option
      val is_ite_cst_u :
        Cudd.Man.v Cudd.Bdd.t ->
        'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.unique option
      val is_eval_cst :
        'a Cudd.Mtbddc.t -> Cudd.Man.v Cudd.Bdd.t -> 'a option
      val is_ite_cst :
        Cudd.Man.v Cudd.Bdd.t ->
        'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.t -> 'a option
      external size : 'a Cudd.Mtbddc.t -> int = "camlidl_cudd_bdd_size"
      external nbpaths : 'a Cudd.Mtbddc.t -> float
        = "camlidl_cudd_bdd_nbpaths"
      external nbnonzeropaths : 'a Cudd.Mtbddc.t -> float
        = "camlidl_cudd_bdd_nbtruepaths"
      external nbminterms : int -> 'a Cudd.Mtbddc.t -> float
        = "camlidl_cudd_bdd_nbminterms"
      external density : int -> 'a Cudd.Mtbddc.t -> float
        = "camlidl_cudd_bdd_density"
      external nbleaves : 'a Cudd.Mtbddc.t -> int
        = "camlidl_cudd_add_nbleaves"
      external varmap : 'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.t
        = "camlidl_cudd_add_varmap"
      external permute : 'a Cudd.Mtbddc.t -> int array -> 'a Cudd.Mtbddc.t
        = "camlidl_cudd_add_permute"
      val iter_cube_u :
        (Cudd.Man.tbool array -> 'a Cudd.Mtbddc.unique -> unit) ->
        'a Cudd.Mtbddc.t -> unit
      val iter_cube :
        (Cudd.Man.tbool array -> 'a -> unit) -> 'a Cudd.Mtbddc.t -> unit
      external iter_node :
        ('a Cudd.Mtbddc.t -> unit) -> 'a Cudd.Mtbddc.t -> unit
        = "camlidl_cudd_iter_node"
      external guard_of_node :
        'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.t -> Cudd.Man.v Cudd.Bdd.t
        = "camlidl_cudd_add_guard_of_node"
      external guard_of_nonbackground :
        'a Cudd.Mtbddc.t -> Cudd.Man.v Cudd.Bdd.t
        = "camlidl_cudd_add_guard_of_nonbackground"
      val nodes_below_level :
        ?max:int -> 'a Cudd.Mtbddc.t -> int option -> 'a Cudd.Mtbddc.t array
      val guard_of_leaf_u :
        'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.unique -> Cudd.Man.v Cudd.Bdd.t
      val guard_of_leaf :
        'a Cudd.Mtbddc.table ->
        'a Cudd.Mtbddc.t -> 'a -> Cudd.Man.v Cudd.Bdd.t
      val leaves_u : 'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.unique array
      val leaves : 'a Cudd.Mtbddc.t -> 'a array
      val pick_leaf_u : 'a Cudd.Mtbddc.t -> 'a Cudd.Mtbddc.unique
      val pick_leaf : 'a Cudd.Mtbddc.t -> 'a
      val guardleafs_u :
        'a Cudd.Mtbddc.t ->
        (Cudd.Man.v Cudd.Bdd.t * 'a Cudd.Mtbddc.unique) array
      val guardleafs : 'a Cudd.Mtbddc.t -> (Cudd.Man.v Cudd.Bdd.t * 'a) array
      external constrain :
        'a Cudd.Mtbddc.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbddc.t
        = "camlidl_cudd_add_constrain"
      external tdconstrain :
        'a Cudd.Mtbddc.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbddc.t
        = "camlidl_cudd_add_tdconstrain"
      external restrict :
        'a Cudd.Mtbddc.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbddc.t
        = "camlidl_cudd_add_restrict"
      external tdrestrict :
        'a Cudd.Mtbddc.t -> Cudd.Man.v Cudd.Bdd.t -> 'a Cudd.Mtbddc.t
        = "camlidl_cudd_add_tdrestrict"
      external transfer :
        'a Cudd.Mtbddc.t -> Cudd.Man.v Cudd.Man.t -> 'a Cudd.Mtbddc.t
        = "camlidl_cudd_add_transfer"
      val print__minterm :
        (Format.formatter -> 'a -> unit) ->
        Format.formatter -> 'a Cudd.Mtbddc.t -> unit
      val print_minterm :
        (Format.formatter -> int -> unit) ->
        (Format.formatter -> 'a -> unit) ->
        Format.formatter -> 'a Cudd.Mtbddc.t -> unit
      val print :
        (Format.formatter -> Cudd.Man.v Cudd.Bdd.t -> unit) ->
        (Format.formatter -> 'a -> unit) ->
        Format.formatter -> 'a Cudd.Mtbddc.t -> unit
    end
  module User :
    sig
      type pid = Cudd.Custom.pid
      type common =
        Cudd.Custom.common = {
        pid : Cudd.User.pid;
        arity : int;
        memo : Cudd.Memo.t;
      }
      val newpid : unit -> Cudd.Custom.pid
      val make_common : ?memo:Cudd.Memo.t -> int -> Cudd.User.common
      type ('a, 'b) op1 =
        ('a, 'b) Cudd.Custom.op1 = private {
        common1 : Cudd.User.common;
        closure1 : 'a -> 'b;
      }
      val make_op1 :
        ?memo:Cudd.Memo.t -> ('a -> 'b) -> ('a, 'b) Cudd.User.op1
      val apply_op1 :
        ('a, 'b) Cudd.User.op1 -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t
      type ('a, 'b, 'c) op2 =
        ('a, 'b, 'c) Cudd.Custom.op2 = private {
        common2 : Cudd.User.common;
        closure2 : 'a -> 'b -> 'c;
        ospecial2 :
          ('a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t option) option;
        commutative : bool;
        idempotent : bool;
      }
      val make_op2 :
        ?memo:Cudd.Memo.t ->
        ?commutative:bool ->
        ?idempotent:bool ->
        ?special:('a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t option) ->
        ('a -> 'b -> 'c) -> ('a, 'b, 'c) Cudd.User.op2
      val apply_op2 :
        ('a, 'b, 'c) Cudd.User.op2 ->
        'a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t
      type ('a, 'b, 'c, 'd) op3 =
        ('a, 'b, 'c, 'd) Cudd.Custom.op3 = private {
        common3 : Cudd.User.common;
        closure3 : 'a -> 'b -> 'c -> 'd;
        ospecial3 :
          ('a Cudd.Vdd.t ->
           'b Cudd.Vdd.t -> 'c Cudd.Vdd.t -> 'd Cudd.Vdd.t option)
          option;
      }
      val make_op3 :
        ?memo:Cudd.Memo.t ->
        ?special:('a Cudd.Vdd.t ->
                  'b Cudd.Vdd.t -> 'c Cudd.Vdd.t -> 'd Cudd.Vdd.t option) ->
        ('a -> 'b -> 'c -> 'd) -> ('a, 'b, 'c, 'd) Cudd.User.op3
      val apply_op3 :
        ('a, 'b, 'c, 'd) Cudd.User.op3 ->
        'a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t -> 'd Cudd.Vdd.t
      type ('a, 'b) opN =
        ('a, 'b) Cudd.Custom.opN = private {
        commonN : Cudd.User.common;
        arityNbdd : int;
        closureN :
          Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t option;
      }
      val make_opN :
        ?memo:Cudd.Memo.t ->
        int ->
        int ->
        (Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t option) ->
        ('a, 'b) Cudd.User.opN
      val apply_opN :
        ('a, 'b) Cudd.User.opN ->
        Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t
      type ('a, 'b) opG =
        ('a, 'b) Cudd.Custom.opG = private {
        commonG : Cudd.User.common;
        arityGbdd : int;
        closureG :
          Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t option;
        oclosureBeforeRec :
          (int * bool ->
           Cudd.Bdd.vt array ->
           'a Cudd.Vdd.t array -> Cudd.Bdd.vt array * 'a Cudd.Vdd.t array)
          option;
        oclosureIte :
          (int -> 'b Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'b Cudd.Vdd.t) option;
      }
      val make_opG :
        ?memo:Cudd.Memo.t ->
        ?beforeRec:(int * bool ->
                    Cudd.Bdd.vt array ->
                    'a Cudd.Vdd.t array ->
                    Cudd.Bdd.vt array * 'a Cudd.Vdd.t array) ->
        ?ite:(int -> 'b Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'b Cudd.Vdd.t) ->
        int ->
        int ->
        (Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t option) ->
        ('a, 'b) Cudd.User.opG
      val apply_opG :
        ('a, 'b) Cudd.User.opG ->
        Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t
      type ('a, 'b) test2 =
        ('a, 'b) Cudd.Custom.test2 = private {
        common2t : Cudd.User.common;
        closure2t : 'a -> 'b -> bool;
        ospecial2t : ('a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> bool option) option;
        symetric : bool;
        reflexive : bool;
      }
      val make_test2 :
        ?memo:Cudd.Memo.t ->
        ?symetric:bool ->
        ?reflexive:bool ->
        ?special:('a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> bool option) ->
        ('a -> 'b -> bool) -> ('a, 'b) Cudd.User.test2
      val apply_test2 :
        ('a, 'b) Cudd.User.test2 -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> bool
      type 'a exist =
        'a Cudd.Custom.exist = private {
        commonexist : Cudd.User.common;
        combineexist : ('a, 'a, 'a) Cudd.User.op2;
      }
      val make_exist :
        ?memo:Cudd.Memo.t -> ('a, 'a, 'a) Cudd.User.op2 -> 'a Cudd.User.exist
      val apply_exist :
        'a Cudd.User.exist ->
        supp:Cudd.Bdd.vt -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t
      type 'a existand =
        'a Cudd.Custom.existand = private {
        commonexistand : Cudd.User.common;
        combineexistand : ('a, 'a, 'a) Cudd.User.op2;
        bottomexistand : 'a;
      }
      val make_existand :
        ?memo:Cudd.Memo.t ->
        bottom:'a -> ('a, 'a, 'a) Cudd.User.op2 -> 'a Cudd.User.existand
      val apply_existand :
        'a Cudd.User.existand ->
        supp:Cudd.Bdd.vt -> Cudd.Bdd.vt -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t
      type ('a, 'b) existop1 =
        ('a, 'b) Cudd.Custom.existop1 = private {
        commonexistop1 : Cudd.User.common;
        combineexistop1 : ('b, 'b, 'b) Cudd.User.op2;
        existop1 : ('a, 'b) Cudd.User.op1;
      }
      val make_existop1 :
        ?memo:Cudd.Memo.t ->
        op1:('a, 'b) Cudd.User.op1 ->
        ('b, 'b, 'b) Cudd.User.op2 -> ('a, 'b) Cudd.User.existop1
      val apply_existop1 :
        ('a, 'b) Cudd.User.existop1 ->
        supp:Cudd.Bdd.vt -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t
      type ('a, 'b) existandop1 =
        ('a, 'b) Cudd.Custom.existandop1 = private {
        commonexistandop1 : Cudd.User.common;
        combineexistandop1 : ('b, 'b, 'b) Cudd.User.op2;
        existandop1 : ('a, 'b) Cudd.User.op1;
        bottomexistandop1 : 'b;
      }
      val make_existandop1 :
        ?memo:Cudd.Memo.t ->
        op1:('a, 'b) Cudd.User.op1 ->
        bottom:'b ->
        ('b, 'b, 'b) Cudd.User.op2 -> ('a, 'b) Cudd.User.existandop1
      val apply_existandop1 :
        ('a, 'b) Cudd.User.existandop1 ->
        supp:Cudd.Bdd.vt -> Cudd.Bdd.vt -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t
      val clear_common : Cudd.User.common -> unit
      val clear_op1 : ('a, 'b) Cudd.User.op1 -> unit
      val clear_op2 : ('a, 'b, 'c) Cudd.User.op2 -> unit
      val clear_op3 : ('a, 'b, 'c, 'd) Cudd.User.op3 -> unit
      val clear_opN : ('a, 'b) Cudd.User.opN -> unit
      val clear_opG : ('a, 'b) Cudd.User.opG -> unit
      val clear_test2 : ('a, 'b) Cudd.User.test2 -> unit
      val clear_exist : 'a Cudd.User.exist -> unit
      val clear_existand : 'a Cudd.User.existand -> unit
      val clear_existop1 : ('a, 'b) Cudd.User.existop1 -> unit
      val clear_existandop1 : ('a, 'b) Cudd.User.existandop1 -> unit
      val map_op1 :
        ?memo:Cudd.Memo.t -> ('a -> 'b) -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t
      val map_op2 :
        ?memo:Cudd.Memo.t ->
        ?commutative:bool ->
        ?idempotent:bool ->
        ?special:('a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t option) ->
        ('a -> 'b -> 'c) -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t
      val map_op3 :
        ?memo:Cudd.Memo.t ->
        ?special:('a Cudd.Vdd.t ->
                  'b Cudd.Vdd.t -> 'c Cudd.Vdd.t -> 'd Cudd.Vdd.t option) ->
        ('a -> 'b -> 'c -> 'd) ->
        'a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t -> 'd Cudd.Vdd.t
      val map_opN :
        ?memo:Cudd.Memo.t ->
        (Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t option) ->
        Cudd.Bdd.vt array -> 'a Cudd.Vdd.t array -> 'b Cudd.Vdd.t
      val map_test2 :
        ?memo:Cudd.Memo.t ->
        ?symetric:bool ->
        ?reflexive:bool ->
        ?special:('a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> bool option) ->
        ('a -> 'b -> bool) -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> bool
    end
  module Mapleaf :
    sig
      val restrict : bool Pervasives.ref
      val mapleaf1 : ('a -> 'b) -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t
      val retractivemapleaf1 :
        default:'a Cudd.Vdd.t ->
        (Cudd.Bdd.vt -> 'b -> Cudd.Bdd.vt * 'a) ->
        'b Cudd.Vdd.t -> 'a Cudd.Vdd.t
      val expansivemapleaf1 :
        default:'a Cudd.Vdd.t ->
        merge:('a Cudd.Vdd.t -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t) ->
        (Cudd.Bdd.vt -> 'b -> Cudd.Bdd.vt * 'a) ->
        'b Cudd.Vdd.t -> 'a Cudd.Vdd.t
      val combineleaf1 :
        default:'a ->
        combine:('b -> 'a -> 'a) ->
        (Cudd.Bdd.vt -> 'c -> 'b) -> 'c Cudd.Vdd.t -> 'a
      val mapleaf2 :
        ('a -> 'b -> 'c) -> 'a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t
      val retractivemapleaf2 :
        default:'a Cudd.Vdd.t ->
        (Cudd.Bdd.vt -> 'b -> 'c -> Cudd.Bdd.vt * 'a) ->
        'b Cudd.Vdd.t -> 'c Cudd.Vdd.t -> 'a Cudd.Vdd.t
      val expansivemapleaf2 :
        default:'a Cudd.Vdd.t ->
        merge:('a Cudd.Vdd.t -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t) ->
        (Cudd.Bdd.vt -> 'b -> 'c -> Cudd.Bdd.vt * 'a) ->
        'b Cudd.Vdd.t -> 'c Cudd.Vdd.t -> 'a Cudd.Vdd.t
      val combineleaf2 :
        default:'a ->
        combine:('b -> 'a -> 'a) ->
        (Cudd.Bdd.vt -> 'c -> 'd -> 'b) ->
        'c Cudd.Vdd.t -> 'd Cudd.Vdd.t -> 'a
      val combineleaf_array :
        default:'a ->
        combine:('b -> 'a -> 'a) ->
        tabsorbant:('c -> bool) option array ->
        (Cudd.Bdd.vt -> 'c array -> 'b) -> 'c Cudd.Vdd.t array -> 'a
      val combineleaf1_array :
        default:'a ->
        combine:('b -> 'a -> 'a) ->
        ?absorbant:('c -> bool) ->
        tabsorbant:('d -> bool) option array ->
        (Cudd.Bdd.vt -> 'c -> 'd array -> 'b) ->
        'c Cudd.Vdd.t -> 'd Cudd.Vdd.t array -> 'a
      val combineleaf2_array :
        default:'a ->
        combine:('b -> 'a -> 'a) ->
        ?absorbant1:('c -> bool) ->
        ?absorbant2:('d -> bool) ->
        tabsorbant:('e -> bool) option array ->
        (Cudd.Bdd.vt -> 'c -> 'd -> 'e array -> 'b) ->
        'c Cudd.Vdd.t -> 'd Cudd.Vdd.t -> 'e Cudd.Vdd.t array -> 'a
      val combineretractive :
        Cudd.Bdd.vt * 'a -> 'a Cudd.Vdd.t -> 'a Cudd.Vdd.t
      val combineexpansive :
        default:'a Cudd.Vdd.t ->
        merge:('a Cudd.Vdd.t -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t) ->
        Cudd.Bdd.vt * 'a -> 'b Cudd.Vdd.t -> 'c Cudd.Vdd.t
    end
  module Add :
    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
end