sig
  type 'a atom =
      Tbool of 'a * bool
    | Tint of 'a * int list
    | Tenum of 'a * 'a list
  type 'a term =
      Tatom of 'a Expr0.O.Expr.atom
    | Texternal of (int * bool)
    | Tcst of bool
  type 'a conjunction = Conjunction of 'a Expr0.O.Expr.term list | Cfalse
  type 'a disjunction =
      Disjunction of 'a Expr0.O.Expr.conjunction list
    | Dtrue
  val map_atom : ('a -> 'b) -> 'a Expr0.O.Expr.atom -> 'b Expr0.O.Expr.atom
  val map_term : ('a -> 'b) -> 'a Expr0.O.Expr.term -> 'b Expr0.O.Expr.term
  val map_conjunction :
    ('a -> 'b) -> 'a Expr0.O.Expr.conjunction -> 'b Expr0.O.Expr.conjunction
  val map_disjunction :
    ('a -> 'b) -> 'a Expr0.O.Expr.disjunction -> 'b Expr0.O.Expr.disjunction
  val term_of_vint : 'a -> 'b Int.t -> Reg.Minterm.t -> 'a Expr0.O.Expr.term
  val term_of_venum :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    'a -> 'b Enum.t -> Reg.Minterm.t -> 'a Expr0.O.Expr.term
  val term_of_idcondb :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    int * bool -> 'a Expr0.O.Expr.term
  val bool_of_tbool : Cudd.Man.tbool -> bool
  val mand :
    'a Expr0.O.Expr.term list Pervasives.ref -> 'a Expr0.O.Expr.term -> unit
  val conjunction_of_minterm :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    Cudd.Man.tbool array -> 'a Expr0.O.Expr.conjunction
  val disjunction_of_bdd :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    'b Cudd.Bdd.t -> 'a Expr0.O.Expr.disjunction
  val print_term :
    ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    Format.formatter -> 'a Expr0.O.Expr.term -> unit
  val print_conjunction :
    ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    Format.formatter -> 'a Expr0.O.Expr.conjunction -> unit
  val print_disjunction :
    ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    Format.formatter -> 'a Expr0.O.Expr.disjunction -> unit
end