package bitwuzla

  1. Overview
  2. Docs

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.

  • parameter b

    The boolean value.

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.

OCaml

Innovation. Community. Security.