sig
  val tid_of_var :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'a -> int array
  val reg_of_expr : 'd Bdd.Expr0.expr -> 'd Cudd.Bdd.t array
  module Bool :
    sig
      type 'd t = 'd Cudd.Bdd.t
      type dt = Cudd.Man.d Bdd.Expr0.O.Bool.t
      type vt = Cudd.Man.v Bdd.Expr0.O.Bool.t
      val of_expr :
        [> `Bool of 'd Bdd.Expr0.O.Bool.t ] -> 'd Bdd.Expr0.O.Bool.t
      val to_expr :
        'd Bdd.Expr0.O.Bool.t -> [> `Bool of 'd Bdd.Expr0.O.Bool.t ]
      val dtrue :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t
      val dfalse :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t
      val of_bool :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        bool -> 'd Bdd.Expr0.O.Bool.t
      val var :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'a -> 'd Bdd.Expr0.O.Bool.t
      val dnot :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
      val dand :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
      val dor :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
      val xor :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
      val nand :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
      val nor :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
      val nxor :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
      val leq :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
      val eq :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
      val ite :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t ->
        'd Bdd.Expr0.O.Bool.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
      val is_true :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t -> bool
      val is_false :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t -> bool
      val is_cst :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t -> bool
      val is_eq :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t -> bool
      val is_leq :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t -> bool
      val is_and_false :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t -> bool
      val exist :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'a list -> 'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
      val forall :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'a list -> 'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
      val cofactor :
        'd Bdd.Expr0.O.Bool.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
      val restrict :
        'd Bdd.Expr0.O.Bool.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
      val tdrestrict :
        'd Bdd.Expr0.O.Bool.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bool.t
      val permute :
        ?memo:Cudd.Memo.t ->
        'd Bdd.Expr0.O.Bool.t -> int array -> 'd Bdd.Expr0.O.Bool.t
      val varmap : 'a Bdd.Expr0.O.Bool.t -> 'a Bdd.Expr0.O.Bool.t
      val substitute_by_var :
        ?memo:Cudd.Memo.t ->
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t -> ('a * 'a) list -> 'd Bdd.Expr0.O.Bool.t
      val substitute :
        ?memo:Cudd.Memo.t ->
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t ->
        ('a * 'd Bdd.Expr0.expr) list -> 'd Bdd.Expr0.O.Bool.t
      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.Expr0.O.Bool.t -> unit
    end
  module Bint :
    sig
      type 'd t = 'd Bdd.Int.t
      type dt = Cudd.Man.d Bdd.Expr0.O.Bint.t
      type vt = Cudd.Man.v Bdd.Expr0.O.Bint.t
      val of_expr :
        [> `Bint of 'd Bdd.Expr0.O.Bint.t ] -> 'd Bdd.Expr0.O.Bint.t
      val to_expr :
        'd Bdd.Expr0.O.Bint.t -> [> `Bint of 'd Bdd.Expr0.O.Bint.t ]
      val of_int :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        [> `Bint of bool * int ] -> int -> 'd Bdd.Expr0.O.Bint.t
      val var :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'a -> 'd Bdd.Expr0.O.Bint.t
      val ite :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t ->
        'd Bdd.Expr0.O.Bint.t ->
        'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bint.t
      val neg :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bint.t
      val succ :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bint.t
      val pred :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bint.t
      val add :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bint.t ->
        'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bint.t
      val sub :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bint.t ->
        'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bint.t
      val mul :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bint.t ->
        'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bint.t
      val shift_left :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        int -> 'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bint.t
      val shift_right :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        int -> 'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bint.t
      val scale :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        int -> 'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bint.t
      val zero :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bool.t
      val eq :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bint.t ->
        'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bool.t
      val eq_int :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bint.t -> int -> 'd Bdd.Expr0.O.Bool.t
      val supeq :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bint.t ->
        'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bool.t
      val supeq_int :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bint.t -> int -> 'd Bdd.Expr0.O.Bool.t
      val sup :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bint.t ->
        'd Bdd.Expr0.O.Bint.t -> 'd Bdd.Expr0.O.Bool.t
      val sup_int :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bint.t -> int -> 'd Bdd.Expr0.O.Bool.t
      val cofactor :
        'd Bdd.Expr0.O.Bint.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bint.t
      val restrict :
        'd Bdd.Expr0.O.Bint.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bint.t
      val tdrestrict :
        'd Bdd.Expr0.O.Bint.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Bint.t
      val permute :
        ?memo:Cudd.Memo.t ->
        'd Bdd.Expr0.O.Bint.t -> int array -> 'd Bdd.Expr0.O.Bint.t
      val varmap : 'a Bdd.Expr0.O.Bint.t -> 'a Bdd.Expr0.O.Bint.t
      val substitute_by_var :
        ?memo:Cudd.Memo.t ->
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bint.t -> ('a * 'a) list -> 'd Bdd.Expr0.O.Bint.t
      val substitute :
        ?memo:Cudd.Memo.t ->
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bint.t ->
        ('a * 'd Bdd.Expr0.expr) list -> 'd Bdd.Expr0.O.Bint.t
      val guard_of_int :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bint.t -> int -> 'd Bdd.Expr0.O.Bool.t
      val guardints :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bint.t -> ('d Bdd.Expr0.O.Bool.t * int) list
      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.Expr0.O.Bint.t -> unit
    end
  module Benum :
    sig
      type 'd t = 'd Bdd.Enum.t
      type dt = Cudd.Man.d Bdd.Expr0.O.Benum.t
      type vt = Cudd.Man.v Bdd.Expr0.O.Benum.t
      val of_expr :
        [> `Benum of 'd Bdd.Expr0.O.Benum.t ] -> 'd Bdd.Expr0.O.Benum.t
      val to_expr :
        'd Bdd.Expr0.O.Benum.t -> [> `Benum of 'd Bdd.Expr0.O.Benum.t ]
      val var :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'a -> 'd Bdd.Expr0.O.Benum.t
      val ite :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Bool.t ->
        'd Bdd.Expr0.O.Benum.t ->
        'd Bdd.Expr0.O.Benum.t -> 'd Bdd.Expr0.O.Benum.t
      val eq :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Benum.t ->
        'd Bdd.Expr0.O.Benum.t -> 'd Bdd.Expr0.O.Bool.t
      val eq_label :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Benum.t -> 'a -> 'd Bdd.Expr0.O.Bool.t
      val cofactor :
        'd Bdd.Expr0.O.Benum.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Benum.t
      val restrict :
        'd Bdd.Expr0.O.Benum.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Benum.t
      val tdrestrict :
        'd Bdd.Expr0.O.Benum.t ->
        'd Bdd.Expr0.O.Bool.t -> 'd Bdd.Expr0.O.Benum.t
      val permute :
        ?memo:Cudd.Memo.t ->
        'd Bdd.Expr0.O.Benum.t -> int array -> 'd Bdd.Expr0.O.Benum.t
      val varmap : 'a Bdd.Expr0.O.Benum.t -> 'a Bdd.Expr0.O.Benum.t
      val substitute_by_var :
        ?memo:Cudd.Memo.t ->
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Benum.t -> ('a * 'a) list -> 'd Bdd.Expr0.O.Benum.t
      val substitute :
        ?memo:Cudd.Memo.t ->
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Benum.t ->
        ('a * 'd Bdd.Expr0.expr) list -> 'd Bdd.Expr0.O.Benum.t
      val guard_of_label :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Benum.t -> 'a -> 'd Bdd.Expr0.O.Bool.t
      val guardlabels :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Bdd.Expr0.O.Benum.t -> ('d Bdd.Expr0.O.Bool.t * 'a) list
      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.Expr0.O.Benum.t -> unit
    end
  val typ_of_expr :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Bdd.Expr0.t -> [> 'a Bdd.Env.typ ]
  val var :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'a -> 'd Bdd.Expr0.t
  val ite :
    'd Bdd.Expr0.O.Bool.t ->
    'd Bdd.Expr0.t -> 'd Bdd.Expr0.t -> 'd Bdd.Expr0.t
  val eq :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Bdd.Expr0.t -> 'd Bdd.Expr0.t -> 'd Bdd.Expr0.O.Bool.t
  val substitute_by_var :
    ?memo:Cudd.Memo.t ->
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Bdd.Expr0.t -> ('a * 'a) list -> 'd Bdd.Expr0.t
  val substitute_by_var_list :
    ?memo:Cudd.Memo.t ->
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Bdd.Expr0.t list -> ('a * 'a) list -> 'd Bdd.Expr0.t list
  val substitute :
    ?memo:Cudd.Memo.t ->
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Bdd.Expr0.t -> ('a * 'd Bdd.Expr0.t) list -> 'd Bdd.Expr0.t
  val substitute_list :
    ?memo:Cudd.Memo.t ->
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Bdd.Expr0.t list -> ('a * 'd Bdd.Expr0.t) list -> 'd Bdd.Expr0.t list
  val support :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Bdd.Expr0.t -> 'a PSette.t
  val support_cond : 'd Cudd.Man.t -> 'd Bdd.Expr0.t -> 'd Cudd.Bdd.t
  val cube_of_bdd :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'd Cudd.Bdd.t -> 'd Cudd.Bdd.t
  val tbdd_of_texpr : 'd Bdd.Expr0.t array -> 'd Cudd.Bdd.t array
  val texpr_of_tbdd :
    'd Bdd.Expr0.t array -> 'd Cudd.Bdd.t array -> 'd Bdd.Expr0.t array
  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.Expr0.t ] -> unit
  val print_minterm :
    ?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 -> Cudd.Man.tbool array -> unit
  val print_bdd :
    ?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 Cudd.Bdd.t -> unit
  val print_idcondb :
    ?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 -> int * bool -> unit
  val print_idcond :
    ?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 -> int -> unit
  val permutation_of_rename :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    ('a * 'a) list -> int array
  val composition_of_lvarexpr :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    ('a * 'd Bdd.Expr0.t) list -> 'd Cudd.Bdd.t array
  val composition_of_lvarlexpr :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'a list -> 'd Bdd.Expr0.t list -> 'd Cudd.Bdd.t array
  val bddsupport :
    ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
    'a list -> 'd Cudd.Bdd.t
  val varmap : 'a Bdd.Expr0.t -> 'a Bdd.Expr0.t
  val permute :
    ?memo:Cudd.Memo.t -> 'd Bdd.Expr0.t -> int array -> 'd Bdd.Expr0.t
  val compose :
    ?memo:Cudd.Memo.t ->
    'd Bdd.Expr0.t -> 'd Cudd.Bdd.t array -> 'd Bdd.Expr0.t
  val permute_list :
    ?memo:Cudd.Memo.t ->
    'd Bdd.Expr0.t list -> int array -> 'd Bdd.Expr0.t list
  val compose_list :
    ?memo:Cudd.Memo.t ->
    'd Bdd.Expr0.t list -> 'd Cudd.Bdd.t array -> 'd Bdd.Expr0.t list
  module Expr :
    sig
      type 'a atom =
          Tbool of 'a * bool
        | Tint of 'a * int list
        | Tenum of 'a * 'a list
      type 'a term =
          Tatom of 'a Bdd.Expr0.O.Expr.atom
        | Texternal of (int * bool)
        | Tcst of bool
      val map_atom :
        ('a -> 'b) -> 'a Bdd.Expr0.O.Expr.atom -> 'b Bdd.Expr0.O.Expr.atom
      val map_term :
        ('a -> 'b) -> 'a Bdd.Expr0.O.Expr.term -> 'b Bdd.Expr0.O.Expr.term
      val term_of_vint :
        'a -> 'd Bdd.Int.t -> Bdd.Reg.Minterm.t -> 'a Bdd.Expr0.O.Expr.term
      val term_of_venum :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'a -> 'd Bdd.Enum.t -> Bdd.Reg.Minterm.t -> 'a Bdd.Expr0.O.Expr.term
      val term_of_idcondb :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        int * bool -> 'a Bdd.Expr0.O.Expr.term
      val bool_of_tbool : Cudd.Man.tbool -> bool
      val mand :
        'a Bdd.Expr0.O.Expr.term list Pervasives.ref ->
        'a Bdd.Expr0.O.Expr.term -> unit
      val conjunction_of_minterm :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        Cudd.Man.tbool array ->
        'a Bdd.Expr0.O.Expr.term Bdd.Normalform.conjunction
      val dnf_of_bdd :
        ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'd Cudd.Bdd.t -> 'a Bdd.Expr0.O.Expr.term Bdd.Normalform.dnf
      val print_term :
        ?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 -> 'a Bdd.Expr0.O.Expr.term -> unit
      val print_conjunction :
        ?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 ->
        'a Bdd.Expr0.O.Expr.term Bdd.Normalform.conjunction -> unit
      val print_dnf :
        ?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 ->
        'a Bdd.Expr0.O.Expr.term Bdd.Normalform.dnf -> unit
    end
end