sig
  type t = Bddenum.t
  val of_expr : Formula.expr -> Formula.Benum.t
  val to_expr : Formula.Benum.t -> Formula.expr
  val var : #Formula.db -> Var.t -> Formula.Benum.t
  val ite :
    #Formula.db ->
    Bdd.t -> Formula.Benum.t -> Formula.Benum.t -> Formula.Benum.t
  val eq : #Formula.db -> Formula.Benum.t -> Formula.Benum.t -> Bdd.t
  val eq_label : #Formula.db -> Formula.Benum.t -> Var.t -> Bdd.t
  val print : #Formula.db -> Format.formatter -> Formula.Benum.t -> unit
end