sig
  module type Level0 =
    sig
      type ('a, 'b) man
      type 'b t
      val size :
        ('a, 'b) Bddapron.Domainlevel1.Level0.man ->
        'b Bddapron.Domainlevel1.Level0.t -> int
      val print :
        ?print_apron:((int -> string) ->
                      Format.formatter -> 'b Apron.Abstract0.t -> unit) ->
        'a Bddapron.Env.t ->
        Format.formatter -> 'b Bddapron.Domainlevel1.Level0.t -> unit
      val bottom :
        ('a, 'b) Bddapron.Domainlevel1.Level0.man ->
        'a Bddapron.Env.t -> 'b Bddapron.Domainlevel1.Level0.t
      val top :
        ('a, 'b) Bddapron.Domainlevel1.Level0.man ->
        'a Bddapron.Env.t -> 'b Bddapron.Domainlevel1.Level0.t
      val of_apron :
        ('a, 'b) Bddapron.Domainlevel1.Level0.man ->
        'a Bddapron.Env.t ->
        'b Apron.Abstract0.t -> 'b Bddapron.Domainlevel1.Level0.t
      val of_bddapron :
        ('a, 'b) Bddapron.Domainlevel1.Level0.man ->
        'a Bddapron.Env.t ->
        ('a Bddapron.Expr0.Bool.t * 'b Apron.Abstract0.t) list ->
        'b Bddapron.Domainlevel1.Level0.t
      val is_bottom :
        ('a, 'b) Bddapron.Domainlevel1.Level0.man ->
        'b Bddapron.Domainlevel1.Level0.t -> bool
      val is_top :
        ('a, 'b) Bddapron.Domainlevel1.Level0.man ->
        'b Bddapron.Domainlevel1.Level0.t -> bool
      val is_leq :
        ('a, 'b) Bddapron.Domainlevel1.Level0.man ->
        'b Bddapron.Domainlevel1.Level0.t ->
        'b Bddapron.Domainlevel1.Level0.t -> bool
      val is_eq :
        ('a, 'b) Bddapron.Domainlevel1.Level0.man ->
        'b Bddapron.Domainlevel1.Level0.t ->
        'b Bddapron.Domainlevel1.Level0.t -> bool
      val to_bddapron :
        ('a, 'b) Bddapron.Domainlevel1.Level0.man ->
        'b Bddapron.Domainlevel1.Level0.t ->
        ('a Bddapron.Expr0.Bool.t * 'b Apron.Abstract0.t) list
      val meet :
        ('a, 'b) Bddapron.Domainlevel1.Level0.man ->
        'b Bddapron.Domainlevel1.Level0.t ->
        'b Bddapron.Domainlevel1.Level0.t ->
        'b Bddapron.Domainlevel1.Level0.t
      val join :
        ('a, 'b) Bddapron.Domainlevel1.Level0.man ->
        'b Bddapron.Domainlevel1.Level0.t ->
        'b Bddapron.Domainlevel1.Level0.t ->
        'b Bddapron.Domainlevel1.Level0.t
      val meet_condition :
        ('a, 'b) Bddapron.Domainlevel1.Level0.man ->
        'a Bddapron.Env.t ->
        'a Bddapron.Cond.t ->
        'b Bddapron.Domainlevel1.Level0.t ->
        'a Bddapron.Expr0.Bool.t -> 'b Bddapron.Domainlevel1.Level0.t
      val assign_lexpr :
        ?relational:bool ->
        ?nodependency:bool ->
        ('a, 'b) Bddapron.Domainlevel1.Level0.man ->
        'a Bddapron.Env.t ->
        'a Bddapron.Cond.t ->
        'b Bddapron.Domainlevel1.Level0.t ->
        'a list ->
        'a Bddapron.Expr0.t list ->
        'b Bddapron.Domainlevel1.Level0.t option ->
        'b Bddapron.Domainlevel1.Level0.t
      val substitute_lexpr :
        ('a, 'b) Bddapron.Domainlevel1.Level0.man ->
        'a Bddapron.Env.t ->
        'a Bddapron.Cond.t ->
        'b Bddapron.Domainlevel1.Level0.t ->
        'a list ->
        'a Bddapron.Expr0.t list ->
        'b Bddapron.Domainlevel1.Level0.t option ->
        'b Bddapron.Domainlevel1.Level0.t
      val forget_list :
        ('a, 'b) Bddapron.Domainlevel1.Level0.man ->
        'a Bddapron.Env.t ->
        'b Bddapron.Domainlevel1.Level0.t ->
        'a list -> 'b Bddapron.Domainlevel1.Level0.t
      val widening :
        ('a, 'b) Bddapron.Domainlevel1.Level0.man ->
        'b Bddapron.Domainlevel1.Level0.t ->
        'b Bddapron.Domainlevel1.Level0.t ->
        'b Bddapron.Domainlevel1.Level0.t
      val widening_threshold :
        ('a, 'b) Bddapron.Domainlevel1.Level0.man ->
        'b Bddapron.Domainlevel1.Level0.t ->
        'b Bddapron.Domainlevel1.Level0.t ->
        Apron.Lincons0.t array -> 'b Bddapron.Domainlevel1.Level0.t
      val apply_change :
        bottom:'b Bddapron.Domainlevel1.Level0.t ->
        ('a, 'b) Bddapron.Domainlevel1.Level0.man ->
        'b Bddapron.Domainlevel1.Level0.t ->
        Bddapron.Env.change -> 'b Bddapron.Domainlevel1.Level0.t
      val apply_permutation :
        ('a, 'b) Bddapron.Domainlevel1.Level0.man ->
        'b Bddapron.Domainlevel1.Level0.t ->
        int array option * Apron.Dim.perm option ->
        'b Bddapron.Domainlevel1.Level0.t
    end
  module type Level1 =
    sig
      type ('a, 'b) man
      type 'b t0
      type ('a, 'b) t =
          ('a Bddapron.Env.t, 'b Bddapron.Domainlevel1.Level1.t0)
          Bddapron.Env.value
      val get_env :
        ('a, 'b) Bddapron.Domainlevel1.Level1.t -> 'a Bddapron.Env.t
      val to_level0 :
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        'b Bddapron.Domainlevel1.Level1.t0
      val of_level0 :
        'a Bddapron.Env.t ->
        'b Bddapron.Domainlevel1.Level1.t0 ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t
      val size :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t -> int
      val print :
        ?print_apron:((int -> string) ->
                      Format.formatter -> 'b Apron.Abstract0.t -> unit) ->
        Format.formatter -> ('a, 'b) Bddapron.Domainlevel1.Level1.t -> unit
      val bottom :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        'a Bddapron.Env.t -> ('a, 'b) Bddapron.Domainlevel1.Level1.t
      val top :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        'a Bddapron.Env.t -> ('a, 'b) Bddapron.Domainlevel1.Level1.t
      val of_apron :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        'a Bddapron.Env.t ->
        'b Apron.Abstract1.t -> ('a, 'b) Bddapron.Domainlevel1.Level1.t
      val of_bddapron :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        'a Bddapron.Env.t ->
        ('a Bddapron.Expr1.Bool.t * 'b Apron.Abstract1.t) list ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t
      val is_bottom :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t -> bool
      val is_top :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t -> bool
      val is_leq :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t -> bool
      val is_eq :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t -> bool
      val to_bddapron :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        ('a Bddapron.Expr1.Bool.t * 'b Apron.Abstract1.t) list
      val meet :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t
      val join :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t
      val meet_condition :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        'a Bddapron.Cond.t ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        'a Bddapron.Expr1.Bool.t -> ('a, 'b) Bddapron.Domainlevel1.Level1.t
      val meet_condition2 :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        'a Bddapron.Expr2.Bool.t -> ('a, 'b) Bddapron.Domainlevel1.Level1.t
      val assign_lexpr :
        ?relational:bool ->
        ?nodependency:bool ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        'a Bddapron.Cond.t ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        'a list ->
        'a Bddapron.Expr1.t list ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t option ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t
      val assign_listexpr2 :
        ?relational:bool ->
        ?nodependency:bool ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        'a list ->
        'a Bddapron.Expr2.List.t ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t option ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t
      val substitute_lexpr :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        'a Bddapron.Cond.t ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        'a list ->
        'a Bddapron.Expr1.t list ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t option ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t
      val substitute_listexpr2 :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        'a list ->
        'a Bddapron.Expr2.List.t ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t option ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t
      val forget_list :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        'a list -> ('a, 'b) Bddapron.Domainlevel1.Level1.t
      val widening :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t
      val widening_threshold :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        Apron.Lincons1.earray -> ('a, 'b) Bddapron.Domainlevel1.Level1.t
      val change_environment :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        'a Bddapron.Env.t -> ('a, 'b) Bddapron.Domainlevel1.Level1.t
      val rename :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        ('a * 'a) list -> ('a, 'b) Bddapron.Domainlevel1.Level1.t
      val unify :
        ('a, 'b) Bddapron.Domainlevel1.Level1.man ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t ->
        ('a, 'b) Bddapron.Domainlevel1.Level1.t
    end
  module Make :
    functor (Level0 : Level0) ->
      sig
        type ('a, 'b) man = ('a, 'b) Level0.man
        type 'b t0 = 'b Level0.t
        type ('a, 'b) t = ('a Env.t, 'b t0) Env.value
        val get_env : ('a, 'b) t -> 'a Env.t
        val to_level0 : ('a, 'b) t -> 'b t0
        val of_level0 : 'a Env.t -> 'b t0 -> ('a, 'b) t
        val size : ('a, 'b) man -> ('a, 'b) t -> int
        val print :
          ?print_apron:((int -> string) ->
                        Format.formatter -> 'b Apron.Abstract0.t -> unit) ->
          Format.formatter -> ('a, 'b) t -> unit
        val bottom : ('a, 'b) man -> 'a Env.t -> ('a, 'b) t
        val top : ('a, 'b) man -> 'a Env.t -> ('a, 'b) t
        val of_apron :
          ('a, 'b) man -> 'a Env.t -> 'b Apron.Abstract1.t -> ('a, 'b) t
        val of_bddapron :
          ('a, 'b) man ->
          'a Env.t ->
          ('a Expr1.Bool.t * 'b Apron.Abstract1.t) list -> ('a, 'b) t
        val is_bottom : ('a, 'b) man -> ('a, 'b) t -> bool
        val is_top : ('a, 'b) man -> ('a, 'b) t -> bool
        val is_leq : ('a, 'b) man -> ('a, 'b) t -> ('a, 'b) t -> bool
        val is_eq : ('a, 'b) man -> ('a, 'b) t -> ('a, 'b) t -> bool
        val to_bddapron :
          ('a, 'b) man ->
          ('a, 'b) t -> ('a Expr1.Bool.t * 'b Apron.Abstract1.t) list
        val meet : ('a, 'b) man -> ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) t
        val join : ('a, 'b) man -> ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) t
        val meet_condition :
          ('a, 'b) man ->
          'a Cond.t -> ('a, 'b) t -> 'a Expr1.Bool.t -> ('a, 'b) t
        val meet_condition2 :
          ('a, 'b) man -> ('a, 'b) t -> 'a Expr2.Bool.t -> ('a, 'b) t
        val assign_lexpr :
          ?relational:bool ->
          ?nodependency:bool ->
          ('a, 'b) man ->
          'a Cond.t ->
          ('a, 'b) t ->
          'a list -> 'a Expr1.t list -> ('a, 'b) t option -> ('a, 'b) t
        val assign_listexpr2 :
          ?relational:bool ->
          ?nodependency:bool ->
          ('a, 'b) man ->
          ('a, 'b) t ->
          'a list -> 'a Expr2.List.t -> ('a, 'b) t option -> ('a, 'b) t
        val substitute_lexpr :
          ('a, 'b) man ->
          'a Cond.t ->
          ('a, 'b) t ->
          'a list -> 'a Expr1.t list -> ('a, 'b) t option -> ('a, 'b) t
        val substitute_listexpr2 :
          ('a, 'b) man ->
          ('a, 'b) t ->
          'a list -> 'a Expr2.List.t -> ('a, 'b) t option -> ('a, 'b) t
        val forget_list : ('a, 'b) man -> ('a, 'b) t -> 'a list -> ('a, 'b) t
        val widening : ('a, 'b) man -> ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) t
        val widening_threshold :
          ('a, 'b) man ->
          ('a, 'b) t -> ('a, 'b) t -> Apron.Lincons1.earray -> ('a, 'b) t
        val change_environment :
          ('a, 'b) man -> ('a, 'b) t -> 'a Env.t -> ('a, 'b) t
        val rename :
          ('a, 'b) man -> ('a, 'b) t -> ('a * 'a) list -> ('a, 'b) t
        val unify : ('a, 'b) man -> ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) t
      end
end