sig
  type 'a typdef = 'a Bdd.Env.typdef
  type 'a typ = [ `Benum of 'a | `Bint of bool * int | `Bool | `Int | `Real ]
  type 'a symbol =
    'a Bdd.Env.symbol = {
    compare : 'a -> 'a -> int;
    marshal : 'a -> string;
    unmarshal : string -> 'a;
    mutable print : Format.formatter -> 'a -> unit;
  }
  type ('a, 'b) ext = {
    mutable table : 'a Bddapron.Apronexpr.t Cudd.Mtbdd.table;
    mutable eapron : Apron.Environment.t;
    mutable aext : 'b;
  }
  type ('a, 'b, 'c, 'd) t0 =
      ('a, 'b, 'c, Cudd.Man.v, ('a, 'd) Bddapron.Env.ext) Bdd.Env.t0
  module O :
    sig
      type ('a, 'b, 'c, 'd) t = ('a, 'b, 'c, 'd) Bddapron.Env.t0
        constraint 'b = [> 'a Bddapron.Env.typ ]
        constraint 'c = [> 'a Bddapron.Env.typdef ]
      val make :
        symbol:'a Bddapron.Env.symbol ->
        copy_aext:('d -> 'd) ->
        ?bddindex0:int ->
        ?bddsize:int ->
        ?relational:bool ->
        Cudd.Man.vt ->
        'd ->
        ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t
      val print :
        (Format.formatter -> ([> 'a Bddapron.Env.typ ] as 'b) -> unit) ->
        (Format.formatter -> ([> 'a Bddapron.Env.typdef ] as 'c) -> unit) ->
        (Format.formatter -> 'd -> unit) ->
        Format.formatter -> ('a, 'b, 'c, 'd) Bddapron.Env.O.t -> unit
    end
  type 'a t =
      ('a, 'a Bddapron.Env.typ, 'a Bddapron.Env.typdef, unit)
      Bddapron.Env.O.t
  val print_typ :
    (Format.formatter -> 'a -> unit) ->
    Format.formatter -> [> 'a Bddapron.Env.typ ] -> unit
  val print_typdef :
    (Format.formatter -> 'a -> unit) ->
    Format.formatter -> [> 'a Bddapron.Env.typdef ] -> unit
  val print_idcondb :
    ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'd)
    Bddapron.Env.O.t -> Format.formatter -> int * bool -> unit
  val print_order :
    ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'd)
    Bddapron.Env.O.t -> Format.formatter -> unit
  val print :
    Format.formatter ->
    ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'd)
    Bddapron.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 Bddapron.Env.symbol
  val string_symbol : string Bddapron.Env.symbol
  val make :
    symbol:'a Bddapron.Env.symbol ->
    ?bddindex0:int ->
    ?bddsize:int -> ?relational:bool -> Cudd.Man.vt -> 'a Bddapron.Env.t
  val make_string :
    ?bddindex0:int ->
    ?bddsize:int -> ?relational:bool -> Cudd.Man.vt -> string Bddapron.Env.t
  val copy :
    ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c,
     'd)
    Bddapron.Env.O.t -> ('a, 'b, 'c, 'd) Bddapron.Env.O.t
  val mem_typ :
    ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'd)
    Bddapron.Env.O.t -> 'a -> bool
  val mem_var :
    ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'd)
    Bddapron.Env.O.t -> 'a -> bool
  val mem_label :
    ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'd)
    Bddapron.Env.O.t -> 'a -> bool
  val typdef_of_typ :
    ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ] as 'b, 'd)
    Bddapron.Env.O.t -> 'a -> 'b
  val typ_of_var :
    ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ], 'd)
    Bddapron.Env.O.t -> 'a -> 'b
  val vars :
    ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'd)
    Bddapron.Env.O.t -> 'a PSette.t
  val labels :
    ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'd)
    Bddapron.Env.O.t -> 'a PSette.t
  val apron :
    ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'd)
    Bddapron.Env.O.t -> Apron.Environment.t
  val add_typ_with :
    ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ] as 'b, 'd)
    Bddapron.Env.O.t -> 'a -> 'b -> unit
  val add_vars_with :
    ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ], 'd)
    Bddapron.Env.O.t -> ('a * 'b) list -> int array option
  val remove_vars_with :
    ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'd)
    Bddapron.Env.O.t -> 'a list -> int array option
  val rename_vars_with :
    ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'd)
    Bddapron.Env.O.t ->
    ('a * 'a) list -> int array option * Apron.Dim.perm option
  val add_typ :
    ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c,
     'd)
    Bddapron.Env.O.t -> 'a -> 'c -> ('a, 'b, 'c, 'd) Bddapron.Env.O.t
  val add_vars :
    ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c,
     'd)
    Bddapron.Env.O.t -> ('a * 'b) list -> ('a, 'b, 'c, 'd) Bddapron.Env.O.t
  val remove_vars :
    ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c,
     'd)
    Bddapron.Env.O.t -> 'a list -> ('a, 'b, 'c, 'd) Bddapron.Env.O.t
  val rename_vars :
    ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c,
     'd)
    Bddapron.Env.O.t -> ('a * 'a) list -> ('a, 'b, 'c, 'd) Bddapron.Env.O.t
  val is_leq :
    ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c,
     'd)
    Bddapron.Env.O.t -> ('a, 'b, 'c, 'd) Bddapron.Env.O.t -> bool
  val is_eq :
    ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c,
     'd)
    Bddapron.Env.O.t -> ('a, 'b, 'c, 'd) Bddapron.Env.O.t -> bool
  val lce :
    ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c,
     'd)
    Bddapron.Env.O.t ->
    ('a, 'b, 'c, 'd) Bddapron.Env.O.t -> ('a, 'b, 'c, 'd) Bddapron.Env.O.t
  type change = {
    cbdd : Cudd.Man.v Bdd.Env.change;
    capron : Apron.Dim.change2;
  }
  val compute_change :
    ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c,
     'd)
    Bddapron.Env.O.t ->
    ('a, 'b, 'c, 'd) Bddapron.Env.O.t -> Bddapron.Env.change
  type ('a, 'b) value = ('a, 'b) Bdd.Env.value = { env : 'a; val0 : 'b; }
  val make_value :
    ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c,
     'd)
    Bddapron.Env.O.t ->
    'e -> (('a, 'b, 'c, 'd) Bddapron.Env.O.t, 'e) Bddapron.Env.value
  val get_env : ('a, 'b) Bddapron.Env.value -> 'a
  val get_val0 : ('a, 'b) Bddapron.Env.value -> 'b
  val check_var :
    ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'd)
    Bddapron.Env.O.t -> 'a -> unit
  val check_lvar :
    ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'd)
    Bddapron.Env.O.t -> 'a list -> unit
  val check_value :
    ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c,
     'd)
    Bddapron.Env.O.t ->
    (('a, 'b, 'c, 'd) Bddapron.Env.O.t, 'e) Bddapron.Env.value -> unit
  val check_value2 :
    (('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c,
      'd)
     Bddapron.Env.O.t, 'e)
    Bddapron.Env.value ->
    (('a, 'b, 'c, 'd) Bddapron.Env.O.t, 'f) Bddapron.Env.value -> unit
  val check_value3 :
    (('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c,
      'd)
     Bddapron.Env.O.t, 'e)
    Bddapron.Env.value ->
    (('a, 'b, 'c, 'd) Bddapron.Env.O.t, 'f) Bddapron.Env.value ->
    (('a, 'b, 'c, 'd) Bddapron.Env.O.t, 'g) Bddapron.Env.value -> unit
  val check_lvarvalue :
    ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c,
     'd)
    Bddapron.Env.O.t ->
    ('a * (('a, 'b, 'c, 'd) Bddapron.Env.O.t, 'e) Bddapron.Env.value) list ->
    ('a * 'e) list
  val check_lvalue :
    ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c,
     'd)
    Bddapron.Env.O.t ->
    (('a, 'b, 'c, 'd) Bddapron.Env.O.t, 'e) Bddapron.Env.value list ->
    'e list
  val check_ovalue :
    ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c,
     'd)
    Bddapron.Env.O.t ->
    (('a, 'b, 'c, 'd) Bddapron.Env.O.t, 'e) Bddapron.Env.value option ->
    'e option
  val mapunop :
    ('e -> 'f) ->
    (('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c,
      'd)
     Bddapron.Env.O.t, 'e)
    Bddapron.Env.value ->
    (('a, 'b, 'c, 'd) Bddapron.Env.O.t, 'f) Bddapron.Env.value
  val mapbinop :
    ('e -> 'f -> 'g) ->
    (('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c,
      'd)
     Bddapron.Env.O.t, 'e)
    Bddapron.Env.value ->
    (('a, 'b, 'c, 'd) Bddapron.Env.O.t, 'f) Bddapron.Env.value ->
    (('a, 'b, 'c, 'd) Bddapron.Env.O.t, 'g) Bddapron.Env.value
  val mapbinope :
    (('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c,
      'd)
     Bddapron.Env.O.t -> 'e -> 'f -> 'g) ->
    (('a, 'b, 'c, 'd) Bddapron.Env.O.t, 'e) Bddapron.Env.value ->
    (('a, 'b, 'c, 'd) Bddapron.Env.O.t, 'f) Bddapron.Env.value ->
    (('a, 'b, 'c, 'd) Bddapron.Env.O.t, 'g) Bddapron.Env.value
  val mapterop :
    ('e -> 'f -> 'g -> 'h) ->
    (('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c,
      'd)
     Bddapron.Env.O.t, 'e)
    Bddapron.Env.value ->
    (('a, 'b, 'c, 'd) Bddapron.Env.O.t, 'f) Bddapron.Env.value ->
    (('a, 'b, 'c, 'd) Bddapron.Env.O.t, 'g) Bddapron.Env.value ->
    (('a, 'b, 'c, 'd) Bddapron.Env.O.t, 'h) Bddapron.Env.value
  val var_of_aprondim :
    ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'd)
    Bddapron.Env.O.t -> Apron.Dim.t -> 'a
  val aprondim_of_var :
    ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'd)
    Bddapron.Env.O.t -> 'a -> Apron.Dim.t
  val string_of_aprondim :
    ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'd)
    Bddapron.Env.O.t -> Apron.Dim.t -> string
end