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