sig
  type ('a, 'b) man = {
    apron : 'b Apron.Manager.t;
    mutable bdd_restrict : Cudd.Bdd.vt -> Cudd.Bdd.vt -> Cudd.Bdd.vt;
    mutable expr_restrict :
      'a Bddapron.Expr0.t -> Cudd.Bdd.vt -> 'a Bddapron.Expr0.t;
    mutable meet_disjoint : bool;
    mutable join_disjoint : bool;
    mutable meet_cond_unique : bool;
    mutable meet_cond_disjoint : bool;
    mutable meet_cond_depth : int;
    mutable assign_unique : bool;
    mutable assign_disjoint : bool;
    mutable substitute_unique : bool;
    mutable substitute_disjoint : bool;
    mutable forget_unique : bool;
    mutable forget_disjoint : bool;
    mutable change_environment_unique : bool;
    mutable change_environment_disjoint : bool;
  }
  type 'b elt = (Cudd.Man.v, 'b Apron.Abstract0.t) Bddapron.Bddleaf.elt
  type 'b t = {
    mutable list : 'b Bddapron.Bdddomain0.elt list;
    bottom : 'b Bddapron.Bdddomain0.elt;
    mutable unique : bool;
    mutable disjoint : bool;
  }
  val make_man : 'b Apron.Manager.t -> ('a, 'b) Bddapron.Bdddomain0.man
  val canonicalize :
    ?apron:bool ->
    ?unique:bool ->
    ?disjoint:bool ->
    ('a, 'b) Bddapron.Bdddomain0.man -> 'b Bddapron.Bdddomain0.t -> unit
  val size :
    ('a, 'b) Bddapron.Bdddomain0.man -> 'b Bddapron.Bdddomain0.t -> int
  val print :
    ?print_apron:((int -> string) ->
                  Format.formatter -> 'b Apron.Abstract0.t -> unit) ->
    'a Bddapron.Env.t -> Format.formatter -> 'b Bddapron.Bdddomain0.t -> unit
  val bottom :
    ('a, 'b) Bddapron.Bdddomain0.man ->
    'a Bddapron.Env.t -> 'b Bddapron.Bdddomain0.t
  val top :
    ('a, 'b) Bddapron.Bdddomain0.man ->
    'a Bddapron.Env.t -> 'b Bddapron.Bdddomain0.t
  val of_apron :
    ('a, 'b) Bddapron.Bdddomain0.man ->
    'a Bddapron.Env.t -> 'b Apron.Abstract0.t -> 'b Bddapron.Bdddomain0.t
  val of_bddapron :
    ('a, 'b) Bddapron.Bdddomain0.man ->
    'a Bddapron.Env.t ->
    ('a Bddapron.Expr0.Bool.t * 'b Apron.Abstract0.t) list ->
    'b Bddapron.Bdddomain0.t
  val is_bottom :
    ('a, 'b) Bddapron.Bdddomain0.man -> 'b Bddapron.Bdddomain0.t -> bool
  val is_top :
    ('a, 'b) Bddapron.Bdddomain0.man -> 'b Bddapron.Bdddomain0.t -> bool
  val is_leq :
    ('a, 'b) Bddapron.Bdddomain0.man ->
    'b Bddapron.Bdddomain0.t -> 'b Bddapron.Bdddomain0.t -> bool
  val is_eq :
    ('a, 'b) Bddapron.Bdddomain0.man ->
    'b Bddapron.Bdddomain0.t -> 'b Bddapron.Bdddomain0.t -> bool
  val to_bddapron :
    ('a, 'b) Bddapron.Bdddomain0.man ->
    'b Bddapron.Bdddomain0.t ->
    ('a Bddapron.Expr0.Bool.t * 'b Apron.Abstract0.t) list
  val meet :
    ('a, 'b) Bddapron.Bdddomain0.man ->
    'b Bddapron.Bdddomain0.t ->
    'b Bddapron.Bdddomain0.t -> 'b Bddapron.Bdddomain0.t
  val join :
    ('a, 'b) Bddapron.Bdddomain0.man ->
    'b Bddapron.Bdddomain0.t ->
    'b Bddapron.Bdddomain0.t -> 'b Bddapron.Bdddomain0.t
  val meet_condition :
    ('a, 'b) Bddapron.Bdddomain0.man ->
    'a Bddapron.Env.t ->
    'a Bddapron.Cond.t ->
    'b Bddapron.Bdddomain0.t ->
    'a Bddapron.Expr0.Bool.t -> 'b Bddapron.Bdddomain0.t
  val assign_lexpr :
    ?relational:bool ->
    ?nodependency:bool ->
    ('a, 'b) Bddapron.Bdddomain0.man ->
    'a Bddapron.Env.t ->
    'a Bddapron.Cond.t ->
    'b Bddapron.Bdddomain0.t ->
    'a list ->
    'a Bddapron.Expr0.t list ->
    'b Bddapron.Bdddomain0.t option -> 'b Bddapron.Bdddomain0.t
  val substitute_lexpr :
    ('a, 'b) Bddapron.Bdddomain0.man ->
    'a Bddapron.Env.t ->
    'a Bddapron.Cond.t ->
    'b Bddapron.Bdddomain0.t ->
    'a list ->
    'a Bddapron.Expr0.t list ->
    'b Bddapron.Bdddomain0.t option -> 'b Bddapron.Bdddomain0.t
  val forget_list :
    ('a, 'b) Bddapron.Bdddomain0.man ->
    'a Bddapron.Env.t ->
    'b Bddapron.Bdddomain0.t -> 'a list -> 'b Bddapron.Bdddomain0.t
  val widening :
    ('a, 'b) Bddapron.Bdddomain0.man ->
    'b Bddapron.Bdddomain0.t ->
    'b Bddapron.Bdddomain0.t -> 'b Bddapron.Bdddomain0.t
  val widening_threshold :
    ('a, 'b) Bddapron.Bdddomain0.man ->
    'b Bddapron.Bdddomain0.t ->
    'b Bddapron.Bdddomain0.t ->
    Apron.Lincons0.t array -> 'b Bddapron.Bdddomain0.t
  val apply_change :
    bottom:'b Bddapron.Bdddomain0.t ->
    ('a, 'b) Bddapron.Bdddomain0.man ->
    'b Bddapron.Bdddomain0.t ->
    Bddapron.Env.change -> 'b Bddapron.Bdddomain0.t
  val apply_permutation :
    ('a, 'b) Bddapron.Bdddomain0.man ->
    'b Bddapron.Bdddomain0.t ->
    int array option * Apron.Dim.perm option -> 'b Bddapron.Bdddomain0.t
  module O :
    sig
      module L :
        sig
          val is_bottom :
            'a Apron.Manager.t -> 'a Bddapron.Bdddomain0.elt -> bool
          val meet_cube :
            'a Apron.Manager.t ->
            ('b, [> 'b Bddapron.Env.typ ] as 'c,
             [> 'b Bddapron.Env.typdef ] as 'd, 'e)
            Bddapron.Env.O.t ->
            ('b, ('b, 'c, 'd, 'e) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
            'a Bddapron.Bdddomain0.elt ->
            Cudd.Bdd.vt -> 'a Bddapron.Bdddomain0.elt
          val forget :
            'a Apron.Manager.t ->
            'a Bddapron.Bdddomain0.elt ->
            Cudd.Bdd.vt -> Apron.Dim.t array -> 'a Bddapron.Bdddomain0.elt
        end
      val check_wellformed :
        ('a, 'b) Bddapron.Bdddomain0.man -> 'b Bddapron.Bdddomain0.t -> bool
      val canonicalize :
        ?apron:bool ->
        ?unique:bool ->
        ?disjoint:bool ->
        ('a, 'b) Bddapron.Bdddomain0.man -> 'b Bddapron.Bdddomain0.t -> unit
      val size :
        ('a, 'b) Bddapron.Bdddomain0.man -> 'b Bddapron.Bdddomain0.t -> int
      val print :
        ?print_apron:((int -> string) ->
                      Format.formatter -> 'b Apron.Abstract0.t -> unit) ->
        ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'e)
        Bddapron.Env.O.t ->
        Format.formatter -> 'b Bddapron.Bdddomain0.t -> unit
      val bottom :
        ('a, 'b) Bddapron.Bdddomain0.man ->
        ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'e)
        Bddapron.Env.O.t -> 'b Bddapron.Bdddomain0.t
      val top :
        ('a, 'b) Bddapron.Bdddomain0.man ->
        ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'e)
        Bddapron.Env.O.t -> 'b Bddapron.Bdddomain0.t
      val of_apron :
        ('a, 'b) Bddapron.Bdddomain0.man ->
        ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'e)
        Bddapron.Env.O.t -> 'b Apron.Abstract0.t -> 'b Bddapron.Bdddomain0.t
      val of_bddapron :
        ('a, 'b) Bddapron.Bdddomain0.man ->
        ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'e)
        Bddapron.Env.O.t ->
        ('a Bddapron.Expr0.Bool.t * 'b Apron.Abstract0.t) list ->
        'b Bddapron.Bdddomain0.t
      val is_bottom :
        ('a, 'b) Bddapron.Bdddomain0.man -> 'b Bddapron.Bdddomain0.t -> bool
      val is_top :
        ('a, 'b) Bddapron.Bdddomain0.man -> 'b Bddapron.Bdddomain0.t -> bool
      val is_leq :
        ('a, 'b) Bddapron.Bdddomain0.man ->
        'b Bddapron.Bdddomain0.t -> 'b Bddapron.Bdddomain0.t -> bool
      val is_eq :
        ('a, 'b) Bddapron.Bdddomain0.man ->
        'b Bddapron.Bdddomain0.t -> 'b Bddapron.Bdddomain0.t -> bool
      val to_bddapron :
        ('a, 'b) Bddapron.Bdddomain0.man ->
        'b Bddapron.Bdddomain0.t ->
        ('a Bddapron.Expr0.Bool.t * 'b Apron.Abstract0.t) list
      val meet :
        ('a, 'b) Bddapron.Bdddomain0.man ->
        'b Bddapron.Bdddomain0.t ->
        'b Bddapron.Bdddomain0.t -> 'b Bddapron.Bdddomain0.t
      val join :
        ('a, 'b) Bddapron.Bdddomain0.man ->
        'b Bddapron.Bdddomain0.t ->
        'b Bddapron.Bdddomain0.t -> 'b Bddapron.Bdddomain0.t
      val meet_condition :
        ('a, 'b) Bddapron.Bdddomain0.man ->
        ('a, [> 'a Bddapron.Env.typ ] as 'c,
         [> 'a Bddapron.Env.typdef ] as 'd, 'e)
        Bddapron.Env.O.t ->
        ('a, ('a, 'c, 'd, 'e) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
        'b Bddapron.Bdddomain0.t ->
        'a Bddapron.Expr0.Bool.t -> 'b Bddapron.Bdddomain0.t
      val assign_lexpr :
        ?relational:bool ->
        ?nodependency:bool ->
        ('a, 'b) Bddapron.Bdddomain0.man ->
        ('a, [> 'a Bddapron.Env.typ ] as 'c,
         [> 'a Bddapron.Env.typdef ] as 'd, 'e)
        Bddapron.Env.O.t ->
        ('a, ('a, 'c, 'd, 'e) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
        'b Bddapron.Bdddomain0.t ->
        'a list ->
        'a Bddapron.Expr0.t list ->
        'b Bddapron.Bdddomain0.t option -> 'b Bddapron.Bdddomain0.t
      val substitute_lexpr :
        ('a, 'b) Bddapron.Bdddomain0.man ->
        ('a, [> 'a Bddapron.Env.typ ] as 'c,
         [> 'a Bddapron.Env.typdef ] as 'd, 'e)
        Bddapron.Env.O.t ->
        ('a, ('a, 'c, 'd, 'e) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
        'b Bddapron.Bdddomain0.t ->
        'a list ->
        'a Bddapron.Expr0.t list ->
        'b Bddapron.Bdddomain0.t option -> 'b Bddapron.Bdddomain0.t
      val forget_list :
        ('a, 'b) Bddapron.Bdddomain0.man ->
        ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'e)
        Bddapron.Env.O.t ->
        'b Bddapron.Bdddomain0.t -> 'a list -> 'b Bddapron.Bdddomain0.t
      val widening :
        ('a, 'b) Bddapron.Bdddomain0.man ->
        'b Bddapron.Bdddomain0.t ->
        'b Bddapron.Bdddomain0.t -> 'b Bddapron.Bdddomain0.t
      val widening_threshold :
        ('a, 'b) Bddapron.Bdddomain0.man ->
        'b Bddapron.Bdddomain0.t ->
        'b Bddapron.Bdddomain0.t ->
        Apron.Lincons0.t array -> 'b Bddapron.Bdddomain0.t
      val apply_change :
        bottom:'b Bddapron.Bdddomain0.t ->
        ('a, 'b) Bddapron.Bdddomain0.man ->
        'b Bddapron.Bdddomain0.t ->
        Bddapron.Env.change -> 'b Bddapron.Bdddomain0.t
      val apply_permutation :
        ('a, 'b) Bddapron.Bdddomain0.man ->
        'b Bddapron.Bdddomain0.t ->
        int array option * Apron.Dim.perm option -> 'b Bddapron.Bdddomain0.t
    end
end