sig
  module Apronexpr :
    sig
      type 'a symbol =
        'Bdd.Env.symbol = {
        compare : '-> '-> int;
        marshal : '-> string;
        unmarshal : string -> 'a;
        mutable print : Format.formatter -> '-> unit;
      }
      type typ = [ `Int | `Real ]
      type ('a, 'b) typ_of_var = '-> 'b
        constraint 'b = [> Bddapron.Apronexpr.typ ]
      module Lin :
        sig
          type 'a term = Mpqf.t * 'a
          type 'a t = {
            cst : Mpqf.t;
            lterm : 'Bddapron.Apronexpr.Lin.term list;
          }
          val normalize :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Lin.t -> 'Bddapron.Apronexpr.Lin.t
          val compare_lterm :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Lin.term list ->
            'Bddapron.Apronexpr.Lin.term list -> int
          val compare :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Lin.t -> 'Bddapron.Apronexpr.Lin.t -> int
          val var : '-> 'Bddapron.Apronexpr.Lin.t
          val zero : 'Bddapron.Apronexpr.Lin.t
          val one : 'Bddapron.Apronexpr.Lin.t
          val cst : Mpqf.t -> 'Bddapron.Apronexpr.Lin.t
          val add :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Lin.t ->
            'Bddapron.Apronexpr.Lin.t -> 'Bddapron.Apronexpr.Lin.t
          val sub :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Lin.t ->
            'Bddapron.Apronexpr.Lin.t -> 'Bddapron.Apronexpr.Lin.t
          val scale :
            Mpqf.t ->
            'Bddapron.Apronexpr.Lin.t -> 'Bddapron.Apronexpr.Lin.t
          val negate :
            'Bddapron.Apronexpr.Lin.t -> 'Bddapron.Apronexpr.Lin.t
          val support :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Lin.t -> 'PSette.t
          val substitute_by_var :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Lin.t ->
            ('a, 'a) PMappe.t -> 'Bddapron.Apronexpr.Lin.t
          val normalize_as_constraint :
            'Bddapron.Apronexpr.Lin.t -> 'Bddapron.Apronexpr.Lin.t
          val print :
            'Bddapron.Apronexpr.symbol ->
            Format.formatter -> 'Bddapron.Apronexpr.Lin.t -> unit
          val of_linexpr0 :
            'Bddapron.Apronexpr.symbol ->
            Apron.Environment.t ->
            Apron.Linexpr0.t -> 'Bddapron.Apronexpr.Lin.t
          val of_linexpr1 :
            'Bddapron.Apronexpr.symbol ->
            Apron.Linexpr1.t -> 'Bddapron.Apronexpr.Lin.t
          val to_linexpr0 :
            'Bddapron.Apronexpr.symbol ->
            Apron.Environment.t ->
            'Bddapron.Apronexpr.Lin.t -> Apron.Linexpr0.t
          val to_linexpr1 :
            'Bddapron.Apronexpr.symbol ->
            Apron.Environment.t ->
            'Bddapron.Apronexpr.Lin.t -> Apron.Linexpr1.t
        end
      module Poly :
        sig
          type 'a varexp = 'a * int
          type 'a monomial = 'Bddapron.Apronexpr.Poly.varexp list
          type 'a term = Mpqf.t * 'Bddapron.Apronexpr.Poly.monomial
          type 'a t = 'Bddapron.Apronexpr.Poly.term list
          val compare_varexp :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Poly.varexp ->
            'Bddapron.Apronexpr.Poly.varexp -> int
          val compare_monomial :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Poly.monomial ->
            'Bddapron.Apronexpr.Poly.monomial -> int
          val normalize_monomial :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Poly.monomial ->
            'Bddapron.Apronexpr.Poly.monomial
          val normalize :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Poly.t -> 'Bddapron.Apronexpr.Poly.t
          val normalize_full :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Poly.t -> 'Bddapron.Apronexpr.Poly.t
          val compare :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Poly.t ->
            'Bddapron.Apronexpr.Poly.t -> int
          val cst : Mpqf.t -> 'Bddapron.Apronexpr.Poly.t
          val var : '-> 'Bddapron.Apronexpr.Poly.t
          val add :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Poly.t ->
            'Bddapron.Apronexpr.Poly.t -> 'Bddapron.Apronexpr.Poly.t
          val sub :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Poly.t ->
            'Bddapron.Apronexpr.Poly.t -> 'Bddapron.Apronexpr.Poly.t
          val scale :
            'Bddapron.Apronexpr.symbol ->
            Mpqf.t * 'Bddapron.Apronexpr.Poly.monomial ->
            'Bddapron.Apronexpr.Poly.t -> 'Bddapron.Apronexpr.Poly.t
          val mul :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Poly.t ->
            'Bddapron.Apronexpr.Poly.t -> 'Bddapron.Apronexpr.Poly.t
          val div :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Poly.t ->
            'Bddapron.Apronexpr.Poly.t -> 'Bddapron.Apronexpr.Poly.t
          val negate :
            'Bddapron.Apronexpr.Poly.t -> 'Bddapron.Apronexpr.Poly.t
          val support :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Poly.t -> 'PSette.t
          val substitute_by_var :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Poly.t ->
            ('a, 'a) PMappe.t -> 'Bddapron.Apronexpr.Poly.t
          val normalize_as_constraint :
            'Bddapron.Apronexpr.Poly.t -> 'Bddapron.Apronexpr.Poly.t
          val print :
            'Bddapron.Apronexpr.symbol ->
            Format.formatter -> 'Bddapron.Apronexpr.Poly.t -> unit
        end
      module Tree :
        sig
          type unop = Apron.Texpr1.unop = Neg | Cast | Sqrt
          type binop = Apron.Texpr1.binop = Add | Sub | Mul | Div | Mod | Pow
          type typ =
            Apron.Texpr1.typ =
              Real
            | Int
            | Single
            | Double
            | Extended
            | Quad
          type round = Apron.Texpr1.round = Near | Zero | Up | Down | Rnd
          type 'a t =
              Cst of Apron.Coeff.t
            | Var of 'a
            | Unop of Bddapron.Apronexpr.Tree.unop *
                'Bddapron.Apronexpr.Tree.t * Bddapron.Apronexpr.Tree.typ *
                Bddapron.Apronexpr.Tree.round
            | Binop of Bddapron.Apronexpr.Tree.binop *
                'Bddapron.Apronexpr.Tree.t * 'Bddapron.Apronexpr.Tree.t *
                Bddapron.Apronexpr.Tree.typ * Bddapron.Apronexpr.Tree.round
          val support :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Tree.t -> 'PSette.t
          val substitute_by_var :
            'Bddapron.Apronexpr.Tree.t ->
            ('a, 'a) PMappe.t -> 'Bddapron.Apronexpr.Tree.t
          val print :
            'Bddapron.Apronexpr.symbol ->
            Format.formatter -> 'Bddapron.Apronexpr.Tree.t -> unit
          val compare :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Tree.t ->
            'Bddapron.Apronexpr.Tree.t -> int
          val of_expr :
            'Bddapron.Apronexpr.symbol ->
            Apron.Texpr1.expr -> 'Bddapron.Apronexpr.Tree.t
          val to_expr :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Tree.t -> Apron.Texpr1.expr
        end
      val lin_of_poly :
        'Bddapron.Apronexpr.symbol ->
        'Bddapron.Apronexpr.Poly.t -> 'Bddapron.Apronexpr.Lin.t
      val lin_of_tree :
        'Bddapron.Apronexpr.symbol ->
        'Bddapron.Apronexpr.Tree.t -> 'Bddapron.Apronexpr.Lin.t
      val poly_of_tree :
        'Bddapron.Apronexpr.symbol ->
        'Bddapron.Apronexpr.Tree.t -> 'Bddapron.Apronexpr.Poly.t
      val tree_of_lin :
        'Bddapron.Apronexpr.Lin.t -> 'Bddapron.Apronexpr.Tree.t
      val tree_of_poly :
        'Bddapron.Apronexpr.Poly.t -> 'Bddapron.Apronexpr.Tree.t
      type 'a t =
          Lin of 'Bddapron.Apronexpr.Lin.t
        | Poly of 'Bddapron.Apronexpr.Poly.t
        | Tree of 'Bddapron.Apronexpr.Tree.t
      type 'a expr = 'Bddapron.Apronexpr.t
      val var :
        'Bddapron.Apronexpr.symbol ->
        ('a, [> Bddapron.Apronexpr.typ ]) Bddapron.Apronexpr.typ_of_var ->
        '-> 'Bddapron.Apronexpr.t
      val zero : 'Bddapron.Apronexpr.t
      val one : 'Bddapron.Apronexpr.t
      val cst : Apron.Coeff.t -> 'Bddapron.Apronexpr.t
      val add :
        'Bddapron.Apronexpr.symbol ->
        ?typ:Apron.Texpr1.typ ->
        ?round:Apron.Texpr1.round ->
        'Bddapron.Apronexpr.t ->
        'Bddapron.Apronexpr.t -> 'Bddapron.Apronexpr.t
      val sub :
        'Bddapron.Apronexpr.symbol ->
        ?typ:Apron.Texpr1.typ ->
        ?round:Apron.Texpr1.round ->
        'Bddapron.Apronexpr.t ->
        'Bddapron.Apronexpr.t -> 'Bddapron.Apronexpr.t
      val mul :
        'Bddapron.Apronexpr.symbol ->
        ?typ:Apron.Texpr1.typ ->
        ?round:Apron.Texpr1.round ->
        'Bddapron.Apronexpr.t ->
        'Bddapron.Apronexpr.t -> 'Bddapron.Apronexpr.t
      val div :
        'Bddapron.Apronexpr.symbol ->
        ?typ:Apron.Texpr1.typ ->
        ?round:Apron.Texpr1.round ->
        'Bddapron.Apronexpr.t ->
        'Bddapron.Apronexpr.t -> 'Bddapron.Apronexpr.t
      val gmod :
        'Bddapron.Apronexpr.symbol ->
        ?typ:Apron.Texpr1.typ ->
        ?round:Apron.Texpr1.round ->
        'Bddapron.Apronexpr.t ->
        'Bddapron.Apronexpr.t -> 'Bddapron.Apronexpr.t
      val negate : 'Bddapron.Apronexpr.t -> 'Bddapron.Apronexpr.t
      val cast :
        ?typ:Apron.Texpr1.typ ->
        ?round:Apron.Texpr1.round ->
        'Bddapron.Apronexpr.t -> 'Bddapron.Apronexpr.t
      val sqrt :
        ?typ:Apron.Texpr1.typ ->
        ?round:Apron.Texpr1.round ->
        'Bddapron.Apronexpr.t -> 'Bddapron.Apronexpr.t
      val support :
        'Bddapron.Apronexpr.symbol ->
        'Bddapron.Apronexpr.t -> 'PSette.t
      val substitute_by_var :
        'Bddapron.Apronexpr.symbol ->
        'Bddapron.Apronexpr.t ->
        ('a, 'a) PMappe.t -> 'Bddapron.Apronexpr.t
      val normalize :
        'Bddapron.Apronexpr.symbol ->
        'Bddapron.Apronexpr.t -> 'Bddapron.Apronexpr.t
      val equal :
        'Bddapron.Apronexpr.symbol ->
        'Bddapron.Apronexpr.t -> 'Bddapron.Apronexpr.t -> bool
      val hash :
        'Bddapron.Apronexpr.symbol -> 'Bddapron.Apronexpr.t -> int
      val compare :
        'Bddapron.Apronexpr.symbol ->
        'Bddapron.Apronexpr.t -> 'Bddapron.Apronexpr.t -> int
      val normalize_as_constraint :
        'Bddapron.Apronexpr.t -> 'Bddapron.Apronexpr.t
      val is_dependent_on_integer_only :
        ('a, [> Bddapron.Apronexpr.typ ]) Bddapron.Apronexpr.typ_of_var ->
        'Bddapron.Apronexpr.t -> bool
      val typ_of_expr :
        ('a, [> Bddapron.Apronexpr.typ ]) Bddapron.Apronexpr.typ_of_var ->
        'Bddapron.Apronexpr.t -> [ `Int | `Real ]
      val print :
        'Bddapron.Apronexpr.symbol ->
        Format.formatter -> 'Bddapron.Apronexpr.t -> unit
      val print_typ : Format.formatter -> [> Bddapron.Apronexpr.typ ] -> unit
      val of_linexpr0 :
        'Bddapron.Apronexpr.symbol ->
        Apron.Environment.t -> Apron.Linexpr0.t -> 'Bddapron.Apronexpr.t
      val of_linexpr1 :
        'Bddapron.Apronexpr.symbol ->
        Apron.Linexpr1.t -> 'Bddapron.Apronexpr.t
      val to_linexpr0 :
        'Bddapron.Apronexpr.symbol ->
        Apron.Environment.t -> 'Bddapron.Apronexpr.t -> Apron.Linexpr0.t
      val to_linexpr1 :
        'Bddapron.Apronexpr.symbol ->
        Apron.Environment.t -> 'Bddapron.Apronexpr.t -> Apron.Linexpr1.t
      val of_texpr0 :
        'Bddapron.Apronexpr.symbol ->
        Apron.Environment.t -> Apron.Texpr0.t -> 'Bddapron.Apronexpr.t
      val of_texpr1 :
        'Bddapron.Apronexpr.symbol ->
        Apron.Texpr1.t -> 'Bddapron.Apronexpr.t
      val to_texpr0 :
        'Bddapron.Apronexpr.symbol ->
        Apron.Environment.t -> 'Bddapron.Apronexpr.t -> Apron.Texpr0.t
      val to_texpr1 :
        'Bddapron.Apronexpr.symbol ->
        Apron.Environment.t -> 'Bddapron.Apronexpr.t -> Apron.Texpr1.t
      val to_apron0 :
        'Bddapron.Apronexpr.symbol ->
        Apron.Environment.t ->
        'Bddapron.Apronexpr.t ->
        [ `Lin of Apron.Linexpr0.t | `Tree of Apron.Texpr0.t ]
      val to_apron1 :
        'Bddapron.Apronexpr.symbol ->
        Apron.Environment.t ->
        'Bddapron.Apronexpr.t ->
        [ `Lin of Apron.Linexpr1.t | `Tree of Apron.Texpr1.t ]
      module Condition :
        sig
          type typ =
            Apron.Tcons1.typ =
              EQ
            | SUPEQ
            | SUP
            | DISEQ
            | EQMOD of Apron.Scalar.t
          type 'a t =
              Bddapron.Apronexpr.Condition.typ * 'Bddapron.Apronexpr.expr
          val make :
            ('a, [> Bddapron.Apronexpr.Condition.typ ])
            Bddapron.Apronexpr.typ_of_var ->
            Bddapron.Apronexpr.Condition.typ ->
            'Bddapron.Apronexpr.expr ->
            [ `Bool of bool | `Cond of 'Bddapron.Apronexpr.Condition.t ]
          val negate :
            ('a, [> Bddapron.Apronexpr.Condition.typ ])
            Bddapron.Apronexpr.typ_of_var ->
            'Bddapron.Apronexpr.Condition.t ->
            'Bddapron.Apronexpr.Condition.t
          val support :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Condition.t -> 'PSette.t
          val print :
            'Bddapron.Apronexpr.symbol ->
            Format.formatter -> 'Bddapron.Apronexpr.Condition.t -> unit
          val compare :
            'Bddapron.Apronexpr.symbol ->
            'Bddapron.Apronexpr.Condition.t ->
            'Bddapron.Apronexpr.Condition.t -> int
          val of_lincons0 :
            'Bddapron.Apronexpr.symbol ->
            ('a, [> Bddapron.Apronexpr.Condition.typ ])
            Bddapron.Apronexpr.typ_of_var ->
            Apron.Environment.t ->
            Apron.Lincons0.t ->
            [ `Bool of bool | `Cond of 'Bddapron.Apronexpr.Condition.t ]
          val of_lincons1 :
            'Bddapron.Apronexpr.symbol ->
            ('a, [> Bddapron.Apronexpr.Condition.typ ])
            Bddapron.Apronexpr.typ_of_var ->
            Apron.Lincons1.t ->
            [ `Bool of bool | `Cond of 'Bddapron.Apronexpr.Condition.t ]
          val of_tcons0 :
            'Bddapron.Apronexpr.symbol ->
            ('a, [> Bddapron.Apronexpr.Condition.typ ])
            Bddapron.Apronexpr.typ_of_var ->
            Apron.Environment.t ->
            Apron.Tcons0.t ->
            [ `Bool of bool | `Cond of 'Bddapron.Apronexpr.Condition.t ]
          val of_tcons1 :
            'Bddapron.Apronexpr.symbol ->
            ('a, [> Bddapron.Apronexpr.Condition.typ ])
            Bddapron.Apronexpr.typ_of_var ->
            Apron.Tcons1.t ->
            [ `Bool of bool | `Cond of 'Bddapron.Apronexpr.Condition.t ]
          val to_tcons0 :
            'Bddapron.Apronexpr.symbol ->
            Apron.Environment.t ->
            'Bddapron.Apronexpr.Condition.t -> Apron.Tcons0.t
          val to_tcons1 :
            'Bddapron.Apronexpr.symbol ->
            Apron.Environment.t ->
            'Bddapron.Apronexpr.Condition.t -> Apron.Tcons1.t
          val to_apron0 :
            'Bddapron.Apronexpr.symbol ->
            Apron.Environment.t ->
            'Bddapron.Apronexpr.Condition.t ->
            [ `Lin of Apron.Lincons0.t | `Tree of Apron.Tcons0.t ]
          val to_apron1 :
            'Bddapron.Apronexpr.symbol ->
            Apron.Environment.t ->
            'Bddapron.Apronexpr.Condition.t ->
            [ `Lin of Apron.Lincons1.t | `Tree of Apron.Tcons1.t ]
        end
    end
  module Env :
    sig
      type 'a typdef = 'Bdd.Env.typdef
      type 'a typ =
          [ `Benum of '| `Bint of bool * int | `Bool | `Int | `Real ]
      type 'a symbol =
        'Bdd.Env.symbol = {
        compare : '-> '-> int;
        marshal : '-> string;
        unmarshal : string -> 'a;
        mutable print : Format.formatter -> '-> unit;
      }
      type ('a, 'b) ext = {
        mutable table : '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 = [> 'Bddapron.Env.typ ]
            constraint 'c = [> 'Bddapron.Env.typdef ]
          val make :
            symbol:'Bddapron.Env.symbol ->
            copy_aext:('-> 'd) ->
            ?bddindex0:int ->
            ?bddsize:int ->
            ?relational:bool ->
            Cudd.Man.vt ->
            '->
            ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
            Bddapron.Env.O.t
          val print :
            (Format.formatter -> ([> 'Bddapron.Env.typ ] as 'b) -> unit) ->
            (Format.formatter -> ([> 'Bddapron.Env.typdef ] as 'c) -> unit) ->
            (Format.formatter -> '-> unit) ->
            Format.formatter -> ('a, 'b, 'c, 'd) Bddapron.Env.O.t -> unit
        end
      type 'a t =
          ('a, 'Bddapron.Env.typ, 'Bddapron.Env.typdef, unit)
          Bddapron.Env.O.t
      val print_typ :
        (Format.formatter -> '-> unit) ->
        Format.formatter -> [> 'Bddapron.Env.typ ] -> unit
      val print_typdef :
        (Format.formatter -> '-> unit) ->
        Format.formatter -> [> 'Bddapron.Env.typdef ] -> unit
      val print_idcondb :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> Format.formatter -> int * bool -> unit
      val print_order :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> Format.formatter -> unit
      val print :
        Format.formatter ->
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> unit
      val marshal : '-> string
      val unmarshal : string -> 'a
      val make_symbol :
        ?compare:('-> '-> int) ->
        ?marshal:('-> string) ->
        ?unmarshal:(string -> 'a) ->
        (Format.formatter -> '-> unit) -> 'Bddapron.Env.symbol
      val string_symbol : string Bddapron.Env.symbol
      val make :
        symbol:'Bddapron.Env.symbol ->
        ?bddindex0:int ->
        ?bddsize:int -> ?relational:bool -> Cudd.Man.vt -> 'Bddapron.Env.t
      val make_string :
        ?bddindex0:int ->
        ?bddsize:int ->
        ?relational:bool -> Cudd.Man.vt -> string Bddapron.Env.t
      val copy :
        ('a, [> 'Bddapron.Env.typ ] as 'b,
         [> 'Bddapron.Env.typdef ] as 'c, 'd)
        Bddapron.Env.O.t -> ('a, 'b, 'c, 'd) Bddapron.Env.O.t
      val mem_typ :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> '-> bool
      val mem_var :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> '-> bool
      val mem_label :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> '-> bool
      val typdef_of_typ :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ] as 'b, 'd)
        Bddapron.Env.O.t -> '-> 'b
      val typ_of_var :
        ('a, [> 'Bddapron.Env.typ ] as 'b, [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> '-> 'b
      val vars :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> 'PSette.t
      val labels :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> 'PSette.t
      val apron :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> Apron.Environment.t
      val add_typ_with :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ] as 'b, 'd)
        Bddapron.Env.O.t -> '-> '-> unit
      val add_vars_with :
        ('a, [> 'Bddapron.Env.typ ] as 'b, [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> ('a * 'b) list -> int array option
      val remove_vars_with :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> 'a list -> int array option
      val rename_vars_with :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t ->
        ('a * 'a) list -> int array option * Apron.Dim.perm option
      val add_typ :
        ('a, [> 'Bddapron.Env.typ ] as 'b,
         [> 'Bddapron.Env.typdef ] as 'c, 'd)
        Bddapron.Env.O.t -> '-> '-> ('a, 'b, 'c, 'd) Bddapron.Env.O.t
      val add_vars :
        ('a, [> 'Bddapron.Env.typ ] as 'b,
         [> '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, [> 'Bddapron.Env.typ ] as 'b,
         [> 'Bddapron.Env.typdef ] as 'c, 'd)
        Bddapron.Env.O.t -> 'a list -> ('a, 'b, 'c, 'd) Bddapron.Env.O.t
      val rename_vars :
        ('a, [> 'Bddapron.Env.typ ] as 'b,
         [> '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, [> 'Bddapron.Env.typ ] as 'b,
         [> 'Bddapron.Env.typdef ] as 'c, 'd)
        Bddapron.Env.O.t -> ('a, 'b, 'c, 'd) Bddapron.Env.O.t -> bool
      val is_eq :
        ('a, [> 'Bddapron.Env.typ ] as 'b,
         [> 'Bddapron.Env.typdef ] as 'c, 'd)
        Bddapron.Env.O.t -> ('a, 'b, 'c, 'd) Bddapron.Env.O.t -> bool
      val lce :
        ('a, [> 'Bddapron.Env.typ ] as 'b,
         [> '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, [> 'Bddapron.Env.typ ] as 'b,
         [> '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, [> 'Bddapron.Env.typ ] as 'b,
         [> 'Bddapron.Env.typdef ] as 'c, 'd)
        Bddapron.Env.O.t ->
        '-> (('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, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> '-> unit
      val check_lvar :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> 'a list -> unit
      val check_value :
        ('a, [> 'Bddapron.Env.typ ] as 'b,
         [> '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, [> 'Bddapron.Env.typ ] as 'b,
          [> '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, [> 'Bddapron.Env.typ ] as 'b,
          [> '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, [> 'Bddapron.Env.typ ] as 'b,
         [> '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, [> 'Bddapron.Env.typ ] as 'b,
         [> '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, [> 'Bddapron.Env.typ ] as 'b,
         [> '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 :
        ('-> 'f) ->
        (('a, [> 'Bddapron.Env.typ ] as 'b,
          [> '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 :
        ('-> '-> 'g) ->
        (('a, [> 'Bddapron.Env.typ ] as 'b,
          [> '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, [> 'Bddapron.Env.typ ] as 'b,
          [> 'Bddapron.Env.typdef ] as 'c, 'd)
         Bddapron.Env.O.t -> '-> '-> '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 :
        ('-> '-> '-> 'h) ->
        (('a, [> 'Bddapron.Env.typ ] as 'b,
          [> '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, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> Apron.Dim.t -> 'a
      val aprondim_of_var :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> '-> Apron.Dim.t
      val string_of_aprondim :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> Apron.Dim.t -> string
    end
  module Cond :
    sig
      type 'a cond = [ `Apron of 'Bddapron.Apronexpr.Condition.t ]
      val print_cond :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t ->
        Format.formatter -> [< 'Bddapron.Cond.cond ] -> unit
      val compare_cond :
        'Bdd.Env.symbol ->
        [< 'Bddapron.Cond.cond ] -> [< 'Bddapron.Cond.cond ] -> int
      val negate_cond :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> 'Bddapron.Cond.cond -> 'Bddapron.Cond.cond
      val support_cond :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> [< 'Bddapron.Cond.cond ] -> 'PSette.t
      module O :
        sig
          type ('a, 'b) t =
              ('a, 'b, 'Bddapron.Cond.cond, Cudd.Man.v) Bdd.Cond.t
            constraint 'b =
              ('a, [> 'Bddapron.Env.typ ] as 'c,
               [> 'Bddapron.Env.typdef ] as 'd, 'e)
              Bddapron.Env.O.t
          val make :
            symbol:'Bdd.Env.symbol ->
            ?bddindex0:int ->
            ?bddsize:int ->
            Cudd.Man.vt ->
            ('a,
             ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'b)
             Bddapron.Env.O.t)
            Bddapron.Cond.O.t
        end
      type 'a t = ('a, 'Bddapron.Env.t) Bddapron.Cond.O.t
      val make :
        symbol:'Bdd.Env.symbol ->
        ?bddindex0:int -> ?bddsize:int -> Cudd.Man.vt -> 'Bddapron.Cond.t
      val copy : 'Bddapron.Cond.t -> 'Bddapron.Cond.t
      val print :
        'Bddapron.Env.t -> Format.formatter -> 'Bddapron.Cond.t -> unit
      type ('a, 'b) value =
        ('a, 'b) Bdd.Cond.value = {
        cond : 'a;
        val1 : 'b;
      }
      val make_value : '-> '-> ('a, 'b) Bddapron.Cond.value
      val get_cond : ('a, 'b) Bddapron.Cond.value -> 'a
      val get_val1 : ('a, 'b) Bddapron.Cond.value -> 'b
      val get_env :
        ('a, ('b, 'c) Bddapron.Env.value) Bddapron.Cond.value -> 'b
      val get_val0 :
        ('a, ('b, 'c) Bddapron.Env.value) Bddapron.Cond.value -> 'c
    end
  module ApronexprDD :
    sig
      type 'a t = 'Bddapron.Apronexpr.t Cudd.Mtbdd.t
      val of_expr :
        [> `Apron of 'Bddapron.ApronexprDD.t ] -> 'Bddapron.ApronexprDD.t
      val to_expr :
        'Bddapron.ApronexprDD.t -> [> `Apron of 'Bddapron.ApronexprDD.t ]
      val of_apronexpr :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t ->
        'Bddapron.Apronexpr.t -> 'Bddapron.ApronexprDD.t
      val print :
        (Format.formatter -> Cudd.Bdd.vt -> unit) ->
        'Bddapron.Apronexpr.symbol ->
        Format.formatter -> 'Bddapron.ApronexprDD.t -> unit
      val is_zero :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> 'Bddapron.Apronexpr.t -> bool
      val is_one :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> 'Bddapron.Apronexpr.t -> bool
      val absorbant_zero :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t ->
        'Bddapron.Apronexpr.t Cudd.Mtbdd.unique ->
        'Bddapron.Apronexpr.t Cudd.Mtbdd.unique option
      val absorbant_one :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t ->
        'Bddapron.Apronexpr.t Cudd.Mtbdd.unique ->
        'Bddapron.Apronexpr.t Cudd.Mtbdd.unique option
      val cst :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> Apron.Coeff.t -> 'Bddapron.ApronexprDD.t
      val var :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> '-> 'Bddapron.ApronexprDD.t
      val add :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t ->
        ?typ:Apron.Texpr1.typ ->
        ?round:Apron.Texpr1.round ->
        'Bddapron.ApronexprDD.t ->
        'Bddapron.ApronexprDD.t -> 'Bddapron.ApronexprDD.t
      val sub :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t ->
        ?typ:Apron.Texpr1.typ ->
        ?round:Apron.Texpr1.round ->
        'Bddapron.ApronexprDD.t ->
        'Bddapron.ApronexprDD.t -> 'Bddapron.ApronexprDD.t
      val mul :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t ->
        ?typ:Apron.Texpr1.typ ->
        ?round:Apron.Texpr1.round ->
        'Bddapron.ApronexprDD.t ->
        'Bddapron.ApronexprDD.t -> 'Bddapron.ApronexprDD.t
      val div :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t ->
        ?typ:Apron.Texpr1.typ ->
        ?round:Apron.Texpr1.round ->
        'Bddapron.ApronexprDD.t ->
        'Bddapron.ApronexprDD.t -> 'Bddapron.ApronexprDD.t
      val gmod :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t ->
        ?typ:Apron.Texpr1.typ ->
        ?round:Apron.Texpr1.round ->
        'Bddapron.ApronexprDD.t ->
        'Bddapron.ApronexprDD.t -> 'Bddapron.ApronexprDD.t
      val negate :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t ->
        'Bddapron.ApronexprDD.t -> 'Bddapron.ApronexprDD.t
      val cast :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t ->
        ?typ:Apron.Texpr1.typ ->
        ?round:Apron.Texpr1.round ->
        'Bddapron.ApronexprDD.t -> 'Bddapron.ApronexprDD.t
      val sqrt :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t ->
        ?typ:Apron.Texpr1.typ ->
        ?round:Apron.Texpr1.round ->
        'Bddapron.ApronexprDD.t -> 'Bddapron.ApronexprDD.t
      val support_leaf :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> 'Bddapron.ApronexprDD.t -> 'PSette.t
      val support_cond :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t -> 'Bddapron.ApronexprDD.t -> Cudd.Bdd.vt
      val substitute_linexpr :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t ->
        'Bddapron.Apronexpr.Lin.t ->
        ('a, [> `Apron of 'Bddapron.ApronexprDD.t ]) PMappe.t ->
        'Bddapron.ApronexprDD.t
      val substitute_polyexpr :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t ->
        'Bddapron.Apronexpr.Poly.t ->
        ('a, [> `Apron of 'Bddapron.ApronexprDD.t ]) PMappe.t ->
        'Bddapron.ApronexprDD.t
      val substitute_treeexpr :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t ->
        'Bddapron.Apronexpr.Tree.t ->
        ('a, [> `Apron of 'Bddapron.ApronexprDD.t ]) PMappe.t ->
        'Bddapron.ApronexprDD.t
      val substitute :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t ->
        'Bddapron.Apronexpr.t ->
        ('a, [> `Apron of 'Bddapron.ApronexprDD.t ]) PMappe.t ->
        'Bddapron.ApronexprDD.t
      module Condition :
        sig
          val of_apronexpr :
            ('a, [> 'Bddapron.Env.typ ] as 'b,
             [> 'Bddapron.Env.typdef ] as 'c, 'd)
            Bddapron.Env.O.t ->
            ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
            'Bddapron.Apronexpr.Condition.t -> Cudd.Bdd.vt
          val of_condition :
            ('a, [> 'Bddapron.Env.typ ] as 'b,
             [> 'Bddapron.Env.typdef ] as 'c, 'd)
            Bddapron.Env.O.t ->
            ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
            [< `Bool of bool | `Cond of 'Bddapron.Apronexpr.Condition.t ] ->
            Cudd.Bdd.vt
          val make :
            ('a, [> 'Bddapron.Env.typ ] as 'b,
             [> 'Bddapron.Env.typdef ] as 'c, 'd)
            Bddapron.Env.O.t ->
            ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
            Bddapron.Apronexpr.Condition.typ ->
            'Bddapron.ApronexprDD.t -> Cudd.Bdd.vt
          val supeq :
            ('a, [> 'Bddapron.Env.typ ] as 'b,
             [> 'Bddapron.Env.typdef ] as 'c, 'd)
            Bddapron.Env.O.t ->
            ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
            'Bddapron.ApronexprDD.t -> Cudd.Bdd.vt
          val sup :
            ('a, [> 'Bddapron.Env.typ ] as 'b,
             [> 'Bddapron.Env.typdef ] as 'c, 'd)
            Bddapron.Env.O.t ->
            ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
            'Bddapron.ApronexprDD.t -> Cudd.Bdd.vt
          val eq :
            ('a, [> 'Bddapron.Env.typ ] as 'b,
             [> 'Bddapron.Env.typdef ] as 'c, 'd)
            Bddapron.Env.O.t ->
            ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
            'Bddapron.ApronexprDD.t -> Cudd.Bdd.vt
          val substitute :
            ('a, [> 'Bddapron.Env.typ ] as 'b,
             [> 'Bddapron.Env.typdef ] as 'c, 'd)
            Bddapron.Env.O.t ->
            ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
            'Bddapron.Apronexpr.Condition.t ->
            ('a, [> `Apron of 'Bddapron.ApronexprDD.t ]) PMappe.t ->
            Cudd.Bdd.vt
        end
    end
  module Common :
    sig
      val tcons0_array_of_cubecond :
        ('a, [> 'Bddapron.Env.typ ] as 'b,
         [> 'Bddapron.Env.typdef ] as 'c, 'd)
        Bddapron.Env.O.t ->
        ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
        Cudd.Bdd.vt -> Apron.Tcons0.t array
      val lvar_split :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'e)
        Bddapron.Env.O.t ->
        'a list -> Cudd.Man.v Cudd.Bdd.t * Apron.Dim.t array
      val condition_of_tcons0 :
        ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
        Bddapron.Env.O.t ->
        Apron.Tcons0.t ->
        [ `Bool of bool | `Cond of 'Bddapron.Apronexpr.Condition.t ]
      val bdd_of_tcons0 :
        ('a, [> 'Bddapron.Env.typ ] as 'b,
         [> 'Bddapron.Env.typdef ] as 'c, 'd)
        Bddapron.Env.O.t ->
        ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
        Apron.Tcons0.t -> Cudd.Bdd.vt
      val bdd_of_tcons0_array :
        ('a, [> 'Bddapron.Env.typ ] as 'b,
         [> 'Bddapron.Env.typdef ] as 'c, 'd)
        Bddapron.Env.O.t ->
        ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
        Apron.Tcons0.t array -> Cudd.Bdd.vt
    end
  module ApronDD :
    sig
      type 'a leaf = 'Apron.Abstract0.t
      type 'a t = 'Bddapron.ApronDD.leaf Cudd.Mtbddc.t
      type 'a table = 'Bddapron.ApronDD.leaf Cudd.Mtbddc.table
      type 'a leaf_u = 'Bddapron.ApronDD.leaf Cudd.Mtbddc.unique
      type 'a global = {
        op_is_leq :
          ('Bddapron.ApronDD.leaf_u, 'Bddapron.ApronDD.leaf_u)
          Cudd.User.test2;
        op_join :
          ('Bddapron.ApronDD.leaf_u, 'Bddapron.ApronDD.leaf_u,
           'Bddapron.ApronDD.leaf_u)
          Cudd.User.op2;
        op_meet :
          ('Bddapron.ApronDD.leaf_u, 'Bddapron.ApronDD.leaf_u,
           'Bddapron.ApronDD.leaf_u)
          Cudd.User.op2;
        op_exist : 'Bddapron.ApronDD.leaf_u Cudd.User.exist;
      }
      type 'a man = {
        apron : 'Apron.Manager.t;
        table : 'Bddapron.ApronDD.table;
        oglobal : 'Bddapron.ApronDD.global option;
      }
      val make_table : 'Apron.Manager.t -> 'Bddapron.ApronDD.table
      val neutral_join : 'Apron.Abstract0.t -> bool
      val special_is_leq :
        'Apron.Manager.t ->
        'Bddapron.ApronDD.t -> 'Bddapron.ApronDD.t -> bool option
      val special_join :
        'Apron.Manager.t ->
        'Bddapron.ApronDD.t ->
        'Bddapron.ApronDD.t -> 'Bddapron.ApronDD.t option
      val special_meet :
        'Apron.Manager.t ->
        'Bddapron.ApronDD.t ->
        'Bddapron.ApronDD.t -> 'Bddapron.ApronDD.t option
      val make_global :
        'Apron.Manager.t ->
        'Bddapron.ApronDD.table -> 'Bddapron.ApronDD.global
      val make_man :
        ?global:bool -> 'Apron.Manager.t -> 'Bddapron.ApronDD.man
      val make_op_join :
        'Bddapron.ApronDD.man ->
        ('Bddapron.ApronDD.leaf_u, 'Bddapron.ApronDD.leaf_u,
         'Bddapron.ApronDD.leaf_u)
        Cudd.User.op2
      val print :
        ?print_apron:((int -> string) ->
                      Format.formatter -> 'Apron.Abstract0.t -> unit) ->
        (Format.formatter -> Cudd.Bdd.vt -> unit) ->
        (int -> string) -> Format.formatter -> 'Bddapron.ApronDD.t -> unit
      val cst :
        cudd:Cudd.Man.vt ->
        'Bddapron.ApronDD.man ->
        'Apron.Abstract0.t -> 'Bddapron.ApronDD.t
      val bottom :
        cudd:Cudd.Man.vt ->
        'Bddapron.ApronDD.man ->
        Apron.Dim.dimension -> 'Bddapron.ApronDD.t
      val top :
        cudd:Cudd.Man.vt ->
        'Bddapron.ApronDD.man ->
        Apron.Dim.dimension -> 'Bddapron.ApronDD.t
      val is_bottom :
        'Bddapron.ApronDD.man -> 'Bddapron.ApronDD.t -> bool
      val is_top : 'Bddapron.ApronDD.man -> 'Bddapron.ApronDD.t -> bool
      val is_eq :
        'Bddapron.ApronDD.man ->
        'Bddapron.ApronDD.t -> 'Bddapron.ApronDD.t -> bool
      val is_leq :
        'Bddapron.ApronDD.man ->
        'Bddapron.ApronDD.t -> 'Bddapron.ApronDD.t -> bool
      val join :
        'Bddapron.ApronDD.man ->
        'Bddapron.ApronDD.t ->
        'Bddapron.ApronDD.t -> 'Bddapron.ApronDD.t
      val meet :
        'Bddapron.ApronDD.man ->
        'Bddapron.ApronDD.t ->
        'Bddapron.ApronDD.t -> 'Bddapron.ApronDD.t
      val widening :
        'Bddapron.ApronDD.man ->
        'Bddapron.ApronDD.t ->
        'Bddapron.ApronDD.t -> 'Bddapron.ApronDD.t
      val widening_threshold :
        'Bddapron.ApronDD.man ->
        'Bddapron.ApronDD.t ->
        'Bddapron.ApronDD.t ->
        Apron.Lincons0.t array -> 'Bddapron.ApronDD.t
      val meet_tcons_array :
        'Bddapron.ApronDD.man ->
        'Bddapron.ApronDD.t ->
        Apron.Tcons0.t array -> 'Bddapron.ApronDD.t
      val forget_array :
        'Bddapron.ApronDD.man ->
        'Bddapron.ApronDD.t -> Apron.Dim.t array -> 'Bddapron.ApronDD.t
      val permute_dimensions :
        'Bddapron.ApronDD.man ->
        'Bddapron.ApronDD.t -> Apron.Dim.perm -> 'Bddapron.ApronDD.t
      val add_dimensions :
        'Bddapron.ApronDD.man ->
        'Bddapron.ApronDD.t ->
        Apron.Dim.change -> bool -> 'Bddapron.ApronDD.t
      val remove_dimensions :
        'Bddapron.ApronDD.man ->
        'Bddapron.ApronDD.t -> Apron.Dim.change -> 'Bddapron.ApronDD.t
      val apply_dimchange2 :
        'Bddapron.ApronDD.man ->
        'Bddapron.ApronDD.t ->
        Apron.Dim.change2 -> bool -> 'Bddapron.ApronDD.t
      type asssub = Assign | Substitute
      val asssub_texpr_array :
        ?asssub_bdd:(Cudd.Bdd.vt -> Cudd.Bdd.vt) ->
        Bddapron.ApronDD.asssub ->
        'Bdd.Env.symbol ->
        'Bddapron.ApronDD.man ->
        Apron.Environment.t ->
        'Bddapron.ApronDD.t ->
        Apron.Dim.t array ->
        'Bddapron.ApronexprDD.t array ->
        'Bddapron.ApronDD.t option -> 'Bddapron.ApronDD.t
      val assign_texpr_array :
        'Bdd.Env.symbol ->
        'Bddapron.ApronDD.man ->
        Apron.Environment.t ->
        'Bddapron.ApronDD.t ->
        Apron.Dim.t array ->
        'Bddapron.ApronexprDD.t array ->
        'Bddapron.ApronDD.t option -> 'Bddapron.ApronDD.t
      val substitute_texpr_array :
        'Bdd.Env.symbol ->
        'Bddapron.ApronDD.man ->
        Apron.Environment.t ->
        'Bddapron.ApronDD.t ->
        Apron.Dim.t array ->
        'Bddapron.ApronexprDD.t array ->
        'Bddapron.ApronDD.t option -> 'Bddapron.ApronDD.t
      val exist :
        'Bddapron.ApronDD.man ->
        supp:Cudd.Bdd.vt -> 'Bddapron.ApronDD.t -> 'Bddapron.ApronDD.t
      val existand :
        'Bddapron.ApronDD.man ->
        bottom:'Apron.Abstract0.t Cudd.Mtbddc.unique ->
        supp:Cudd.Bdd.vt ->
        Cudd.Bdd.vt -> 'Bddapron.ApronDD.t -> 'Bddapron.ApronDD.t
    end
  module Expr0 :
    sig
      type 'a t =
          [ `Apron of 'Bddapron.ApronexprDD.t
          | `Benum of Cudd.Man.v Bdd.Enum.t
          | `Bint of Cudd.Man.v Bdd.Int.t
          | `Bool of Cudd.Man.v Cudd.Bdd.t ]
      type 'a expr = 'Bddapron.Expr0.t
      module Bool :
        sig
          type 'a t = Cudd.Bdd.vt
          val of_expr : 'Bddapron.Expr0.expr -> 'Bddapron.Expr0.Bool.t
          val to_expr : 'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.expr
          val dtrue :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t -> 'Bddapron.Expr0.Bool.t
          val dfalse :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t -> 'Bddapron.Expr0.Bool.t
          val of_bool :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t -> bool -> 'Bddapron.Expr0.Bool.t
          val var :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t -> '-> 'Bddapron.Expr0.Bool.t
          val ite :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bool.t ->
            'Bddapron.Expr0.Bool.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bool.t
          val dnot :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bool.t
          val dand :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bool.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bool.t
          val dor :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bool.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bool.t
          val xor :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bool.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bool.t
          val nand :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bool.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bool.t
          val nor :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bool.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bool.t
          val nxor :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bool.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bool.t
          val leq :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bool.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bool.t
          val eq :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bool.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bool.t
          val is_true :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t -> 'Bddapron.Expr0.Bool.t -> bool
          val is_false :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t -> 'Bddapron.Expr0.Bool.t -> bool
          val is_cst :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t -> 'Bddapron.Expr0.Bool.t -> bool
          val is_leq :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bool.t -> bool
          val is_eq :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bool.t -> bool
          val is_and_false :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bool.t -> bool
          val exist :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'a list -> 'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bool.t
          val forall :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'a list -> 'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bool.t
          val cofactor :
            'Bddapron.Expr0.Bool.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bool.t
          val restrict :
            'Bddapron.Expr0.Bool.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bool.t
          val tdrestrict :
            'Bddapron.Expr0.Bool.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bool.t
          val permute :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Expr0.Bool.t -> int array -> 'Bddapron.Expr0.Bool.t
          val varmap : 'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bool.t
          val substitute_by_var :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bool.t ->
            ('a * 'a) list -> 'Bddapron.Expr0.Bool.t
          val substitute :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bool.t ->
            ('a * 'Bddapron.Expr0.expr) list -> 'Bddapron.Expr0.Bool.t
          val print :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            Format.formatter -> 'Bddapron.Expr0.Bool.t -> unit
        end
      module Bint :
        sig
          type 'a t = Cudd.Man.v Bdd.Int.t
          val of_expr : 'Bddapron.Expr0.expr -> 'Bddapron.Expr0.Bint.t
          val to_expr : 'Bddapron.Expr0.Bint.t -> 'Bddapron.Expr0.expr
          val of_int :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            [ `Bint of bool * int ] -> int -> 'Bddapron.Expr0.Bint.t
          val var :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t -> '-> 'Bddapron.Expr0.Bint.t
          val ite :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bool.t ->
            'Bddapron.Expr0.Bint.t ->
            'Bddapron.Expr0.Bint.t -> 'Bddapron.Expr0.Bint.t
          val neg :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bint.t -> 'Bddapron.Expr0.Bint.t
          val succ :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bint.t -> 'Bddapron.Expr0.Bint.t
          val pred :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bint.t -> 'Bddapron.Expr0.Bint.t
          val add :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bint.t ->
            'Bddapron.Expr0.Bint.t -> 'Bddapron.Expr0.Bint.t
          val sub :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bint.t ->
            'Bddapron.Expr0.Bint.t -> 'Bddapron.Expr0.Bint.t
          val mul :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bint.t ->
            'Bddapron.Expr0.Bint.t -> 'Bddapron.Expr0.Bint.t
          val shift_left :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            int -> 'Bddapron.Expr0.Bint.t -> 'Bddapron.Expr0.Bint.t
          val shift_right :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            int -> 'Bddapron.Expr0.Bint.t -> 'Bddapron.Expr0.Bint.t
          val scale :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            int -> 'Bddapron.Expr0.Bint.t -> 'Bddapron.Expr0.Bint.t
          val zero :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bint.t -> 'Bddapron.Expr0.Bool.t
          val eq :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bint.t ->
            'Bddapron.Expr0.Bint.t -> 'Bddapron.Expr0.Bool.t
          val eq_int :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bint.t -> int -> 'Bddapron.Expr0.Bool.t
          val supeq :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bint.t ->
            'Bddapron.Expr0.Bint.t -> 'Bddapron.Expr0.Bool.t
          val supeq_int :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bint.t -> int -> 'Bddapron.Expr0.Bool.t
          val sup :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bint.t ->
            'Bddapron.Expr0.Bint.t -> 'Bddapron.Expr0.Bool.t
          val sup_int :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bint.t -> int -> 'Bddapron.Expr0.Bool.t
          val cofactor :
            'Bddapron.Expr0.Bint.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bint.t
          val restrict :
            'Bddapron.Expr0.Bint.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bint.t
          val tdrestrict :
            'Bddapron.Expr0.Bint.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Bint.t
          val permute :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Expr0.Bint.t -> int array -> 'Bddapron.Expr0.Bint.t
          val varmap : 'Bddapron.Expr0.Bint.t -> 'Bddapron.Expr0.Bint.t
          val substitute_by_var :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bint.t ->
            ('a * 'a) list -> 'Bddapron.Expr0.Bint.t
          val substitute :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bint.t ->
            ('a * 'Bddapron.Expr0.expr) list -> 'Bddapron.Expr0.Bint.t
          val print :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            Format.formatter -> 'Bddapron.Expr0.Bint.t -> unit
        end
      module Benum :
        sig
          type 'a t = Cudd.Man.v Bdd.Enum.t
          val of_expr : 'Bddapron.Expr0.expr -> 'Bddapron.Expr0.Benum.t
          val to_expr : 'Bddapron.Expr0.Benum.t -> 'Bddapron.Expr0.expr
          val var :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t -> '-> 'Bddapron.Expr0.Benum.t
          val ite :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bool.t ->
            'Bddapron.Expr0.Benum.t ->
            'Bddapron.Expr0.Benum.t -> 'Bddapron.Expr0.Benum.t
          val eq :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Benum.t ->
            'Bddapron.Expr0.Benum.t -> 'Bddapron.Expr0.Bool.t
          val eq_label :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Benum.t -> '-> 'Bddapron.Expr0.Bool.t
          val cofactor :
            'Bddapron.Expr0.Benum.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Benum.t
          val restrict :
            'Bddapron.Expr0.Benum.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Benum.t
          val tdrestrict :
            'Bddapron.Expr0.Benum.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Benum.t
          val permute :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Expr0.Benum.t ->
            int array -> 'Bddapron.Expr0.Benum.t
          val varmap : 'Bddapron.Expr0.Benum.t -> 'Bddapron.Expr0.Benum.t
          val substitute_by_var :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Benum.t ->
            ('a * 'a) list -> 'Bddapron.Expr0.Benum.t
          val substitute :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Benum.t ->
            ('a * 'Bddapron.Expr0.expr) list -> 'Bddapron.Expr0.Benum.t
          val print :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            Format.formatter -> 'Bddapron.Expr0.Benum.t -> unit
        end
      type apron_coeff = Apron.Coeff.t
      type apron_typ = Apron.Texpr1.typ
      type apron_round = Apron.Texpr1.round
      module Apron :
        sig
          type 'a t = 'Bddapron.ApronexprDD.t
          val of_expr : 'Bddapron.Expr0.expr -> 'Bddapron.Expr0.Apron.t
          val to_expr : 'Bddapron.Expr0.Apron.t -> 'Bddapron.Expr0.expr
          val cst :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t -> Apron.Coeff.t -> 'Bddapron.Expr0.Apron.t
          val var :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t -> '-> 'Bddapron.Expr0.Apron.t
          val add :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            ?typ:Apron.Texpr1.typ ->
            ?round:Apron.Texpr1.round ->
            'Bddapron.Expr0.Apron.t ->
            'Bddapron.Expr0.Apron.t -> 'Bddapron.Expr0.Apron.t
          val sub :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            ?typ:Apron.Texpr1.typ ->
            ?round:Apron.Texpr1.round ->
            'Bddapron.Expr0.Apron.t ->
            'Bddapron.Expr0.Apron.t -> 'Bddapron.Expr0.Apron.t
          val mul :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            ?typ:Apron.Texpr1.typ ->
            ?round:Apron.Texpr1.round ->
            'Bddapron.Expr0.Apron.t ->
            'Bddapron.Expr0.Apron.t -> 'Bddapron.Expr0.Apron.t
          val div :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            ?typ:Apron.Texpr1.typ ->
            ?round:Apron.Texpr1.round ->
            'Bddapron.Expr0.Apron.t ->
            'Bddapron.Expr0.Apron.t -> 'Bddapron.Expr0.Apron.t
          val gmod :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            ?typ:Apron.Texpr1.typ ->
            ?round:Apron.Texpr1.round ->
            'Bddapron.Expr0.Apron.t ->
            'Bddapron.Expr0.Apron.t -> 'Bddapron.Expr0.Apron.t
          val negate :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Apron.t -> 'Bddapron.Expr0.Apron.t
          val cast :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            ?typ:Apron.Texpr1.typ ->
            ?round:Apron.Texpr1.round ->
            'Bddapron.Expr0.Apron.t -> 'Bddapron.Expr0.Apron.t
          val sqrt :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            ?typ:Apron.Texpr1.typ ->
            ?round:Apron.Texpr1.round ->
            'Bddapron.Expr0.Apron.t -> 'Bddapron.Expr0.Apron.t
          val supeq :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Apron.t -> 'Bddapron.Expr0.Bool.t
          val sup :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Apron.t -> 'Bddapron.Expr0.Bool.t
          val eq :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Apron.t -> 'Bddapron.Expr0.Bool.t
          val ite :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Bool.t ->
            'Bddapron.Expr0.Apron.t ->
            'Bddapron.Expr0.Apron.t -> 'Bddapron.Expr0.Apron.t
          val cofactor :
            'Bddapron.Expr0.Apron.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Apron.t
          val restrict :
            'Bddapron.Expr0.Apron.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Apron.t
          val tdrestrict :
            'Bddapron.Expr0.Apron.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.Apron.t
          val permute :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Expr0.Apron.t ->
            int array -> 'Bddapron.Expr0.Apron.t
          val varmap : 'Bddapron.Expr0.Apron.t -> 'Bddapron.Expr0.Apron.t
          val substitute_by_var :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Apron.t ->
            ('a * 'a) list -> 'Bddapron.Expr0.Apron.t
          val substitute :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr0.Apron.t ->
            ('a * 'Bddapron.Expr0.expr) list -> 'Bddapron.Expr0.Apron.t
          val print :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            Format.formatter -> 'Bddapron.Expr0.Apron.t -> unit
        end
      val typ_of_expr :
        'Bddapron.Env.t -> 'Bddapron.Expr0.t -> 'Bddapron.Env.typ
      val var :
        'Bddapron.Env.t -> 'Bddapron.Cond.t -> '-> 'Bddapron.Expr0.t
      val ite :
        'Bddapron.Env.t ->
        'Bddapron.Cond.t ->
        'Bddapron.Expr0.Bool.t ->
        'Bddapron.Expr0.t -> 'Bddapron.Expr0.t -> 'Bddapron.Expr0.t
      val cofactor :
        'Bddapron.Expr0.t ->
        'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.t
      val substitute_by_var :
        ?memo:Cudd.Memo.t ->
        'Bddapron.Env.t ->
        'Bddapron.Cond.t ->
        'Bddapron.Expr0.t -> ('a * 'a) list -> 'Bddapron.Expr0.t
      val substitute_by_var_list :
        ?memo:Cudd.Memo.t ->
        'Bddapron.Env.t ->
        'Bddapron.Cond.t ->
        'Bddapron.Expr0.t list ->
        ('a * 'a) list -> 'Bddapron.Expr0.t list
      val substitute :
        ?memo:Cudd.Memo.t ->
        'Bddapron.Env.t ->
        'Bddapron.Cond.t ->
        'Bddapron.Expr0.t ->
        ('a * 'Bddapron.Expr0.t) list -> 'Bddapron.Expr0.t
      val substitute_list :
        ?memo:Cudd.Memo.t ->
        'Bddapron.Env.t ->
        'Bddapron.Cond.t ->
        'Bddapron.Expr0.t list ->
        ('a * 'Bddapron.Expr0.t) list -> 'Bddapron.Expr0.t list
      val restrict :
        'Bddapron.Expr0.t ->
        'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.t
      val tdrestrict :
        'Bddapron.Expr0.t ->
        'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr0.t
      val permute :
        ?memo:Cudd.Memo.t ->
        'Bddapron.Expr0.t -> int array -> 'Bddapron.Expr0.t
      val varmap : 'Bddapron.Expr0.t -> 'Bddapron.Expr0.t
      val support :
        'Bddapron.Env.t ->
        'Bddapron.Cond.t -> 'Bddapron.Expr0.t -> 'PSette.t
      val eq :
        'Bddapron.Env.t ->
        'Bddapron.Cond.t ->
        'Bddapron.Expr0.t ->
        'Bddapron.Expr0.t -> 'Bddapron.Expr0.Bool.t
      val support_cond : Cudd.Man.vt -> 'Bddapron.Expr0.t -> Cudd.Bdd.vt
      val print :
        'Bddapron.Env.t ->
        'Bddapron.Cond.t ->
        Format.formatter -> [< 'Bddapron.Expr0.t ] -> unit
      val normalize :
        ?reduce:bool ->
        ?careset:bool ->
        'Bddapron.Cond.t * 'Bddapron.Expr0.t list ->
        'Bddapron.Cond.t * 'Bddapron.Expr0.t list
      module O :
        sig
          val check_typ2 :
            ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
            Bddapron.Env.O.t ->
            [< 'Bddapron.Expr0.t ] ->
            [< 'Bddapron.Expr0.t ] -> 'Bddapron.Env.typ
          module Bool :
            sig
              type 'a t = Cudd.Bdd.vt
              val of_expr :
                'Bddapron.Expr0.expr -> 'Bddapron.Expr0.O.Bool.t
              val to_expr :
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.expr
              val dtrue :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t
              val dfalse :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t
              val of_bool :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                bool -> 'Bddapron.Expr0.O.Bool.t
              val var :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                '-> 'Bddapron.Expr0.O.Bool.t
              val ite :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t ->
                'Bddapron.Expr0.O.Bool.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Bool.t
              val dnot :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Bool.t
              val dand :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Bool.t
              val dor :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Bool.t
              val xor :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Bool.t
              val nand :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Bool.t
              val nor :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Bool.t
              val nxor :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Bool.t
              val leq :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Bool.t
              val eq :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Bool.t
              val is_true :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t -> bool
              val is_false :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t -> bool
              val is_cst :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t -> bool
              val is_leq :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t ->
                'Bddapron.Expr0.O.Bool.t -> bool
              val is_eq :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t ->
                'Bddapron.Expr0.O.Bool.t -> bool
              val is_and_false :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t ->
                'Bddapron.Expr0.O.Bool.t -> bool
              val exist :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'a list ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Bool.t
              val forall :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'a list ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Bool.t
              val cofactor :
                'Bddapron.Expr0.O.Bool.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Bool.t
              val restrict :
                'Bddapron.Expr0.O.Bool.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Bool.t
              val tdrestrict :
                'Bddapron.Expr0.O.Bool.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Bool.t
              val permute :
                ?memo:Cudd.Memo.t ->
                'Bddapron.Expr0.O.Bool.t ->
                int array -> 'Bddapron.Expr0.O.Bool.t
              val varmap :
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Bool.t
              val substitute_by_var :
                ?memo:Cudd.Memo.t ->
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t ->
                ('a * 'a) list -> 'Bddapron.Expr0.O.Bool.t
              val substitute :
                ?memo:Cudd.Memo.t ->
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t ->
                ('a * 'Bddapron.Expr0.expr) list ->
                'Bddapron.Expr0.O.Bool.t
              val print :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                Format.formatter -> 'Bddapron.Expr0.O.Bool.t -> unit
            end
          module Bint :
            sig
              type 'a t = Cudd.Man.v Bdd.Int.t
              val of_expr :
                'Bddapron.Expr0.expr -> 'Bddapron.Expr0.O.Bint.t
              val to_expr :
                'Bddapron.Expr0.O.Bint.t -> 'Bddapron.Expr0.expr
              val of_int :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                [> `Bint of bool * int ] -> int -> 'Bddapron.Expr0.O.Bint.t
              val var :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                '-> 'Bddapron.Expr0.O.Bint.t
              val ite :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t ->
                'Bddapron.Expr0.O.Bint.t ->
                'Bddapron.Expr0.O.Bint.t -> 'Bddapron.Expr0.O.Bint.t
              val neg :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bint.t -> 'Bddapron.Expr0.O.Bint.t
              val succ :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bint.t -> 'Bddapron.Expr0.O.Bint.t
              val pred :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bint.t -> 'Bddapron.Expr0.O.Bint.t
              val add :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bint.t ->
                'Bddapron.Expr0.O.Bint.t -> 'Bddapron.Expr0.O.Bint.t
              val sub :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bint.t ->
                'Bddapron.Expr0.O.Bint.t -> 'Bddapron.Expr0.O.Bint.t
              val mul :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bint.t ->
                'Bddapron.Expr0.O.Bint.t -> 'Bddapron.Expr0.O.Bint.t
              val shift_left :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                int ->
                'Bddapron.Expr0.O.Bint.t -> 'Bddapron.Expr0.O.Bint.t
              val shift_right :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                int ->
                'Bddapron.Expr0.O.Bint.t -> 'Bddapron.Expr0.O.Bint.t
              val scale :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                int ->
                'Bddapron.Expr0.O.Bint.t -> 'Bddapron.Expr0.O.Bint.t
              val zero :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bint.t -> 'Bddapron.Expr0.O.Bool.t
              val eq :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bint.t ->
                'Bddapron.Expr0.O.Bint.t -> 'Bddapron.Expr0.O.Bool.t
              val eq_int :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bint.t ->
                int -> 'Bddapron.Expr0.O.Bool.t
              val supeq :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bint.t ->
                'Bddapron.Expr0.O.Bint.t -> 'Bddapron.Expr0.O.Bool.t
              val supeq_int :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bint.t ->
                int -> 'Bddapron.Expr0.O.Bool.t
              val sup :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bint.t ->
                'Bddapron.Expr0.O.Bint.t -> 'Bddapron.Expr0.O.Bool.t
              val sup_int :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bint.t ->
                int -> 'Bddapron.Expr0.O.Bool.t
              val cofactor :
                'Bddapron.Expr0.O.Bint.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Bint.t
              val restrict :
                'Bddapron.Expr0.O.Bint.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Bint.t
              val tdrestrict :
                'Bddapron.Expr0.O.Bint.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Bint.t
              val permute :
                ?memo:Cudd.Memo.t ->
                'Bddapron.Expr0.O.Bint.t ->
                int array -> 'Bddapron.Expr0.O.Bint.t
              val varmap :
                'Bddapron.Expr0.O.Bint.t -> 'Bddapron.Expr0.O.Bint.t
              val substitute_by_var :
                ?memo:Cudd.Memo.t ->
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bint.t ->
                ('a * 'a) list -> 'Bddapron.Expr0.O.Bint.t
              val substitute :
                ?memo:Cudd.Memo.t ->
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bint.t ->
                ('a * 'Bddapron.Expr0.expr) list ->
                'Bddapron.Expr0.O.Bint.t
              val print :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                Format.formatter -> 'Bddapron.Expr0.O.Bint.t -> unit
            end
          module Benum :
            sig
              type 'a t = Cudd.Man.v Bdd.Enum.t
              val of_expr :
                'Bddapron.Expr0.expr -> 'Bddapron.Expr0.O.Benum.t
              val to_expr :
                'Bddapron.Expr0.O.Benum.t -> 'Bddapron.Expr0.expr
              val var :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                '-> 'Bddapron.Expr0.O.Benum.t
              val ite :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t ->
                'Bddapron.Expr0.O.Benum.t ->
                'Bddapron.Expr0.O.Benum.t -> 'Bddapron.Expr0.O.Benum.t
              val eq :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Benum.t ->
                'Bddapron.Expr0.O.Benum.t -> 'Bddapron.Expr0.O.Bool.t
              val eq_label :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Benum.t ->
                '-> 'Bddapron.Expr0.O.Bool.t
              val cofactor :
                'Bddapron.Expr0.O.Benum.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Benum.t
              val restrict :
                'Bddapron.Expr0.O.Benum.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Benum.t
              val tdrestrict :
                'Bddapron.Expr0.O.Benum.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Benum.t
              val permute :
                ?memo:Cudd.Memo.t ->
                'Bddapron.Expr0.O.Benum.t ->
                int array -> 'Bddapron.Expr0.O.Benum.t
              val varmap :
                'Bddapron.Expr0.O.Benum.t -> 'Bddapron.Expr0.O.Benum.t
              val substitute_by_var :
                ?memo:Cudd.Memo.t ->
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Benum.t ->
                ('a * 'a) list -> 'Bddapron.Expr0.O.Benum.t
              val substitute :
                ?memo:Cudd.Memo.t ->
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Benum.t ->
                ('a * 'Bddapron.Expr0.expr) list ->
                'Bddapron.Expr0.O.Benum.t
              val print :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                Format.formatter -> 'Bddapron.Expr0.O.Benum.t -> unit
            end
          module Apron :
            sig
              type 'a t = 'Bddapron.ApronexprDD.t
              val of_expr :
                [> `Apron of 'Bddapron.Expr0.O.Apron.t ] ->
                'Bddapron.Expr0.O.Apron.t
              val to_expr :
                'Bddapron.Expr0.O.Apron.t ->
                [> `Apron of 'Bddapron.Expr0.O.Apron.t ]
              val cst :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                Bddapron.Expr0.apron_coeff -> 'Bddapron.Expr0.O.Apron.t
              val var :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                '-> 'Bddapron.Expr0.O.Apron.t
              val add :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                ?typ:Bddapron.Expr0.apron_typ ->
                ?round:Bddapron.Expr0.apron_round ->
                'Bddapron.Expr0.O.Apron.t ->
                'Bddapron.Expr0.O.Apron.t -> 'Bddapron.Expr0.O.Apron.t
              val sub :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                ?typ:Bddapron.Expr0.apron_typ ->
                ?round:Bddapron.Expr0.apron_round ->
                'Bddapron.Expr0.O.Apron.t ->
                'Bddapron.Expr0.O.Apron.t -> 'Bddapron.Expr0.O.Apron.t
              val mul :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                ?typ:Bddapron.Expr0.apron_typ ->
                ?round:Bddapron.Expr0.apron_round ->
                'Bddapron.Expr0.O.Apron.t ->
                'Bddapron.Expr0.O.Apron.t -> 'Bddapron.Expr0.O.Apron.t
              val div :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                ?typ:Bddapron.Expr0.apron_typ ->
                ?round:Bddapron.Expr0.apron_round ->
                'Bddapron.Expr0.O.Apron.t ->
                'Bddapron.Expr0.O.Apron.t -> 'Bddapron.Expr0.O.Apron.t
              val gmod :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                ?typ:Bddapron.Expr0.apron_typ ->
                ?round:Bddapron.Expr0.apron_round ->
                'Bddapron.Expr0.O.Apron.t ->
                'Bddapron.Expr0.O.Apron.t -> 'Bddapron.Expr0.O.Apron.t
              val negate :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Apron.t -> 'Bddapron.Expr0.O.Apron.t
              val cast :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                ?typ:Bddapron.Expr0.apron_typ ->
                ?round:Bddapron.Expr0.apron_round ->
                'Bddapron.Expr0.O.Apron.t -> 'Bddapron.Expr0.O.Apron.t
              val sqrt :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                ?typ:Bddapron.Expr0.apron_typ ->
                ?round:Bddapron.Expr0.apron_round ->
                'Bddapron.Expr0.O.Apron.t -> 'Bddapron.Expr0.O.Apron.t
              val supeq :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Apron.t -> 'Bddapron.Expr0.O.Bool.t
              val sup :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Apron.t -> 'Bddapron.Expr0.O.Bool.t
              val eq :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Apron.t -> 'Bddapron.Expr0.O.Bool.t
              val ite :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Bool.t ->
                'Bddapron.Expr0.O.Apron.t ->
                'Bddapron.Expr0.O.Apron.t -> 'Bddapron.Expr0.O.Apron.t
              val cofactor :
                'Bddapron.Expr0.O.Apron.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Apron.t
              val restrict :
                'Bddapron.Expr0.O.Apron.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Apron.t
              val tdrestrict :
                'Bddapron.Expr0.O.Apron.t ->
                'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.O.Apron.t
              val permute :
                ?memo:Cudd.Memo.t ->
                'Bddapron.Expr0.O.Apron.t ->
                int array -> 'Bddapron.Expr0.O.Apron.t
              val varmap :
                'Bddapron.Expr0.O.Apron.t -> 'Bddapron.Expr0.O.Apron.t
              val substitute_by_var :
                ?memo:Cudd.Memo.t ->
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Apron.t ->
                ('a * 'a) list -> 'Bddapron.Expr0.O.Apron.t
              val substitute :
                ?memo:Cudd.Memo.t ->
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                'Bddapron.Expr0.O.Apron.t ->
                ('a * 'Bddapron.Expr0.expr) list ->
                'Bddapron.Expr0.O.Apron.t
              val print :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                Format.formatter -> 'Bddapron.Expr0.O.Apron.t -> unit
            end
          val typ_of_expr :
            ('a, [> 'Bddapron.Env.typ ], [> 'Bddapron.Env.typdef ], 'd)
            Bddapron.Env.O.t ->
            [< 'Bddapron.Expr0.t ] -> 'Bddapron.Env.typ
          val var :
            ('a, [> 'Bddapron.Env.typ ] as 'b,
             [> 'Bddapron.Env.typdef ] as 'c, 'd)
            Bddapron.Env.O.t ->
            ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
            '-> 'Bddapron.Expr0.t
          val ite :
            ('a, [> 'Bddapron.Env.typ ] as 'b,
             [> 'Bddapron.Env.typdef ] as 'c, 'd)
            Bddapron.Env.O.t ->
            ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
            'Bddapron.Expr0.O.Bool.t ->
            'Bddapron.Expr0.t -> 'Bddapron.Expr0.t -> 'Bddapron.Expr0.t
          val cofactor :
            'Bddapron.Expr0.t ->
            'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.t
          val restrict :
            'Bddapron.Expr0.t ->
            'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.t
          val tdrestrict :
            'Bddapron.Expr0.t ->
            'Bddapron.Expr0.O.Bool.t -> 'Bddapron.Expr0.t
          val permute :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Expr0.t -> int array -> 'Bddapron.Expr0.t
          val permute_list :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Expr0.t list -> int array -> 'Bddapron.Expr0.t list
          val varmap : 'Bddapron.Expr0.t -> 'Bddapron.Expr0.t
          val substitute_by_var :
            ?memo:Cudd.Memo.t ->
            ('a, [> 'Bddapron.Env.typ ] as 'b,
             [> 'Bddapron.Env.typdef ] as 'c, 'd)
            Bddapron.Env.O.t ->
            ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
            'Bddapron.Expr0.t -> ('a * 'a) list -> 'Bddapron.Expr0.t
          val substitute_by_var_list :
            ?memo:Cudd.Memo.t ->
            ('a, [> 'Bddapron.Env.typ ] as 'b,
             [> 'Bddapron.Env.typdef ] as 'c, 'd)
            Bddapron.Env.O.t ->
            ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
            'Bddapron.Expr0.t list ->
            ('a * 'a) list -> 'Bddapron.Expr0.t list
          val substitute :
            ?memo:Cudd.Memo.t ->
            ('a, [> 'Bddapron.Env.typ ] as 'b,
             [> 'Bddapron.Env.typdef ] as 'c, 'd)
            Bddapron.Env.O.t ->
            ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
            'Bddapron.Expr0.t ->
            ('a * 'Bddapron.Expr0.t) list -> 'Bddapron.Expr0.t
          val substitute_list :
            ?memo:Cudd.Memo.t ->
            ('a, [> 'Bddapron.Env.typ ] as 'b,
             [> 'Bddapron.Env.typdef ] as 'c, 'd)
            Bddapron.Env.O.t ->
            ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
            'Bddapron.Expr0.t list ->
            ('a * 'Bddapron.Expr0.t) list -> 'Bddapron.Expr0.t list
          val support :
            ('a, [> 'Bddapron.Env.typ ] as 'b,
             [> 'Bddapron.Env.typdef ] as 'c, 'd)
            Bddapron.Env.O.t ->
            ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
            'Bddapron.Expr0.t -> 'PSette.t
          val eq :
            ('a, [> 'Bddapron.Env.typ ] as 'b,
             [> 'Bddapron.Env.typdef ] as 'c, 'd)
            Bddapron.Env.O.t ->
            ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
            'Bddapron.Expr0.t ->
            'Bddapron.Expr0.t -> 'Bddapron.Expr0.O.Bool.t
          val support_cond :
            Cudd.Man.vt -> 'Bddapron.Expr0.t -> Cudd.Bdd.vt
          val print :
            ('a, [> 'Bddapron.Env.typ ] as 'b,
             [> 'Bddapron.Env.typdef ] as 'c, 'd)
            Bddapron.Env.O.t ->
            ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
            Format.formatter -> [< 'Bddapron.Expr0.t ] -> unit
          val print_bdd :
            ('a, [> 'Bddapron.Env.typ ] as 'b,
             [> 'Bddapron.Env.typdef ] as 'c, 'd)
            Bddapron.Env.O.t ->
            ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
            Format.formatter -> Cudd.Bdd.vt -> unit
          val normalize :
            ?reduce:bool ->
            ?careset:bool ->
            ('a,
             ('a, [> 'Bddapron.Env.typ ] as 'b,
              [> 'Bddapron.Env.typdef ] as 'c, 'd)
             Bddapron.Env.O.t)
            Bddapron.Cond.O.t * 'Bddapron.Expr0.t list ->
            ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t *
            'Bddapron.Expr0.t list
          val compose_of_lvarexpr :
            ('a, [> 'Bddapron.Env.typ ] as 'b,
             [> 'Bddapron.Env.typdef ] as 'c, 'd)
            Bddapron.Env.O.t ->
            ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
            ('a * 'Bddapron.Expr0.t) list ->
            Cudd.Bdd.vt array option * ('a, 'Bddapron.Expr0.t) PMappe.t
        end
    end
  module Expr1 :
    sig
      type 'a t = ('Bddapron.Env.t, 'Bddapron.Expr0.t) Bddapron.Env.value
      type 'a expr = 'Bddapron.Expr1.t
      module Bool :
        sig
          type 'a t =
              ('Bddapron.Env.t, Cudd.Man.v Bddapron.Expr0.Bool.t)
              Bddapron.Env.value
          val of_expr0 :
            'Bddapron.Env.t ->
            'Bddapron.Expr0.Bool.t -> 'Bddapron.Expr1.Bool.t
          val get_env : 'Bddapron.Expr1.Bool.t -> 'Bddapron.Env.t
          val to_expr0 : 'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr0.Bool.t
          val of_expr : 'Bddapron.Expr1.expr -> 'Bddapron.Expr1.Bool.t
          val to_expr : 'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.expr
          val extend_environment :
            'Bddapron.Expr1.Bool.t ->
            'Bddapron.Env.t -> 'Bddapron.Expr1.Bool.t
          val dtrue :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t -> 'Bddapron.Expr1.Bool.t
          val dfalse :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t -> 'Bddapron.Expr1.Bool.t
          val of_bool :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t -> bool -> 'Bddapron.Expr1.Bool.t
          val var :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t -> '-> 'Bddapron.Expr1.Bool.t
          val dnot :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bool.t
          val dand :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bool.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bool.t
          val dor :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bool.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bool.t
          val xor :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bool.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bool.t
          val nand :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bool.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bool.t
          val nor :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bool.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bool.t
          val nxor :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bool.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bool.t
          val eq :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bool.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bool.t
          val leq :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bool.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bool.t
          val ite :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bool.t ->
            'Bddapron.Expr1.Bool.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bool.t
          val is_true :
            'Bddapron.Cond.t -> 'Bddapron.Expr1.Bool.t -> bool
          val is_false :
            'Bddapron.Cond.t -> 'Bddapron.Expr1.Bool.t -> bool
          val is_cst : 'Bddapron.Cond.t -> 'Bddapron.Expr1.Bool.t -> bool
          val is_eq :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bool.t -> bool
          val is_leq :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bool.t -> bool
          val is_inter_false :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bool.t -> bool
          val exist :
            'Bddapron.Cond.t ->
            'a list -> 'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bool.t
          val forall :
            'Bddapron.Cond.t ->
            'a list -> 'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bool.t
          val cofactor :
            'Bddapron.Expr1.Bool.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bool.t
          val restrict :
            'Bddapron.Expr1.Bool.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bool.t
          val tdrestrict :
            'Bddapron.Expr1.Bool.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bool.t
          val substitute_by_var :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bool.t ->
            ('a * 'a) list -> 'Bddapron.Expr1.Bool.t
          val substitute :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bool.t ->
            ('a * 'Bddapron.Expr1.expr) list -> 'Bddapron.Expr1.Bool.t
          val print :
            'Bddapron.Cond.t ->
            Format.formatter -> 'Bddapron.Expr1.Bool.t -> unit
        end
      module Bint :
        sig
          type 'a t =
              ('Bddapron.Env.t, Cudd.Man.v Bdd.Int.t) Bddapron.Env.value
          val of_expr0 :
            'Bddapron.Env.t ->
            'Bddapron.Expr0.Bint.t -> 'Bddapron.Expr1.Bint.t
          val get_env : 'Bddapron.Expr1.Bint.t -> 'Bddapron.Env.t
          val to_expr0 : 'Bddapron.Expr1.Bint.t -> 'Bddapron.Expr0.Bint.t
          val of_expr : 'Bddapron.Expr1.expr -> 'Bddapron.Expr1.Bint.t
          val to_expr : 'Bddapron.Expr1.Bint.t -> 'Bddapron.Expr1.expr
          val extend_environment :
            'Bddapron.Expr1.Bint.t ->
            'Bddapron.Env.t -> 'Bddapron.Expr1.Bint.t
          val of_int :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t ->
            [ `Bint of bool * int ] -> int -> 'Bddapron.Expr1.Bint.t
          val var :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t -> '-> 'Bddapron.Expr1.Bint.t
          val neg :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bint.t -> 'Bddapron.Expr1.Bint.t
          val succ :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bint.t -> 'Bddapron.Expr1.Bint.t
          val pred :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bint.t -> 'Bddapron.Expr1.Bint.t
          val add :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bint.t ->
            'Bddapron.Expr1.Bint.t -> 'Bddapron.Expr1.Bint.t
          val sub :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bint.t ->
            'Bddapron.Expr1.Bint.t -> 'Bddapron.Expr1.Bint.t
          val mul :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bint.t ->
            'Bddapron.Expr1.Bint.t -> 'Bddapron.Expr1.Bint.t
          val shift_left :
            'Bddapron.Cond.t ->
            int -> 'Bddapron.Expr1.Bint.t -> 'Bddapron.Expr1.Bint.t
          val shift_right :
            'Bddapron.Cond.t ->
            int -> 'Bddapron.Expr1.Bint.t -> 'Bddapron.Expr1.Bint.t
          val scale :
            'Bddapron.Cond.t ->
            int -> 'Bddapron.Expr1.Bint.t -> 'Bddapron.Expr1.Bint.t
          val ite :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bool.t ->
            'Bddapron.Expr1.Bint.t ->
            'Bddapron.Expr1.Bint.t -> 'Bddapron.Expr1.Bint.t
          val zero :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bint.t -> 'Bddapron.Expr1.Bool.t
          val eq :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bint.t ->
            'Bddapron.Expr1.Bint.t -> 'Bddapron.Expr1.Bool.t
          val supeq :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bint.t ->
            'Bddapron.Expr1.Bint.t -> 'Bddapron.Expr1.Bool.t
          val sup :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bint.t ->
            'Bddapron.Expr1.Bint.t -> 'Bddapron.Expr1.Bool.t
          val eq_int :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bint.t -> int -> 'Bddapron.Expr1.Bool.t
          val supeq_int :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bint.t -> int -> 'Bddapron.Expr1.Bool.t
          val sup_int :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bint.t -> int -> 'Bddapron.Expr1.Bool.t
          val cofactor :
            'Bddapron.Expr1.Bint.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bint.t
          val restrict :
            'Bddapron.Expr1.Bint.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bint.t
          val tdrestrict :
            'Bddapron.Expr1.Bint.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Bint.t
          val substitute_by_var :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bint.t ->
            ('a * 'a) list -> 'Bddapron.Expr1.Bint.t
          val substitute :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bint.t ->
            ('a * 'Bddapron.Expr1.expr) list -> 'Bddapron.Expr1.Bint.t
          val guard_of_int :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bint.t -> int -> 'Bddapron.Expr1.Bool.t
          val guardints :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bint.t -> ('Bddapron.Expr1.Bool.t * int) list
          val print :
            'Bddapron.Cond.t ->
            Format.formatter -> 'Bddapron.Expr1.Bint.t -> unit
        end
      module Benum :
        sig
          type 'a t =
              ('Bddapron.Env.t, Cudd.Man.v Bdd.Enum.t) Bddapron.Env.value
          val of_expr0 :
            'Bddapron.Env.t ->
            'Bddapron.Expr0.Benum.t -> 'Bddapron.Expr1.Benum.t
          val get_env : 'Bddapron.Expr1.Benum.t -> 'Bddapron.Env.t
          val to_expr0 :
            'Bddapron.Expr1.Benum.t -> 'Bddapron.Expr0.Benum.t
          val of_expr : 'Bddapron.Expr1.expr -> 'Bddapron.Expr1.Benum.t
          val to_expr : 'Bddapron.Expr1.Benum.t -> 'Bddapron.Expr1.expr
          val extend_environment :
            'Bddapron.Expr1.Benum.t ->
            'Bddapron.Env.t -> 'Bddapron.Expr1.Benum.t
          val var :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t -> '-> 'Bddapron.Expr1.Benum.t
          val ite :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bool.t ->
            'Bddapron.Expr1.Benum.t ->
            'Bddapron.Expr1.Benum.t -> 'Bddapron.Expr1.Benum.t
          val eq :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Benum.t ->
            'Bddapron.Expr1.Benum.t -> 'Bddapron.Expr1.Bool.t
          val eq_label :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Benum.t -> '-> 'Bddapron.Expr1.Bool.t
          val cofactor :
            'Bddapron.Expr1.Benum.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Benum.t
          val restrict :
            'Bddapron.Expr1.Benum.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Benum.t
          val tdrestrict :
            'Bddapron.Expr1.Benum.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Benum.t
          val substitute_by_var :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Benum.t ->
            ('a * 'a) list -> 'Bddapron.Expr1.Benum.t
          val substitute :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Benum.t ->
            ('a * 'Bddapron.Expr1.expr) list -> 'Bddapron.Expr1.Benum.t
          val guard_of_label :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Benum.t -> '-> 'Bddapron.Expr1.Bool.t
          val guardlabels :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Benum.t -> ('Bddapron.Expr1.Bool.t * 'a) list
          val print :
            'Bddapron.Cond.t ->
            Format.formatter -> 'Bddapron.Expr1.Benum.t -> unit
        end
      type apron_coeff = Apron.Coeff.t
      type apron_typ = Apron.Texpr1.typ
      type apron_round = Apron.Texpr1.round
      type apron_cons_typ = Apron.Tcons1.typ
      module Apron :
        sig
          type 'a t =
              ('Bddapron.Env.t, 'Bddapron.Expr0.Apron.t)
              Bddapron.Env.value
          val of_expr0 :
            'Bddapron.Env.t ->
            'Bddapron.Expr0.Apron.t -> 'Bddapron.Expr1.Apron.t
          val get_env : 'Bddapron.Expr1.Apron.t -> 'Bddapron.Env.t
          val to_expr0 :
            'Bddapron.Expr1.Apron.t -> 'Bddapron.Expr0.Apron.t
          val of_expr : 'Bddapron.Expr1.expr -> 'Bddapron.Expr1.Apron.t
          val to_expr : 'Bddapron.Expr1.Apron.t -> 'Bddapron.Expr1.expr
          val extend_environment :
            'Bddapron.Expr1.Apron.t ->
            'Bddapron.Env.t -> 'Bddapron.Expr1.Apron.t
          val var :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t -> '-> 'Bddapron.Expr1.Apron.t
          val cst :
            'Bddapron.Env.t ->
            'Bddapron.Cond.t -> Apron.Coeff.t -> 'Bddapron.Expr1.Apron.t
          val add :
            'Bddapron.Cond.t ->
            ?typ:Apron.Texpr1.typ ->
            ?round:Apron.Texpr1.round ->
            'Bddapron.Expr1.Apron.t ->
            'Bddapron.Expr1.Apron.t -> 'Bddapron.Expr1.Apron.t
          val mul :
            'Bddapron.Cond.t ->
            ?typ:Apron.Texpr1.typ ->
            ?round:Apron.Texpr1.round ->
            'Bddapron.Expr1.Apron.t ->
            'Bddapron.Expr1.Apron.t -> 'Bddapron.Expr1.Apron.t
          val sub :
            'Bddapron.Cond.t ->
            ?typ:Apron.Texpr1.typ ->
            ?round:Apron.Texpr1.round ->
            'Bddapron.Expr1.Apron.t ->
            'Bddapron.Expr1.Apron.t -> 'Bddapron.Expr1.Apron.t
          val div :
            'Bddapron.Cond.t ->
            ?typ:Apron.Texpr1.typ ->
            ?round:Apron.Texpr1.round ->
            'Bddapron.Expr1.Apron.t ->
            'Bddapron.Expr1.Apron.t -> 'Bddapron.Expr1.Apron.t
          val gmod :
            'Bddapron.Cond.t ->
            ?typ:Apron.Texpr1.typ ->
            ?round:Apron.Texpr1.round ->
            'Bddapron.Expr1.Apron.t ->
            'Bddapron.Expr1.Apron.t -> 'Bddapron.Expr1.Apron.t
          val negate :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Apron.t -> 'Bddapron.Expr1.Apron.t
          val sqrt :
            'Bddapron.Cond.t ->
            ?typ:Apron.Texpr1.typ ->
            ?round:Apron.Texpr1.round ->
            'Bddapron.Expr1.Apron.t -> 'Bddapron.Expr1.Apron.t
          val cast :
            'Bddapron.Cond.t ->
            ?typ:Apron.Texpr1.typ ->
            ?round:Apron.Texpr1.round ->
            'Bddapron.Expr1.Apron.t -> 'Bddapron.Expr1.Apron.t
          val ite :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Bool.t ->
            'Bddapron.Expr1.Apron.t ->
            'Bddapron.Expr1.Apron.t -> 'Bddapron.Expr1.Apron.t
          val condition :
            'Bddapron.Cond.t ->
            Apron.Tcons1.typ ->
            'Bddapron.Expr1.Apron.t -> 'Bddapron.Expr1.Bool.t
          val supeq :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Apron.t -> 'Bddapron.Expr1.Bool.t
          val sup :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Apron.t -> 'Bddapron.Expr1.Bool.t
          val eq :
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Apron.t -> 'Bddapron.Expr1.Bool.t
          val cofactor :
            'Bddapron.Expr1.Apron.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Apron.t
          val restrict :
            'Bddapron.Expr1.Apron.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Apron.t
          val tdrestrict :
            'Bddapron.Expr1.Apron.t ->
            'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.Apron.t
          val substitute_by_var :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Apron.t ->
            ('a * 'a) list -> 'Bddapron.Expr1.Apron.t
          val substitute :
            ?memo:Cudd.Memo.t ->
            'Bddapron.Cond.t ->
            'Bddapron.Expr1.Apron.t ->
            ('a * 'Bddapron.Expr1.expr) list -> 'Bddapron.Expr1.Apron.t
          val print :
            'Bddapron.Cond.t ->
            Format.formatter -> 'Bddapron.Expr1.Apron.t -> unit
        end
      val typ_of_expr : 'Bddapron.Expr1.t -> 'Bddapron.Env.typ
      val make :
        'Bddapron.Env.t -> 'Bddapron.Expr0.t -> 'Bddapron.Expr1.t
      val of_expr0 :
        'Bddapron.Env.t -> 'Bddapron.Expr0.t -> 'Bddapron.Expr1.t
      val get_env : 'Bddapron.Expr1.t -> 'Bddapron.Env.t
      val to_expr0 : 'Bddapron.Expr1.t -> 'Bddapron.Expr0.t
      val extend_environment :
        'Bddapron.Expr1.t -> 'Bddapron.Env.t -> 'Bddapron.Expr1.t
      val var :
        'Bddapron.Env.t -> 'Bddapron.Cond.t -> '-> 'Bddapron.Expr1.t
      val ite :
        'Bddapron.Cond.t ->
        'Bddapron.Expr1.Bool.t ->
        'Bddapron.Expr1.t -> 'Bddapron.Expr1.t -> 'Bddapron.Expr1.t
      val eq :
        'Bddapron.Cond.t ->
        'Bddapron.Expr1.t ->
        'Bddapron.Expr1.t -> 'Bddapron.Expr1.Bool.t
      val substitute_by_var :
        ?memo:Cudd.Memo.t ->
        'Bddapron.Cond.t ->
        'Bddapron.Expr1.t -> ('a * 'a) list -> 'Bddapron.Expr1.t
      val substitute_by_var_list :
        ?memo:Cudd.Memo.t ->
        'Bddapron.Cond.t ->
        'Bddapron.Expr1.t list ->
        ('a * 'a) list -> 'Bddapron.Expr1.t list
      val substitute :
        ?memo:Cudd.Memo.t ->
        'Bddapron.Cond.t ->
        'Bddapron.Expr1.t ->
        ('a * 'Bddapron.Expr1.t) list -> 'Bddapron.Expr1.t
      val substitute_list :
        ?memo:Cudd.Memo.t ->
        'Bddapron.Cond.t ->
        'Bddapron.Expr1.t list ->
        ('a * 'Bddapron.Expr1.t) list -> 'Bddapron.Expr1.t list
      val support : 'Bddapron.Cond.t -> 'Bddapron.Expr1.t -> 'PSette.t
      val support_cond : Cudd.Man.vt -> 'Bddapron.Expr1.t -> Cudd.Bdd.vt
      val cofactor :
        'Bddapron.Expr1.t ->
        'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.t
      val restrict :
        'Bddapron.Expr1.t ->
        'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.t
      val tdrestrict :
        'Bddapron.Expr1.t ->
        'Bddapron.Expr1.Bool.t -> 'Bddapron.Expr1.t
      val print :
        'Bddapron.Cond.t -> Format.formatter -> 'Bddapron.Expr1.t -> unit
      val normalize :
        ?reduce:bool ->
        ?careset:bool ->
        'Bddapron.Cond.t * 'Bddapron.Expr1.t list ->
        'Bddapron.Cond.t * 'Bddapron.Expr1.t list
      module List :
        sig
          type 'a t =
              ('Bddapron.Env.t, 'Bddapron.Expr0.t list)
              Bddapron.Env.value
          val of_lexpr0 :
            'Bddapron.Env.t ->
            'Bddapron.Expr0.t list -> 'Bddapron.Expr1.List.t
          val get_env : 'Bddapron.Expr1.List.t -> 'Bddapron.Env.t
          val to_lexpr0 :
            'Bddapron.Expr1.List.t -> 'Bddapron.Expr0.t list
          val of_lexpr :
            'Bddapron.Env.t ->
            'Bddapron.Expr1.expr list -> 'Bddapron.Expr1.List.t
          val to_lexpr :
            'Bddapron.Expr1.List.t -> 'Bddapron.Expr1.expr list
          val extend_environment :
            'Bddapron.Expr1.List.t ->
            'Bddapron.Env.t -> 'Bddapron.Expr1.List.t
          val normalize :
            ?reduce:bool ->
            ?careset:bool ->
            'Bddapron.Cond.t * 'Bddapron.Expr1.List.t ->
            'Bddapron.Cond.t * 'Bddapron.Expr1.List.t
          val print :
            ?first:(unit, Format.formatter, unit) Pervasives.format ->
            ?sep:(unit, Format.formatter, unit) Pervasives.format ->
            ?last:(unit, Format.formatter, unit) Pervasives.format ->
            'Bddapron.Cond.t ->
            Format.formatter -> 'Bddapron.Expr1.List.t -> unit
        end
      module O :
        sig
          type ('a, 'b) t = ('b, 'Bddapron.Expr0.t) Bddapron.Env.value
            constraint 'b =
              ('a, [> 'Bddapron.Env.typ ] as 'c,
               [> 'Bddapron.Env.typdef ] as 'd, 'e)
              Bddapron.Env.O.t
          type ('a, 'b) expr = ('a, 'b) Bddapron.Expr1.O.t
            constraint 'b =
              ('a, [> 'Bddapron.Env.typ ] as 'c,
               [> 'Bddapron.Env.typdef ] as 'd, 'e)
              Bddapron.Env.O.t
          module Bool :
            sig
              type ('a, 'b) t =
                  ('b, 'Bddapron.Expr0.Bool.t) Bddapron.Env.value
                constraint 'b =
                  ('a, [> 'Bddapron.Env.typ ] as 'c,
                   [> 'Bddapron.Env.typdef ] as 'd, 'e)
                  Bddapron.Env.O.t
              val of_expr :
                (('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t, [> `Bool of 'Bddapron.Expr0.Bool.t ])
                Bddapron.Env.value ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val to_expr :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                (('a, 'b, 'c, 'd) Bddapron.Env.O.t,
                 [> `Bool of 'Bddapron.Expr0.Bool.t ])
                Bddapron.Env.value
              val extend_environment :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, 'b, 'c, 'd) Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val dtrue :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val dfalse :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val of_bool :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                bool ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val var :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                '->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val dnot :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val dand :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val dor :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val xor :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val nand :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val nor :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val nxor :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val eq :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val leq :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val ite :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val is_true :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t -> bool
              val is_false :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t -> bool
              val is_cst :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t -> bool
              val is_eq :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t -> bool
              val is_leq :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t -> bool
              val is_inter_false :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t -> bool
              val exist :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                'a list ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val forall :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                'a list ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val cofactor :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val restrict :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val tdrestrict :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val substitute_by_var :
                ?memo:Cudd.Memo.t ->
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a * 'a) list ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val substitute :
                ?memo:Cudd.Memo.t ->
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a *
                 ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                 Bddapron.Expr1.O.expr)
                list ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val print :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                Format.formatter ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t -> unit
            end
          module Bint :
            sig
              type ('a, 'b) t = ('b, Cudd.Man.v Bdd.Int.t) Bddapron.Env.value
                constraint 'b =
                  ('a, [> 'Bddapron.Env.typ ] as 'c,
                   [> 'Bddapron.Env.typdef ] as 'd, 'e)
                  Bddapron.Env.O.t
              val of_expr :
                (('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t, [> `Bint of 'Bddapron.Expr0.Bint.t ])
                Bddapron.Env.value ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t
              val to_expr :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                (('a, 'b, 'c, 'd) Bddapron.Env.O.t,
                 [> `Bint of 'Bddapron.Expr0.Bint.t ])
                Bddapron.Env.value
              val extend_environment :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, 'b, 'c, 'd) Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t
              val of_int :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                [ `Bint of bool * int ] ->
                int ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t
              val var :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                '->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t
              val neg :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t
              val succ :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t
              val pred :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t
              val add :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t
              val sub :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t
              val mul :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t
              val shift_left :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                int ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t
              val shift_right :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                int ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t
              val scale :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                int ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t
              val ite :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t
              val zero :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val eq :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val supeq :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val sup :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val eq_int :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                int ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val supeq_int :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                int ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val sup_int :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                int ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val cofactor :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t
              val restrict :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t
              val tdrestrict :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t
              val substitute_by_var :
                ?memo:Cudd.Memo.t ->
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a * 'a) list ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t
              val substitute :
                ?memo:Cudd.Memo.t ->
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                ('a *
                 ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                 Bddapron.Expr1.O.expr)
                list ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t
              val guard_of_int :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                int ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val guardints :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t ->
                (('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                 Bddapron.Expr1.O.Bool.t * int)
                list
              val print :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                Format.formatter ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bint.t -> unit
            end
          module Benum :
            sig
              type ('a, 'b) t =
                  ('b, Cudd.Man.v Bdd.Enum.t) Bddapron.Env.value
                constraint 'b =
                  ('a, [> 'Bddapron.Env.typ ] as 'c,
                   [> 'Bddapron.Env.typdef ] as 'd, 'e)
                  Bddapron.Env.O.t
              val of_expr :
                (('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t, [> `Benum of 'Bddapron.Expr0.Benum.t ])
                Bddapron.Env.value ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t
              val to_expr :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t ->
                (('a, 'b, 'c, 'd) Bddapron.Env.O.t,
                 [> `Benum of 'Bddapron.Expr0.Benum.t ])
                Bddapron.Env.value
              val extend_environment :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t ->
                ('a, 'b, 'c, 'd) Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t
              val var :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                '->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t
              val ite :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t
              val eq :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val eq_label :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t ->
                '->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val cofactor :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t
              val restrict :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t
              val tdrestrict :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t
              val substitute_by_var :
                ?memo:Cudd.Memo.t ->
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t ->
                ('a * 'a) list ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t
              val substitute :
                ?memo:Cudd.Memo.t ->
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t ->
                ('a *
                 ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                 Bddapron.Expr1.O.expr)
                list ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t
              val guard_of_label :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t ->
                '->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Bool.t
              val guardlabels :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t ->
                (('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                 Bddapron.Expr1.O.Bool.t * 'a)
                list
              val print :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                Format.formatter ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Benum.t -> unit
            end
          module Apron :
            sig
              type ('a, 'b) t =
                  ('b, 'Bddapron.Expr0.Apron.t) Bddapron.Env.value
                constraint 'b =
                  ('a, [> 'Bddapron.Env.typ ] as 'c,
                   [> 'Bddapron.Env.typdef ] as 'd, 'e)
                  Bddapron.Env.O.t
              val of_expr :
                (('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t, [> `Apron of 'Bddapron.Expr0.Apron.t ])
                Bddapron.Env.value ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Apron.t
              val to_expr :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Expr1.O.Apron.t ->
                (('a, 'b, 'c, 'd) Bddapron.Env.O.t,
                 [> `Apron of 'Bddapron.Expr0.Apron.t ])
                Bddapron.Env.value
              val extend_environment :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Expr1.O.Apron.t ->
                ('a, 'b, 'c, 'd) Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Apron.t
              val var :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                '->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Apron.t
              val cst :
                ('a, [> 'Bddapron.Env.typ ] as 'b,
                 [> 'Bddapron.Env.typdef ] as 'c, 'd)
                Bddapron.Env.O.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
                Bddapron.Expr1.apron_coeff ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Apron.t
              val add :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ?typ:Bddapron.Expr1.apron_typ ->
                ?round:Bddapron.Expr1.apron_round ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Apron.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Apron.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Apron.t
              val mul :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ?typ:Bddapron.Expr1.apron_typ ->
                ?round:Bddapron.Expr1.apron_round ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Apron.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Apron.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Apron.t
              val sub :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ?typ:Bddapron.Expr1.apron_typ ->
                ?round:Bddapron.Expr1.apron_round ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Apron.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Apron.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Apron.t
              val div :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.Env.O.t)
                Bddapron.Cond.O.t ->
                ?typ:Bddapron.Expr1.apron_typ ->
                ?round:Bddapron.Expr1.apron_round ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Apron.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Apron.t ->
                ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t)
                Bddapron.Expr1.O.Apron.t
              val gmod :
                ('a,
                 ('a, [> 'Bddapron.Env.typ ] as 'b,
                  [> 'Bddapron.Env.typdef ] as 'c, 'd)
                 Bddapron.