sig
  type ('a, 'b, 'c, 'd) man = ('a, 'b, 'c, 'd) Domain0.man
  type ('a, 'b) mtbdd =
      ('a, 'b, ('a, 'b) Mtbdddomain0.man, 'b Mtbdddomain0.t) Domain1.man
  type ('a, 'b) bdd =
      ('a, 'b, ('a, 'b) Bdddomain0.man, 'b Bdddomain0.t) Domain1.man
  type ('a, 'b) t = ('a Env.t, 'b) Env.value
  val canonicalize :
    ?apron:bool -> ('a, 'b, 'c, 'd) Domain1.man -> ('a, 'd) Domain1.t -> unit
  val print :
    ?print_apron:((int -> string) ->
                  Format.formatter -> 'a Apron.Abstract0.t -> unit) ->
    ('b, 'a, 'c, 'd) Domain1.man ->
    Format.formatter -> ('b, 'd) Domain1.t -> unit
  val get_env : ('a, 'b) Domain1.t -> 'a Env.t
  val to_level0 : ('a, 'b) Domain1.t -> 'b
  val size : ('a, 'b, 'c, 'd) Domain1.man -> ('a, 'd) Domain1.t -> int
  val bottom : ('a, 'b, 'c, 'd) Domain1.man -> 'a Env.t -> ('a, 'd) Domain1.t
  val top : ('a, 'b, 'c, 'd) Domain1.man -> 'a Env.t -> ('a, 'd) Domain1.t
  val of_apron :
    ('a, 'b, 'c, 'd) Domain1.man ->
    'a Env.t -> 'b Apron.Abstract1.t -> ('a, 'd) Domain1.t
  val is_bottom : ('a, 'b, 'c, 'd) Domain1.man -> ('a, 'd) Domain1.t -> bool
  val is_top : ('a, 'b, 'c, 'd) Domain1.man -> ('a, 'd) Domain1.t -> bool
  val is_leq :
    ('a, 'b, 'c, 'd) Domain1.man ->
    ('a, 'd) Domain1.t -> ('a, 'd) Domain1.t -> bool
  val is_eq :
    ('a, 'b, 'c, 'd) Domain1.man ->
    ('a, 'd) Domain1.t -> ('a, 'd) Domain1.t -> bool
  val to_bddapron :
    ('a, 'b, 'c, 'd) Domain1.man ->
    ('a, 'd) Domain1.t -> ('a Expr1.Bool.t * 'b Apron.Abstract1.t) list
  val meet :
    ('a, 'b, 'c, 'd) Domain1.man ->
    ('a, 'd) Domain1.t -> ('a, 'd) Domain1.t -> ('a, 'd) Domain1.t
  val join :
    ('a, 'b, 'c, 'd) Domain1.man ->
    ('a, 'd) Domain1.t -> ('a, 'd) Domain1.t -> ('a, 'd) Domain1.t
  val meet_condition :
    ('a, 'b, 'c, 'd) Domain1.man ->
    'a Cond.t -> ('a, 'd) Domain1.t -> 'a Expr1.Bool.t -> ('a, 'd) Domain1.t
  val meet_condition2 :
    ('a, 'b, 'c, 'd) Domain1.man ->
    ('a, 'd) Domain1.t -> 'a Expr2.Bool.t -> ('a, 'd) Domain1.t
  val assign_lexpr :
    ?relational:bool ->
    ?nodependency:bool ->
    ('a, 'b, 'c, 'd) Domain1.man ->
    'a Cond.t ->
    ('a, 'd) Domain1.t ->
    'a list ->
    'a Expr1.t list -> ('a, 'd) Domain1.t option -> ('a, 'd) Domain1.t
  val assign_listexpr2 :
    ?relational:bool ->
    ?nodependency:bool ->
    ('a, 'b, 'c, 'd) Domain1.man ->
    ('a, 'd) Domain1.t ->
    'a list ->
    'a Expr2.List.t -> ('a, 'd) Domain1.t option -> ('a, 'd) Domain1.t
  val substitute_lexpr :
    ('a, 'b, 'c, 'd) Domain1.man ->
    'a Cond.t ->
    ('a, 'd) Domain1.t ->
    'a list ->
    'a Expr1.t list -> ('a, 'd) Domain1.t option -> ('a, 'd) Domain1.t
  val substitute_listexpr2 :
    ('a, 'b, 'c, 'd) Domain1.man ->
    ('a, 'd) Domain1.t ->
    'a list ->
    'a Expr2.List.t -> ('a, 'd) Domain1.t option -> ('a, 'd) Domain1.t
  val forget_list :
    ('a, 'b, 'c, 'd) Domain1.man ->
    ('a, 'd) Domain1.t -> 'a list -> ('a, 'd) Domain1.t
  val widening :
    ('a, 'b, 'c, 'd) Domain1.man ->
    ('a, 'd) Domain1.t -> ('a, 'd) Domain1.t -> ('a, 'd) Domain1.t
  val change_environment :
    ('a, 'b, 'c, 'd) Domain1.man ->
    ('a, 'd) Domain1.t -> 'a Env.t -> ('a, 'd) Domain1.t
  val unify :
    ('a, 'b, 'c, 'd) Domain1.man ->
    ('a, 'd) Domain1.t -> ('a, 'd) Domain1.t -> ('a, 'd) Domain1.t
  val rename :
    ('a, 'b, 'c, 'd) Domain1.man ->
    ('a, 'd) Domain1.t -> ('a * 'a) list -> ('a, 'd) Domain1.t
  val make_mtbdd :
    ?global:bool -> 'a Apron.Manager.t -> ('b, 'a) Domain0.mtbdd
  val man_is_mtbdd : ('a, 'b, 'c, 'd) Domain1.man -> bool
  val man_of_mtbdd : ('a, 'b) Domain1.mtbdd -> ('a, 'b, 'c, 'd) Domain1.man
  val man_to_mtbdd : ('a, 'b, 'c, 'd) Domain1.man -> ('a, 'b) Domain1.mtbdd
  val of_mtbdd :
    ('a, 'b) Domain1.mtbdd * ('a, 'b Mtbdddomain0.t) Domain1.t ->
    ('a, 'b, 'c, 'd) Domain1.man * ('a, 'd) Domain1.t
  val to_mtbdd :
    ('a, 'b, 'c, 'd) Domain1.man * ('a, 'd) Domain1.t ->
    ('a, 'b) Domain1.mtbdd * ('a, 'b Mtbdddomain0.t) Domain1.t
  val make_bdd : 'a Apron.Manager.t -> ('b, 'a) Domain1.bdd
  val man_is_bdd : ('a, 'b, 'c, 'd) Domain1.man -> bool
  val man_of_bdd : ('a, 'b) Domain1.bdd -> ('a, 'b, 'c, 'd) Domain1.man
  val man_to_bdd : ('a, 'b, 'c, 'd) Domain1.man -> ('a, 'b) Domain1.bdd
  val of_bdd :
    ('a, 'b) Domain1.bdd * ('a, 'b Bdddomain0.t) Domain1.t ->
    ('a, 'b, 'c, 'd) Domain1.man * ('a, 'd) Domain1.t
  val to_bdd :
    ('a, 'b, 'c, 'd) Domain1.man * ('a, 'd) Domain1.t ->
    ('a, 'b) Domain1.bdd * ('a, 'b Bdddomain0.t) Domain1.t
end