sig
  val check_value :
    ('a -> int array -> 'a) ->
    (('b, [> 'b Bdd.Env.typ ] as 'c, [> 'b Bdd.Env.typdef ] as 'd, 'e, 'f)
     Bdd.Env.O.t, 'a)
    Bdd.Env.value -> ('b, 'c, 'd, 'e, 'f) Bdd.Env.O.t -> 'a
  val check_lvalue :
    ('a -> int array -> 'a) ->
    (('b, [> 'b Bdd.Env.typ ] as 'c, [> 'b Bdd.Env.typdef ] as 'd, 'e, 'f)
     Bdd.Env.O.t, 'a)
    Bdd.Env.value list -> ('b, 'c, 'd, 'e, 'f) Bdd.Env.O.t -> 'a list
  type ('a, 'b, 'c) t = ('a, 'b, 'c) Bdd.Expr1.O.Bool.t
    constraint 'b =
      ('a, [> 'a Bdd.Env.typ ] as 'd, [> 'a Bdd.Env.typdef ] as 'e, 'c, 'f)
      Bdd.Env.O.t
  type ('a, 'b) dt = ('a, 'b, Cudd.Man.d) Bdd.Domain1.O.t
    constraint 'b =
      ('a, [> 'a Bdd.Env.typ ] as 'c, [> 'a Bdd.Env.typdef ] as 'd,
       Cudd.Man.d, 'e)
      Bdd.Env.O.t
  type ('a, 'b) vt = ('a, 'b, Cudd.Man.v) Bdd.Domain1.O.t
    constraint 'b =
      ('a, [> 'a Bdd.Env.typ ] as 'c, [> 'a Bdd.Env.typdef ] as 'd,
       Cudd.Man.v, 'e)
      Bdd.Env.O.t
  val of_domain0 :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
    Bdd.Env.O.t ->
    'c Bdd.Domain0.t ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
  val get_env :
    ('a,
     ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
     Bdd.Env.O.t, 'c)
    Bdd.Domain1.O.t -> ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t
  val to_domain0 :
    ('a,
     ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b) Bdd.Env.O.t,
     'c)
    Bdd.Domain1.O.t -> 'c Bdd.Domain0.t
  val of_expr1 :
    ('a,
     ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
     Bdd.Env.O.t, 'c)
    Bdd.Expr1.O.Bool.t ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
  val to_expr1 :
    ('a,
     ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
     Bdd.Env.O.t, 'c)
    Bdd.Domain1.O.t ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
  val size :
    ('a,
     ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b) Bdd.Env.O.t,
     'c)
    Bdd.Domain1.O.t -> int
  val print :
    Format.formatter ->
    ('a,
     ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b) Bdd.Env.O.t,
     'c)
    Bdd.Domain1.O.t -> unit
  val bottom :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
    Bdd.Env.O.t -> ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
  val top :
    ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
    Bdd.Env.O.t -> ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
  val is_bottom :
    ('a,
     ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b) Bdd.Env.O.t,
     'c)
    Bdd.Domain1.O.t -> bool
  val is_top :
    ('a,
     ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b) Bdd.Env.O.t,
     'c)
    Bdd.Domain1.O.t -> bool
  val is_leq :
    ('a,
     ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
     Bdd.Env.O.t, 'c)
    Bdd.Domain1.O.t ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t -> bool
  val is_eq :
    ('a,
     ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
     Bdd.Env.O.t, 'c)
    Bdd.Domain1.O.t ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t -> bool
  val is_variable_unconstrained :
    ('a,
     ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'c, 'b) Bdd.Env.O.t,
     'c)
    Bdd.Domain1.O.t -> 'a -> bool
  val meet :
    ('a,
     ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
     Bdd.Env.O.t, 'c)
    Bdd.Domain1.O.t ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
  val join :
    ('a,
     ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
     Bdd.Env.O.t, 'c)
    Bdd.Domain1.O.t ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
  val meet_condition :
    ('a,
     ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
     Bdd.Env.O.t, 'c)
    Bdd.Domain1.O.t ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
  val assign_lexpr :
    ?relational:bool ->
    ?nodependency:bool ->
    ('a,
     ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
     Bdd.Env.O.t, 'c)
    Bdd.Domain1.O.t ->
    'a list ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t list ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
  val assign_listexpr :
    ?relational:bool ->
    ?nodependency:bool ->
    ('a,
     ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
     Bdd.Env.O.t, 'c)
    Bdd.Domain1.O.t ->
    'a list ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.List.t ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
  val substitute_lexpr :
    ('a,
     ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
     Bdd.Env.O.t, 'c)
    Bdd.Domain1.O.t ->
    'a list ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t list ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
  val substitute_listexpr :
    ('a,
     ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
     Bdd.Env.O.t, 'c)
    Bdd.Domain1.O.t ->
    'a list ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.List.t ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
  val forget_list :
    ('a,
     ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
     Bdd.Env.O.t, 'c)
    Bdd.Domain1.O.t ->
    'a list -> ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
  val change_environment :
    ('a,
     ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
     Bdd.Env.O.t, 'c)
    Bdd.Domain1.O.t ->
    ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
  val rename :
    ('a,
     ('a, [> 'a Bdd.Env.typ ] as 'b, [> 'a Bdd.Env.typdef ] as 'd, 'c, 'e)
     Bdd.Env.O.t, 'c)
    Bdd.Domain1.O.t ->
    ('a * 'a) list ->
    ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
end