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