sig
  type 'a t = 'a Bdd.Expr0.Bool.t
  type dt = Cudd.Man.d Bdd.Domain0.t
  type vt = Cudd.Man.v Bdd.Domain0.t
  val size : 'a Bdd.Domain0.t -> int
  val print :
    ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
    ('a, 'b) Bdd.Env.t -> Format.formatter -> 'b Bdd.Domain0.t -> unit
  val bottom : ('a, 'b) Bdd.Env.t -> 'b Bdd.Domain0.t
  val top : ('a, 'b) Bdd.Env.t -> 'b Bdd.Domain0.t
  val is_bottom : ('a, 'b) Bdd.Env.t -> 'b Bdd.Domain0.t -> bool
  val is_top : ('a, 'b) Bdd.Env.t -> 'b Bdd.Domain0.t -> bool
  val is_leq :
    ('a, 'b) Bdd.Env.t -> 'b Bdd.Domain0.t -> 'b Bdd.Domain0.t -> bool
  val is_eq :
    ('a, 'b) Bdd.Env.t -> 'b Bdd.Domain0.t -> 'b Bdd.Domain0.t -> bool
  val is_variable_unconstrained :
    ('a, 'b) Bdd.Env.t -> 'b Bdd.Domain0.t -> 'a -> bool
  val meet :
    ('a, 'b) Bdd.Env.t ->
    'b Bdd.Domain0.t -> 'b Bdd.Domain0.t -> 'b Bdd.Domain0.t
  val join :
    ('a, 'b) Bdd.Env.t ->
    'b Bdd.Domain0.t -> 'b Bdd.Domain0.t -> 'b Bdd.Domain0.t
  val meet_condition :
    ('a, 'b) Bdd.Env.t ->
    'b Bdd.Domain0.t -> 'b Bdd.Expr0.Bool.t -> 'b Bdd.Domain0.t
  val assign_lexpr :
    ?relational:bool ->
    ?nodependency:bool ->
    ('a, 'b) Bdd.Env.t ->
    'b Bdd.Domain0.t -> 'a list -> 'b Bdd.Expr0.expr list -> 'b Bdd.Domain0.t
  val substitute_lexpr :
    ('a, 'b) Bdd.Env.t ->
    'b Bdd.Domain0.t -> 'a list -> 'b Bdd.Expr0.expr list -> 'b Bdd.Domain0.t
  val forget_list :
    ('a, 'b) Bdd.Env.t -> 'b Bdd.Domain0.t -> 'a list -> 'b Bdd.Domain0.t
  module O :
    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
end