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