"/>

Module Term.Bv

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.