sig
  exception Bddindex
  type 'a typdef = [ `Benum of 'a array ]
  type 'a typ = [ `Benum of 'a | `Bint of bool * int | `Bool ]
  type 'a symbol = {
    compare : 'a -> 'a -> int;
    marshal : 'a -> string;
    unmarshal : string -> 'a;
    mutable print : Format.formatter -> 'a -> unit;
  }
  type ('a, 'b, 'c, 'd, 'e) t0 = {
    mutable cudd : 'd Cudd.Man.t;
    mutable typdef : ('a, 'c) PMappe.t;
    mutable vartyp : ('a, 'b) PMappe.t;
    mutable bddindex0 : int;
    mutable bddsize : int;
    mutable bddindex : int;
    mutable bddincr : int;
    mutable idcondvar : (int, 'a) PMappe.t;
    mutable vartid : ('a, int array) PMappe.t;
    mutable varset : ('a, 'd Cudd.Bdd.t) PMappe.t;
    mutable print_external_idcondb : Format.formatter -> int * bool -> unit;
    mutable ext : 'e;
    symbol : 'a Bdd.Env.symbol;
    copy_ext : 'e -> 'e;
  }
  module O :
    sig
      type ('a, 'b, 'c, 'd, 'e) t = ('a, 'b, 'c, 'd, 'e) Bdd.Env.t0
        constraint 'b = [> 'a Bdd.Env.typ ]
        constraint 'c = [> 'a Bdd.Env.typdef ]
      val make :
        symbol:'a Bdd.Env.symbol ->
        copy_ext:('e -> 'e) ->
        ?bddindex0:int ->
        ?bddsize:int ->
        ?relational:bool ->
        'd Cudd.Man.t ->
        'e ->
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t
      val print :
        (Format.formatter -> ([> 'a Bdd.Env.typ ] as 'b) -> unit) ->
        (Format.formatter -> ([> 'a Bdd.Env.typdef ] as 'c) -> unit) ->
        (Format.formatter -> 'e -> unit) ->
        Format.formatter -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> unit
    end
  type ('a, 'd) t =
      ('a, 'a Bdd.Env.typ, 'a Bdd.Env.typdef, 'd, unit) Bdd.Env.O.t
  val print_typ :
    (Format.formatter -> 'a -> unit) ->
    Format.formatter -> [> 'a Bdd.Env.typ ] -> unit
  val print_typdef :
    (Format.formatter -> 'a -> unit) ->
    Format.formatter -> [> 'a Bdd.Env.typdef ] -> unit
  val print_tid : Format.formatter -> int array -> unit
  val print_idcondb :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    Format.formatter -> int * bool -> unit
  val print_order :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    Format.formatter -> unit
  val print :
    Format.formatter ->
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    unit
  val marshal : 'a -> string
  val unmarshal : string -> 'a
  val make_symbol :
    ?compare:('a -> 'a -> int) ->
    ?marshal:('a -> string) ->
    ?unmarshal:(string -> 'a) ->
    (Format.formatter -> 'a -> unit) -> 'a Bdd.Env.symbol
  val string_symbol : string Bdd.Env.symbol
  val make :
    symbol:'a Bdd.Env.symbol ->
    ?bddindex0:int ->
    ?bddsize:int -> ?relational:bool -> 'd Cudd.Man.t -> ('a, 'd) Bdd.Env.t
  val make_string :
    ?bddindex0:int ->
    ?bddsize:int ->
    ?relational:bool -> 'd Cudd.Man.t -> (string, 'd) Bdd.Env.t
  val copy :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
    Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
  val mem_typ :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'a -> bool
  val mem_var :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'a -> bool
  val mem_label :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'a -> bool
  val typdef_of_typ :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ] as 'b, 'd, 'e)
    Bdd.Env.O.t -> 'a -> 'b
  val typ_of_var :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ], 'd, 'e)
    Bdd.Env.O.t -> 'a -> 'b
  val vars :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'a PSette.t
  val labels :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'a PSette.t
  val add_typ_with :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ] as 'b, 'd, 'e)
    Bdd.Env.O.t -> 'a -> 'b -> unit
  val add_vars_with :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ], 'd, 'e)
    Bdd.Env.O.t -> ('a * 'b) list -> int array option
  val remove_vars_with :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'a list -> int array option
  val rename_vars_with :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    ('a * 'a) list -> int array option
  val add_typ :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
    Bdd.Env.O.t -> 'a -> 'c -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
  val add_vars :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
    Bdd.Env.O.t -> ('a * 'b) list -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
  val remove_vars :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
    Bdd.Env.O.t -> 'a list -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
  val rename_vars :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
    Bdd.Env.O.t -> ('a * 'a) list -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
  val add_var_with :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ], 'd, 'e)
    Bdd.Env.O.t -> 'a -> 'b -> unit
  val iter_ordered :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    ('a -> int array -> unit) -> unit
  val is_leq :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
    Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> bool
  val is_eq :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
    Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> bool
  val shift :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
    Bdd.Env.O.t -> int -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
  val lce :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
    Bdd.Env.O.t ->
    ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
  val permutation12 :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
    Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> int array
  val permutation21 :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
    Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> int array
  type 'a change = {
    intro : int array option;
    remove : ('a Cudd.Bdd.t * int array) option;
  }
  val compute_change :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
    Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> 'd Bdd.Env.change
  val notfound : ('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'a
  type ('a, 'b) value = { env : 'a; val0 : 'b; }
  val make_value :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
    Bdd.Env.O.t -> 'f -> (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value
  val get_env : ('a, 'b) Bdd.Env.value -> 'a
  val get_val0 : ('a, 'b) Bdd.Env.value -> 'b
  val extend_environment :
    ('f -> int array -> 'f) ->
    (('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
     Bdd.Env.O.t, 'f)
    Bdd.Env.value ->
    ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t ->
    (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value
  val compare_idb : int * bool -> int * bool -> int
  val permutation :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    int array
  val permute_with :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    int array -> unit
  val normalize_with :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    int array
  val check_normalized :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    bool
  val compose_permutation : int array -> int array -> int array
  val compose_opermutation :
    int array option -> int array option -> int array option
  val permutation_of_offset : int -> int -> int array
  val check_var :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'a -> unit
  val check_lvar :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'a list -> unit
  val check_value :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
    Bdd.Env.O.t ->
    (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value -> unit
  val check_value2 :
    (('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
     Bdd.Env.O.t, 'f)
    Bdd.Env.value ->
    (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'g) Bdd.Env.value -> unit
  val check_value3 :
    (('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
     Bdd.Env.O.t, 'f)
    Bdd.Env.value ->
    (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'g) Bdd.Env.value ->
    (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'h) Bdd.Env.value -> unit
  val check_lvarvalue :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
    Bdd.Env.O.t ->
    ('a * (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value) list ->
    ('a * 'f) list
  val check_lvalue :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
    Bdd.Env.O.t ->
    (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value list -> 'f list
  val check_ovalue :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
    Bdd.Env.O.t ->
    (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value option -> 'f option
  val mapunop :
    ('f -> 'g) ->
    (('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
     Bdd.Env.O.t, 'f)
    Bdd.Env.value -> (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'g) Bdd.Env.value
  val mapbinop :
    ('f -> 'g -> 'h) ->
    (('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
     Bdd.Env.O.t, 'f)
    Bdd.Env.value ->
    (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'g) Bdd.Env.value ->
    (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'h) Bdd.Env.value
  val mapbinope :
    (('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
     Bdd.Env.O.t -> 'f -> 'g -> 'h) ->
    (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value ->
    (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'g) Bdd.Env.value ->
    (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'h) Bdd.Env.value
  val mapterop :
    ('f -> 'g -> 'h -> 'i) ->
    (('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'c, 'd, 'e)
     Bdd.Env.O.t, 'f)
    Bdd.Env.value ->
    (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'g) Bdd.Env.value ->
    (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'h) Bdd.Env.value ->
    (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'i) Bdd.Env.value
end