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