sig
  type t = Bdd.t
  val of_expr : Formula.expr -> Formula.Bool.t
  val to_expr : Formula.Bool.t -> Formula.expr
  val dtrue : #Formula.db -> Formula.Bool.t
  val dfalse : #Formula.db -> Formula.Bool.t
  val of_bool : #Formula.db -> bool -> Formula.Bool.t
  val var : #Formula.db -> Var.t -> Formula.Bool.t
  val dnot : #Formula.db -> Formula.Bool.t -> Formula.Bool.t
  val dand :
    #Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
  val dor : #Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
  val xor : #Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
  val nand :
    #Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
  val nor : #Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
  val nxor :
    #Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
  val eq : #Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
  val ite :
    #Formula.db ->
    Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
  val is_included_in :
    ?sem:bool -> #Formula.db -> Formula.Bool.t -> Formula.Bool.t -> bool
  val is_inter_empty :
    ?sem:bool -> #Formula.db -> Formula.Bool.t -> Formula.Bool.t -> bool
  val exists :
    ?sem:bool ->
    #Formula.db -> Var.t list -> Formula.Bool.t -> Formula.Bool.t
  val forall :
    ?sem:bool ->
    #Formula.db -> Var.t list -> Formula.Bool.t -> Formula.Bool.t
  val print : #Formula.db -> Format.formatter -> Formula.Bool.t -> unit
end