You can search for identifiers within the package.
in-package search v0.2.0
Boolean
Operation over bit-vectors of size 1.
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.
of_bool b
bool
The boolean value.
Either true' or false'.
true'
false'
val of_bv : bv term -> t
of_bv t create a bit-wise or reduction of all bits.
of_bv t
The bit-vector term.
A term equal to t <> 0.
t <> 0
val logand : t -> t -> t
logand t0 t1 create a boolean and.
logand t0 t1
The first boolean term.
The second boolean term.
SMT-LIB: and
and
val lognand : t -> t -> t
lognand t0 t1 create a boolean nand.
lognand t0 t1
SMT-LIB: bvnand
bvnand
val redand : t array -> t
redand ts create a nary boolean and.
redand ts
The boolean terms.
val logor : t -> t -> t
logor t0 t1 create a boolean or.
logor t0 t1
SMT-LIB: or
or
val lognor : t -> t -> t
lognor t0 t1 create a boolean nor.
lognor t0 t1
SMT-LIB: bvnor
bvnor
val redor : t array -> t
redor ts create a nary boolean or.
redor ts
val logxor : t -> t -> t
logxor t0 t1 create a boolean xor.
logxor t0 t1
SMT-LIB: xor
xor
val logxnor : t -> t -> t
logxnor t0 t1 create a boolean xnor.
logxnor t0 t1
SMT-LIB: bvxnor
bvxnor
val redxor : t array -> t
redxor ts create a nary boolean xor.
redxor ts
val lognot : t -> t
lognot t create a boolean not.
lognot t
The boolean term.
SMT-LIB: not
not
val iff : t -> t -> t
iff t0 t1 create a boolean if and only if.
iff t0 t1
SMT-LIB: =
=
val implies : t -> t -> t
implies t0 t1 create a boolean implies.
implies t0 t1
SMT-LIB: =>
=>
val assignment : bv value -> bool
assignment t get boolean representation of the current model value of given boolean term.
assignment t
The term to query a model value for.
boolean representation of current model value of term t.
t