Module Typed.Bool

type t = bool expr
val true_ : t

The boolean literal true.

val false_ : t

The boolean literal false.

val of_bool : bool -> t
val symbol : Symbol.t -> t
val not : t -> t

not t is the logical negation of t.

val and_ : t -> t -> t

and_ t1 t2 is the logical conjunction of t1 and t2.

val or_ : t -> t -> t

or_ t1 t2 is the logical disjunction of t1 and t2.

val logand : t list -> t
val logor : t list -> t
val xor : t -> t -> t

xor t1 t2 is the exclusive-or of t1 and t2.

val implies : t -> t -> t

implies t1 t2 constructs the implication t1 => t2.

val eq : 'a expr -> 'a expr -> t

eq t1 t2 returns true if t1 and t2 are structurally equal.

val distinct : 'a expr list -> t

distinct es returns true if all expressions in the list es are pair-wise distinct.

val ite : t -> 'a expr -> 'a expr -> 'a expr

ite cond then_ else_ constructs an if-then-else expression. Returns then_ if cond evaluates to true, and else_ otherwise.

val split_conjunctions : t -> Expr.Set.t

split_conjunctions t breaks a conjunction term into a set of its top-level conjuncts.

val pp : t Fmt.t