sig
  val print :
    ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    Format.formatter -> 'd Bdd.Domain0.t -> unit
  val bottom :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Bdd.Domain0.t
  val top :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Bdd.Domain0.t
  val is_bottom :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Bdd.Domain0.t -> bool
  val is_top :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Bdd.Domain0.t -> bool
  val is_leq :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Bdd.Domain0.t -> 'd Bdd.Domain0.t -> bool
  val is_eq :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Bdd.Domain0.t -> 'd Bdd.Domain0.t -> bool
  val is_variable_unconstrained :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Bdd.Domain0.t -> 'a -> bool
  val meet :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Bdd.Domain0.t -> 'd Bdd.Domain0.t -> 'd Bdd.Domain0.t
  val join :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Bdd.Domain0.t -> 'd Bdd.Domain0.t -> 'd Bdd.Domain0.t
  val meet_condition :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Bdd.Domain0.t -> 'd Bdd.Expr0.Bool.t -> 'd Bdd.Domain0.t
  val assign_lexpr :
    ?relational:bool ->
    ?nodependency:bool ->
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Bdd.Domain0.t -> 'a list -> 'd Bdd.Expr0.expr list -> 'd Bdd.Domain0.t
  val substitute_lexpr :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Bdd.Domain0.t -> 'a list -> 'd Bdd.Expr0.expr list -> 'd Bdd.Domain0.t
  val forget_list :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Bdd.Domain0.t -> 'a list -> 'd Bdd.Domain0.t
  module Asssub :
    sig
      val sort :
        int array -> 'a Cudd.Bdd.t array -> int array * 'a Cudd.Bdd.t array
      val is_equal : 'a Cudd.Bdd.t array -> 'a Cudd.Bdd.t array -> bool
      val post :
        'a Cudd.Bdd.t -> int array -> 'a Cudd.Bdd.t array -> 'a Cudd.Bdd.t
      val postcondition :
        'a Cudd.Bdd.t -> 'a Cudd.Bdd.t array -> 'a Cudd.Bdd.t
    end
  val relation_supp_compose_of_lvarlexpr :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'a list ->
    'd Bdd.Expr0.expr list ->
    'd Cudd.Bdd.t * 'd Cudd.Bdd.t * 'd Cudd.Bdd.t array
  val apply_change :
    'a Bdd.Domain0.t -> 'a Bdd.Env.change -> 'a Bdd.Domain0.t
end