bitwuzla 1.0.3 · OCaml Package

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 =

| Add : (t -> t -> t, t * t) operator
(*
Bit-vector addition.
SMT-LIB: bvadd
*)
| And : (t -> t -> t, t * t) operator
(*
Bit-vector and.
SMT-LIB: bvand
*)
| Ashr : (t -> t -> t, t * t) operator
(*
Bit-vector arithmetic right shift.
SMT-LIB: bvashr
*)
| Concat : (t -> t -> t, t * t) operator
(*
Bit-vector concat.
SMT-LIB: concat
*)
| Extract : (hi:int -> lo:int -> t -> t, int * int * t) operator
(*
Bit-vector extract.
SMT-LIB: extract (indexed)
*)
| Mul : (t -> t -> t, t * t) operator
(*
Bit-vector multiplication.
SMT-LIB: bvmul
*)
| Neg : (t -> t, t) operator
(*
Bit-vector negation (two's complement).
SMT-LIB: bvneg
*)
| Not : (t -> t, t) operator
(*
Bit-vector not (one's complement).
SMT-LIB: bvnot
*)
| Or : (t -> t -> t, t * t) operator
(*
Bit-vector or.
SMT-LIB: bvor
*)
| Rol : (t -> t -> t, t * t) operator
(*
Bit-vector rotate left (not indexed).
This is a non-indexed variant of SMT-LIB rotate_left.
*)
| Ror : (t -> t -> t, t * t) operator
(*
Bit-vector rotate right.
This is a non-indexed variant of SMT-LIB rotate_right.
*)
| Sdiv : (t -> t -> t, t * t) operator
(*
Bit-vector signed division.
SMT-LIB: bvsdiv
*)
| Sge : (t -> t -> t, t * t) operator
(*
Bit-vector signed greater than or equal.
SMT-LIB: bvsge
*)
| Sgt : (t -> t -> t, t * t) operator
(*
Bit-vector signed greater than.
SMT-LIB: bvsgt
*)
| Shl : (t -> t -> t, t * t) operator
(*
Bit-vector signed less than.
SMT-LIB: bvslt
*)
| Shr : (t -> t -> t, t * t) operator
(*
Bit-vector logical right shift.
SMT-LIB: bvshr
*)
| Sle : (t -> t -> t, t * t) operator
(*
Bit-vector signed less than or equal.
SMT-LIB: bvsle
*)
| Slt : (t -> t -> t, t * t) operator
(*
Bit-vector signed less than.
SMT-LIB: bvslt
*)
| Smod : (t -> t -> t, t * t) operator
(*
Bit-vector signed modulo.
SMT-LIB: bvsmod
*)
| Srem : (t -> t -> t, t * t) operator
(*
Bit-vector signed remainder.
SMT-LIB: bvsrem
*)
| Sub : (t -> t -> t, t * t) operator
(*
Bit-vector subtraction.
SMT-LIB: bvsub
*)
| Udiv : (t -> t -> t, t * t) operator
(*
Bit-vector unsigned division.
SMT-LIB: bvudiv
*)
| Uge : (t -> t -> t, t * t) operator
(*
Bit-vector unsigned greater than or equal.
SMT-LIB: bvuge
*)
| Ugt : (t -> t -> t, t * t) operator
(*
Bit-vector unsigned greater than.
SMT-LIB: bvugt
*)
| Ule : (t -> t -> t, t * t) operator
(*
Bit-vector unsigned less than or equal.
SMT-LIB: bvule
*)
| Ult : (t -> t -> t, t * t) operator
(*
Bit-vector unsigned less than.
SMT-LIB: bvult
*)
| Urem : (t -> t -> t, t * t) operator
(*
Bit-vector unsigned remainder.
SMT-LIB: bvurem
*)
| 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.

package bitwuzla