Module `Term.Bl`

Boolean

type t = bv term: A boolean term.

val false' : t: A bit-vector value 0 of size 1.

val true' : t: A bit-vector value 1 of size 1.

val of_bool : bool -> t

of_bool b create a bit-vector value of size 1 from a bool.

parameter b: The boolean value.

returns: Either true' or false'.

val of_bv : bv term -> t

of_bv t create a bit-wise or reduction of all bits.

parameter t: The bit-vector term.

returns: A term equal to t <> 0.

val logand : t -> t -> t

logand t0 t1 create a boolean and.

parameter t0: The first boolean term.

parameter t1: The second boolean term.

returns: SMT-LIB: and

val lognand : t -> t -> t

lognand t0 t1 create a boolean nand.

parameter t0: The first boolean term.

parameter t1: The second boolean term.

returns: SMT-LIB: bvnand

val redand : t array -> t

redand ts create a nary boolean and.

parameter ts: The boolean terms.

returns: SMT-LIB: and

val logor : t -> t -> t

logor t0 t1 create a boolean or.

parameter t0: The first boolean term.

parameter t1: The second boolean term.

returns: SMT-LIB: or

val lognor : t -> t -> t

lognor t0 t1 create a boolean nor.

parameter t0: The first boolean term.

parameter t1: The second boolean term.

returns: SMT-LIB: bvnor

val redor : t array -> t

redor ts create a nary boolean or.

parameter ts: The boolean terms.

returns: SMT-LIB: or

val logxor : t -> t -> t

logxor t0 t1 create a boolean xor.

parameter t0: The first boolean term.

parameter t1: The second boolean term.

returns: SMT-LIB: xor

val logxnor : t -> t -> t

logxnor t0 t1 create a boolean xnor.

parameter t0: The first boolean term.

parameter t1: The second boolean term.

returns: SMT-LIB: bvxnor

val redxor : t array -> t

redxor ts create a nary boolean xor.

parameter ts: The boolean terms.

returns: SMT-LIB: xor

val lognot : t -> t

lognot t create a boolean not.

parameter t: The boolean term.

returns: SMT-LIB: not

val iff : t -> t -> t

iff t0 t1 create a boolean if and only if.

parameter t0: The first boolean term.

parameter t1: The second boolean term.

returns: SMT-LIB: =

val implies : t -> t -> t

implies t0 t1 create a boolean implies.

parameter t0: The first boolean term.

parameter t1: The second boolean term.

returns: SMT-LIB: =>

val assignment : bv value -> bool

assignment t get boolean representation of the current model value of given boolean term.

parameter t: The term to query a model value for.

returns: boolean representation of current model value of term t.