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 Env.symbol;
    copy_ext : 'e -> 'e;
  }
  module O :
    sig
      type ('a, 'b, 'c, 'd, 'e) t = ('a, 'b, 'c, 'd, 'e) Env.t0
        constraint 'b = [> 'a Env.typ ] constraint 'c = [> 'a Env.typdef ]
      val make :
        symbol:'a Env.symbol ->
        copy_ext:('b -> 'b) ->
        ?bddindex0:int ->
        ?bddsize:int ->
        ?relational:bool ->
        'c Cudd.Man.t ->
        'b -> ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'c, 'b) Env.O.t
      val print :
        (Format.formatter -> ([> 'b Env.typ ] as 'a) -> unit) ->
        (Format.formatter -> ([> 'b Env.typdef ] as 'c) -> unit) ->
        (Format.formatter -> 'd -> unit) ->
        Format.formatter -> ('b, 'a, 'c, 'e, 'd) Env.O.t -> unit
    end
  type ('a, 'b) t = ('a, 'a Env.typ, 'a Env.typdef, 'b, unit) Env.O.t
  val print_typ :
    (Format.formatter -> 'a -> unit) ->
    Format.formatter -> [> 'a Env.typ ] -> unit
  val print_typdef :
    (Format.formatter -> 'a -> unit) ->
    Format.formatter -> [> 'a Env.typdef ] -> unit
  val print_tid : Format.formatter -> int array -> unit
  val print_idcondb :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    Format.formatter -> int * bool -> unit
  val print_order :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    Format.formatter -> unit
  val print :
    Format.formatter ->
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) 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 Env.symbol
  val string_symbol : string Env.symbol
  val make :
    symbol:'a Env.symbol ->
    ?bddindex0:int ->
    ?bddsize:int -> ?relational:bool -> 'b Cudd.Man.t -> ('a, 'b) Env.t
  val make_string :
    ?bddindex0:int ->
    ?bddsize:int -> ?relational:bool -> 'a Cudd.Man.t -> (string, 'a) Env.t
  val copy :
    ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t ->
    ('a, 'b, 'c, 'd, 'e) Env.O.t
  val mem_typ :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t -> 'a -> bool
  val mem_var :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t -> 'a -> bool
  val mem_label :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t -> 'a -> bool
  val typdef_of_typ :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ] as 'b, 'c, 'd) Env.O.t ->
    'a -> 'b
  val typ_of_var :
    ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ], 'c, 'd) Env.O.t ->
    'a -> 'b
  val vars :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t -> 'a PSette.t
  val labels :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t -> 'a PSette.t
  val add_typ_with :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ] as 'b, 'c, 'd) Env.O.t ->
    'a -> 'b -> unit
  val add_vars_with :
    ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ], 'c, 'd) Env.O.t ->
    ('a * 'b) list -> int array option
  val remove_vars_with :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    'a list -> int array option
  val rename_vars_with :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    ('a * 'a) list -> int array option
  val add_typ :
    ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t ->
    'a -> 'c -> ('a, 'b, 'c, 'd, 'e) Env.O.t
  val add_vars :
    ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t ->
    ('a * 'b) list -> ('a, 'b, 'c, 'd, 'e) Env.O.t
  val remove_vars :
    ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t ->
    'a list -> ('a, 'b, 'c, 'd, 'e) Env.O.t
  val rename_vars :
    ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t ->
    ('a * 'a) list -> ('a, 'b, 'c, 'd, 'e) Env.O.t
  val add_var_with :
    ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ], 'c, 'd) Env.O.t ->
    'a -> 'b -> unit
  val iter_ordered :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    ('a -> int array -> unit) -> unit
  val is_leq :
    ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t ->
    ('a, 'b, 'c, 'd, 'e) Env.O.t -> bool
  val is_eq :
    ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t ->
    ('a, 'b, 'c, 'd, 'e) Env.O.t -> bool
  val shift :
    ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t ->
    int -> ('a, 'b, 'c, 'd, 'e) Env.O.t
  val lce :
    ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t ->
    ('a, 'b, 'c, 'd, 'e) Env.O.t -> ('a, 'b, 'c, 'd, 'e) Env.O.t
  val permutation12 :
    ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t ->
    ('a, 'b, 'c, 'd, 'e) Env.O.t -> int array
  val permutation21 :
    ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t ->
    ('a, 'b, 'c, 'd, 'e) 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 Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t ->
    ('a, 'b, 'c, 'd, 'e) Env.O.t -> 'd 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 Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t ->
    'f -> (('a, 'b, 'c, 'd, 'e) Env.O.t, 'f) Env.value
  val get_env : ('a, 'b) Env.value -> 'a
  val get_val0 : ('a, 'b) Env.value -> 'b
  val extend_environment :
    ('a -> int array -> 'a) ->
    (('b, [> 'b Env.typ ] as 'c, [> 'b Env.typdef ] as 'd, 'e, 'f) Env.O.t,
     'a)
    Env.value ->
    ('b, 'c, 'd, 'e, 'f) Env.O.t ->
    (('b, 'c, 'd, 'e, 'f) Env.O.t, 'a) Env.value
  val compare_idb : int * bool -> int * bool -> int
  val permutation :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t -> int array
  val permute_with :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    int array -> unit
  val normalize_with :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t -> int array
  val check_normalized :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) 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 Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t -> 'a -> unit
  val check_lvar :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    'a list -> unit
  val check_value :
    ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t ->
    (('a, 'b, 'c, 'd, 'e) Env.O.t, 'f) Env.value -> unit
  val check_value2 :
    (('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t,
     'f)
    Env.value -> (('a, 'b, 'c, 'd, 'e) Env.O.t, 'g) Env.value -> unit
  val check_value3 :
    (('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t,
     'f)
    Env.value ->
    (('a, 'b, 'c, 'd, 'e) Env.O.t, 'g) Env.value ->
    (('a, 'b, 'c, 'd, 'e) Env.O.t, 'h) Env.value -> unit
  val check_lvarvalue :
    ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t ->
    ('a * (('a, 'b, 'c, 'd, 'e) Env.O.t, 'f) Env.value) list ->
    ('a * 'f) list
  val check_lvalue :
    ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t ->
    (('a, 'b, 'c, 'd, 'e) Env.O.t, 'f) Env.value list -> 'f list
  val check_ovalue :
    ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t ->
    (('a, 'b, 'c, 'd, 'e) Env.O.t, 'f) Env.value option -> 'f option
  val mapunop :
    ('a -> 'b) ->
    (('c, [> 'c Env.typ ] as 'd, [> 'c Env.typdef ] as 'e, 'f, 'g) Env.O.t,
     'a)
    Env.value -> (('c, 'd, 'e, 'f, 'g) Env.O.t, 'b) Env.value
  val mapbinop :
    ('a -> 'b -> 'c) ->
    (('d, [> 'd Env.typ ] as 'e, [> 'd Env.typdef ] as 'f, 'g, 'h) Env.O.t,
     'a)
    Env.value ->
    (('d, 'e, 'f, 'g, 'h) Env.O.t, 'b) Env.value ->
    (('d, 'e, 'f, 'g, 'h) Env.O.t, 'c) Env.value
  val mapbinope :
    (('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd, 'e) Env.O.t ->
     'f -> 'g -> 'h) ->
    (('a, 'b, 'c, 'd, 'e) Env.O.t, 'f) Env.value ->
    (('a, 'b, 'c, 'd, 'e) Env.O.t, 'g) Env.value ->
    (('a, 'b, 'c, 'd, 'e) Env.O.t, 'h) Env.value
  val mapterop :
    ('a -> 'b -> 'c -> 'd) ->
    (('e, [> 'e Env.typ ] as 'f, [> 'e Env.typdef ] as 'g, 'h, 'i) Env.O.t,
     'a)
    Env.value ->
    (('e, 'f, 'g, 'h, 'i) Env.O.t, 'b) Env.value ->
    (('e, 'f, 'g, 'h, 'i) Env.O.t, 'c) Env.value ->
    (('e, 'f, 'g, 'h, 'i) Env.O.t, 'd) Env.value
end