sig
  type atom =
      Tbool of Var.t * bool
    | Tint of Var.t * int list
    | Tenum of Var.t * Var.t list
  type term =
      Tatom of Bddvar.Expr.atom
    | Texternal of int * bool
    | Tcst of bool
  type conjunction = Conjunction of Bddvar.Expr.term list | Cfalse
  type disjunction = Disjunction of Bddvar.Expr.conjunction list | Dtrue
  val term_of_vint :
    Var.t -> Bddint.t -> Bddreg.Minterm.t -> Bddvar.Expr.term
  val term_of_venum :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    Var.t -> Bddenum.t -> Bddreg.Minterm.t -> Bddvar.Expr.term
  val term_of_idcondb :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    MappeI.key * bool -> Bddvar.Expr.term
  val bool_of_tbool : Manager.tbool -> bool
  val mand : Bddvar.Expr.term list Pervasives.ref -> Bddvar.Expr.term -> unit
  val conjunction_of_minterm :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    Manager.tbool array -> Bddvar.Expr.conjunction
  val disjunction_of_bdd :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    Bdd.t -> Bddvar.Expr.disjunction
  val print_term :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    Format.formatter -> Bddvar.Expr.term -> unit
  val print_conjunction :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    Format.formatter -> Bddvar.Expr.conjunction -> unit
  val print_disjunction :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    Format.formatter -> Bddvar.Expr.disjunction -> unit
end