Module Const.Bitv

A module for bit vector constant symbols that occur in terms.

val bitv : string -> t

Bitvetor literals.

val to_nat : int -> t

Conversion to integers.

val of_int : int -> t

Conversion from integers.

val concat : (int * int) -> t

Bitvector concatenation.

val extract : (int * int * int) -> t

Bitvector extraction.

val repeat : (int * int) -> t

Bitvector repetition.

val zero_extend : (int * int) -> t

Bitvector extension with zeros.

val sign_extend : (int * int) -> t

Bitvector extension with its most significant.

val rotate_right : (int * int) -> t

Bitvector rotation to the right.

val rotate_left : (int * int) -> t

Bitvector rotation to the left.

val not : int -> t

Bitwise negation.

val and_ : int -> t

Bitwise conjunction.

val or_ : int -> t

Bitwise disjunction.

val nand : int -> t

Bitwise nand.

val nor : int -> t

Bitwise nor.

val xor : int -> t

Bitwise xor.

val xnor : int -> t

Bitwise xnor.

val comp : int -> t

Bitwise comparison.

val neg : int -> t

Arithmetic complement on bitvectors.

val add : int -> t

Arithmetic addition on bitvectors.

val sub : int -> t

Arithmetic substraction on bitvectors.

val mul : int -> t

Arithmetic multiplication on bitvectors.

val udiv : int -> t

Arithmetic euclidian integer division on bitvectors.

val urem : int -> t

Arithmetic euclidian integer remainder on bitvectors.

val sdiv : int -> t

Arithmetic 2's complement signed division. (see smtlib's specification for more information).

val srem : int -> t

Arithmetic 2's coplement signed remainder (sign follows dividend). (see smtlib's specification for more information).

val smod : int -> t

Arithmetic 2's coplement signed remainder (sign follows divisor). (see smtlib's specification for more information).

val shl : int -> t

Logical shift left.

val lshr : int -> t

Logical shift right.

val ashr : int -> t

Arithmetic shift right.

val ult : int -> t

Boolean arithmetic comparison (less than).

val ule : int -> t

Boolean arithmetic comparison (less or equal than).

val ugt : int -> t

Boolean arithmetic comparison (greater than).

val uge : int -> t

Boolean arithmetic comparison (greater or equal than).

val slt : int -> t

Boolean signed arithmetic comparison (less than). (See smtlib's specification for more information).

val sle : int -> t

Boolean signed arithmetic comparison (less or equal than).

val sgt : int -> t

Boolean signed arithmetic comparison (greater than).

val sge : int -> t

Boolean signed arithmetic comparison (greater or equal than).