sig
  type ('a, 'b) t = ('a, 'b) Bdd.Expr1.Bool.t
  type 'a dt = ('a, Cudd.Man.d) Bdd.Domain1.t
  type 'a vt = ('a, Cudd.Man.v) Bdd.Domain1.t
  val of_domain0 :
    ('a, 'b) Bdd.Env.t -> 'b Bdd.Domain0.t -> ('a, 'b) Bdd.Domain1.t
  val get_env : ('a, 'b) Bdd.Domain1.t -> ('a, 'b) Bdd.Env.t
  val to_domain0 : ('a, 'b) Bdd.Domain1.t -> 'b Bdd.Domain0.t
  val of_expr1 : ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Domain1.t
  val to_expr1 : ('a, 'b) Bdd.Domain1.t -> ('a, 'b) Bdd.Expr1.Bool.t
  val size : ('a, 'b) Bdd.Domain1.t -> int
  val print : Format.formatter -> ('a, 'b) Bdd.Domain1.t -> unit
  val bottom : ('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Domain1.t
  val top : ('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Domain1.t
  val is_bottom : ('a, 'b) Bdd.Domain1.t -> bool
  val is_top : ('a, 'b) Bdd.Domain1.t -> bool
  val is_leq : ('a, 'b) Bdd.Domain1.t -> ('a, 'b) Bdd.Domain1.t -> bool
  val is_eq : ('a, 'b) Bdd.Domain1.t -> ('a, 'b) Bdd.Domain1.t -> bool
  val is_variable_unconstrained : ('a, 'b) Bdd.Domain1.t -> 'a -> bool
  val meet :
    ('a, 'b) Bdd.Domain1.t ->
    ('a, 'b) Bdd.Domain1.t -> ('a, 'b) Bdd.Domain1.t
  val join :
    ('a, 'b) Bdd.Domain1.t ->
    ('a, 'b) Bdd.Domain1.t -> ('a, 'b) Bdd.Domain1.t
  val meet_condition :
    ('a, 'b) Bdd.Domain1.t ->
    ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Domain1.t
  val assign_lexpr :
    ?relational:bool ->
    ?nodependency:bool ->
    ('a, 'b) Bdd.Domain1.t ->
    'a list -> ('a, 'b) Bdd.Expr1.t list -> ('a, 'b) Bdd.Domain1.t
  val assign_listexpr :
    ?relational:bool ->
    ?nodependency:bool ->
    ('a, 'b) Bdd.Domain1.t ->
    'a list -> ('a, 'b) Bdd.Expr1.List.t -> ('a, 'b) Bdd.Domain1.t
  val substitute_lexpr :
    ('a, 'b) Bdd.Domain1.t ->
    'a list -> ('a, 'b) Bdd.Expr1.t list -> ('a, 'b) Bdd.Domain1.t
  val substitute_listexpr :
    ('a, 'b) Bdd.Domain1.t ->
    'a list -> ('a, 'b) Bdd.Expr1.List.t -> ('a, 'b) Bdd.Domain1.t
  val forget_list :
    ('a, 'b) Bdd.Domain1.t -> 'a list -> ('a, 'b) Bdd.Domain1.t
  val change_environment :
    ('a, 'b) Bdd.Domain1.t -> ('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Domain1.t
  val rename :
    ('a, 'b) Bdd.Domain1.t -> ('a * 'a) list -> ('a, 'b) Bdd.Domain1.t
  module O :
    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
end