Module F.Bl

type t
val const : string -> t

const name creates the (first-order) boolean constant named name .

val top : t

The value true.

val bot : t

The value false.

val lognot : t -> t

lognot x y creates the boolean not operation of x.

val logand : t -> t -> t

logand x y creates the boolean and operation between x and y.

val logor : t -> t -> t

logor x y creates the boolean or operation between x and y.

val logxor : t -> t -> t

logxor x y creates the boolean xor operation between x and y.

val ite : t -> t -> t -> t

ite x y z creates the boolean ite operation between y and z according to x.

val equal : t -> t -> t

equal x y creates the boolean = operation between x and y.

val diff : t -> t -> t

diff x y creates the boolean <> operation between x and y.

val implies : t -> t -> t

implies x y creates the boolean => operation between x and y.

val to_bv : t -> Bv.t

to_bv x cast the boolean x as a 1-bit bitvector.