package bitwuzla

  1. Overview
  2. Docs

Bit-vector

type t = bv term

A bit-vector term.

val zero : bv sort -> t

zero sort create a bit-vector value zero.

  • parameter sort

    The sort of the value.

  • returns

    A term representing the bit-vector value 0 of given sort.

val one : bv sort -> t

one sort create a bit-vector value one.

  • parameter sort

    The sort of the value.

  • returns

    A term representing the bit-vector value 1 of given sort.

val ones : bv sort -> t

ones sort create a bit-vector value where all bits are set to 1.

  • parameter sort

    The sort of the value.

  • returns

    A term representing the bit-vector value of given sort where all bits are set to 1.

val min_signed : bv sort -> t

min_signed sort create a bit-vector minimum signed value.

  • parameter sort

    The sort of the value.

  • returns

    A term representing the bit-vector value of given sort where the MSB is set to 1 and all remaining bits are set to 0.

val max_signed : bv sort -> t

max_signed sort create a bit-vector maximum signed value.

  • parameter sort

    The sort of the value.

  • returns

    A term representing the bit-vector value of given sort where the MSB is set to 0 and all remaining bits are set to 1.

val of_int : bv sort -> int -> t

of_int sort value create a bit-vector value from its unsigned integer representation.

If given value does not fit into a bit-vector of given size (sort), the value is truncated to fit.

  • parameter sort

    The sort of the value.

  • parameter value

    The unsigned integer representation of the bit-vector value.

  • returns

    A term representing the bit-vector value of given sort.

val of_z : bv sort -> Z.t -> t

of_z sort value create a bit-vector value from its unsigned integer representation.

If given value does not fit into a bit-vector of given size (sort), the value is truncated to fit.

  • parameter sort

    The sort of the value.

  • parameter value

    The unsigned integer representation of the bit-vector value.

  • returns

    A term representing the bit-vector value of given sort.

val of_string : bv sort -> string -> t

of_string sort value create a bit-vector value from its string representation.

Prefix determine the base of the string representation:

  • 0b for binary;
  • 0x for hexadecimal;
  • others for decimal.

Given value must fit into a bit-vector of given size (sort).

  • parameter sort

    The sort of the value.

  • parameter value

    A string representing the value.

  • returns

    A term representing the bit-vector value of given sort.

type (!'a, !'b) operator =
  1. | Add : (t -> t -> t, t * t) operator
    (*

    Bit-vector addition.

    SMT-LIB: bvadd

    *)
  2. | And : (t -> t -> t, t * t) operator
    (*

    Bit-vector and.

    SMT-LIB: bvand

    *)
  3. | Ashr : (t -> t -> t, t * t) operator
    (*

    Bit-vector arithmetic right shift.

    SMT-LIB: bvashr

    *)
  4. | Concat : (t -> t -> t, t * t) operator
    (*

    Bit-vector concat.

    SMT-LIB: concat

    *)
  5. | Extract : (hi:int -> lo:int -> t -> t, int * int * t) operator
    (*

    Bit-vector extract.

    SMT-LIB: extract (indexed)

    *)
  6. | Mul : (t -> t -> t, t * t) operator
    (*

    Bit-vector multiplication.

    SMT-LIB: bvmul

    *)
  7. | Neg : (t -> t, t) operator
    (*

    Bit-vector negation (two's complement).

    SMT-LIB: bvneg

    *)
  8. | Not : (t -> t, t) operator
    (*

    Bit-vector not (one's complement).

    SMT-LIB: bvnot

    *)
  9. | Or : (t -> t -> t, t * t) operator
    (*

    Bit-vector or.

    SMT-LIB: bvor

    *)
  10. | Rol : (t -> t -> t, t * t) operator
    (*

    Bit-vector rotate left (not indexed).

    This is a non-indexed variant of SMT-LIB rotate_left.

    *)
  11. | Ror : (t -> t -> t, t * t) operator
    (*

    Bit-vector rotate right.

    This is a non-indexed variant of SMT-LIB rotate_right.

    *)
  12. | Sdiv : (t -> t -> t, t * t) operator
    (*

    Bit-vector signed division.

    SMT-LIB: bvsdiv

    *)
  13. | Sge : (t -> t -> t, t * t) operator
    (*

    Bit-vector signed greater than or equal.

    SMT-LIB: bvsge

    *)
  14. | Sgt : (t -> t -> t, t * t) operator
    (*

    Bit-vector signed greater than.

    SMT-LIB: bvsgt

    *)
  15. | Shl : (t -> t -> t, t * t) operator
    (*

    Bit-vector signed less than.

    SMT-LIB: bvslt

    *)
  16. | Shr : (t -> t -> t, t * t) operator
    (*

    Bit-vector logical right shift.

    SMT-LIB: bvshr

    *)
  17. | Sle : (t -> t -> t, t * t) operator
    (*

    Bit-vector signed less than or equal.

    SMT-LIB: bvsle

    *)
  18. | Slt : (t -> t -> t, t * t) operator
    (*

    Bit-vector signed less than.

    SMT-LIB: bvslt

    *)
  19. | Smod : (t -> t -> t, t * t) operator
    (*

    Bit-vector signed modulo.

    SMT-LIB: bvsmod

    *)
  20. | Srem : (t -> t -> t, t * t) operator
    (*

    Bit-vector signed remainder.

    SMT-LIB: bvsrem

    *)
  21. | Sub : (t -> t -> t, t * t) operator
    (*

    Bit-vector subtraction.

    SMT-LIB: bvsub

    *)
  22. | Udiv : (t -> t -> t, t * t) operator
    (*

    Bit-vector unsigned division.

    SMT-LIB: bvudiv

    *)
  23. | Uge : (t -> t -> t, t * t) operator
    (*

    Bit-vector unsigned greater than or equal.

    SMT-LIB: bvuge

    *)
  24. | Ugt : (t -> t -> t, t * t) operator
    (*

    Bit-vector unsigned greater than.

    SMT-LIB: bvugt

    *)
  25. | Ule : (t -> t -> t, t * t) operator
    (*

    Bit-vector unsigned less than or equal.

    SMT-LIB: bvule

    *)
  26. | Ult : (t -> t -> t, t * t) operator
    (*

    Bit-vector unsigned less than.

    SMT-LIB: bvult

    *)
  27. | Urem : (t -> t -> t, t * t) operator
    (*

    Bit-vector unsigned remainder.

    SMT-LIB: bvurem

    *)
  28. | Xor : (t -> t -> t, t * t) operator
    (*

    Bit-vector xor.

    SMT-LIB: bvxor

    *)

The term operator.

val term : ('a, 'b) operator -> 'a

term op .. create a bit-vector term constructor of given kind.

  • parameter op

    The operator kind.

  • returns

    A function to build a term representing an operation of given kind.

val pred : t -> t

pred t create a bit-vector decrement.

  • parameter t

    The bit-vector term.

  • returns

    Decrement by one.

val succ : t -> t

succ t create a bit-vector increment.

  • parameter t

    The bit-vector term.

  • returns

    Increment by one.

val neg : t -> t

neg t create a bit-vector negation.

  • parameter t

    The bit-vector term.

  • returns

    SMT-LIB: bvneg.

val add : t -> t -> t

add t0 t1 create a bit-vector addition.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvadd

val sadd_overflow : t -> t -> t

sadd_overflow t0 t1 create a bit-vector signed addition overflow test.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    Single bit to indicate if signed addition produces an overflow

val uadd_overflow : t -> t -> t

uadd_overflow t0 t1 create a bit-vector unsigned addition overflow test.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    Single bit to indicate if unsigned addition produces an overflow

val sub : t -> t -> t

sub t0 t1 create a bit-vector substraction.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvsub

val ssub_overflow : t -> t -> t

ssub_overflow t0 t1 create a bit-vector signed substraction overflow test.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    Single bit to indicate if signed substraction produces an overflow

val usub_overflow : t -> t -> t

usub_overflow t0 t1 create a bit-vector ubsigned substraction overflow test.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    Single bit to indicate if unsigned substraction produces an overflow

val mul : t -> t -> t

mul t0 t1 create a bit-vector multiplication.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvmul

val smul_overflow : t -> t -> t

smul_overflow t0 t1 create a bit-vector signed multiplication overflow test.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    Single bit to indicate if signed multiplication produces an overflow

val umul_overflow : t -> t -> t

umul_overflow t0 t1 create a bit-vector unsigned multiplication overflow test.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    Single bit to indicate if unsigned multiplication produces an overflow

val sdiv : t -> t -> t

sdiv t0 t1 create a bit-vector signed division.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvsdiv

val sdiv_overflow : t -> t -> t

sdiv_overflow t0 t1 create a bit-vector signed division overflow test.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    Single bit to indicate if signed division produces an overflow

val udiv : t -> t -> t

udiv t0 t1 create a bit-vector unsigned division.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvudiv

val smod : t -> t -> t

smod t0 t1 create a bit-vector signed modulo.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvsmod

val srem : t -> t -> t

srem t0 t1 create a bit-vector signed reminder.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvsrem

val urem : t -> t -> t

urem t0 t1 create a bit-vector unsigned reminder.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvurem

val logand : t -> t -> t

logand t0 t1 create a bit-vector and.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvand

val lognand : t -> t -> t

lognand t0 t1 create a bit-vector nand.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvnand

val redand : t -> t

redand t create a bit-vector and reduction.

  • parameter t

    The bit-vector term.

  • returns

    Bit-wise and reduction, all bits are and'ed together into a single bit.

val logor : t -> t -> t

logor t0 t1 create a bit-vector or.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvor

val lognor : t -> t -> t

lognor t0 t1 create a bit-vector nor.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvnor

val redor : t -> t

redor t create a bit-vector or reduction.

  • parameter t

    The bit-vector term.

  • returns

    Bit-wise or reduction, all bits are or'ed together into a single bit.

val logxor : t -> t -> t

logxor t0 t1 create a bit-vector xor.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvxor

val logxnor : t -> t -> t

logxnor t0 t1 create a bit-vector xnor.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvxnor

val redxor : t -> t

redxor t create a bit-vector xor reduction.

  • parameter t

    The bit-vector term.

  • returns

    Bit-wise xor reduction, all bits are xor'ed together into a single bit.

val lognot : t -> t

lognot t create a bit-vector not (one's complement).

  • parameter t

    The first bit-vector term.

  • returns

    SMT-LIB: bvnot

val shift_left : t -> t -> t

shift_left t0 t1 create a bit-vector logical left shift.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB bvshl

val shift_right : t -> t -> t

shift_right t0 t1 create a bit-vector arithmetic right shift.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB bvashr

val shift_right_logical : t -> t -> t

shift_right_logical t0 t1 create a bit-vector logical right shift.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB bvshr

val rotate_left : t -> t -> t

rotate_left t0 t1 create a bit-vector left rotation.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    non indexed variant of SMT-LIB rotate_left

val rotate_lefti : t -> int -> t

rotate_lefti t n create a bit-vector left rotation.

  • parameter t

    The bit-vector term.

  • parameter n

    The rotation count.

  • returns

    SMT-LIB: rotate_left (indexed)

val rotate_right : t -> t -> t

rotate_right t0 t1 create a bit-vector right rotation.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    non indexed variant of SMT-LIB rotate_right

val rotate_righti : t -> int -> t

rotate_righti t n create a bit-vector right rotation.

  • parameter t

    The bit-vector term.

  • parameter n

    The rotation count.

  • returns

    SMT-LIB: rotate_right (indexed)

val zero_extend : int -> t -> t

zero_extend n t create a bit-vector unsigned extension.

  • parameter n

    The number of bits.

  • parameter t

    The bit-vector term.

  • returns

    SMT-LIB: zero_extend (indexed)

val sign_extend : int -> t -> t

sign_extend n t create a bit-vector signed extension.

  • parameter n

    The number of bits.

  • parameter t

    The bit-vector term.

  • returns

    SMT-LIB: sign_extend (indexed)

val append : t -> t -> t

append t0 t1 create a bit-vector concat.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: concat

val concat : t array -> t

concat ts create a bit-vector nary concat.

  • parameter ts

    The bit-vector terms.

  • returns

    SMT-LIB: concat

val repeat : int -> t -> t

repeat n t create a bit-vector repetition.

  • parameter n

    The number of repetitions.

  • parameter t

    The bit-vector term.

  • returns

    SMT-LIB: repeat (indexed)

val extract : hi:int -> lo:int -> t -> t

extract hi lo t create a bit-vector extract.

  • parameter hi

    MSB index.

  • parameter lo

    LSB index.

  • parameter t

    The bit-vector term.

  • returns

    SMT-LIB: extract (indexed)

val sge : t -> t -> t

sge t0 t1 create a bit-vector signed greater than or equal.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvsge

val uge : t -> t -> t

uge t0 t1 create a bit-vector unsigned greater than or equal.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvuge

val sgt : t -> t -> t

sgt t0 t1 create a bit-vector signed greater than.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvsgt

val ugt : t -> t -> t

ugt t0 t1 create a bit-vector unsigned greater than.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvugt

val sle : t -> t -> t

sle t0 t1 create a bit-vector signed lower than or equal.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvsle

val ule : t -> t -> t

ule t0 t1 create a bit-vector unsigned lower than or equal.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvadd

val slt : t -> t -> t

slt t0 t1 create a bit-vector signed lower than.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvslt

val ult : t -> t -> t

ult t0 t1 create a bit-vector unsigned lower than.

  • parameter t0

    The first bit-vector term.

  • parameter t1

    The second bit-vector term.

  • returns

    SMT-LIB: bvult

val to_bl : t -> t

Same as Bl.of_bv.

val assignment : bv value -> Z.t

assignment t get bit-vector representation of the current model value of given term.

  • parameter t

    The term to query a model value for.

  • returns

    bit-vector representation of current model value of term t.

OCaml

Innovation. Community. Security.