Module Const.BitvSource

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

Sourceval bitv : string -> t

Bitvetor literals.

Sourceval concat : (int * int) -> t

Bitvector concatenation.

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

Bitvector extraction.

Sourceval repeat : (int * int) -> t

Bitvector repetition.

Sourceval zero_extend : (int * int) -> t

Bitvector extension with zeros.

Sourceval sign_extend : (int * int) -> t

Bitvector extension with its most significant.

Sourceval rotate_right : (int * int) -> t

Bitvector rotation to the right.

Sourceval rotate_left : (int * int) -> t

Bitvector rotation to the left.

Sourceval not : int -> t

Bitwise negation.

Sourceval and_ : int -> t

Bitwise conjunction.

Sourceval or_ : int -> t

Bitwise disjunction.

Sourceval nand : int -> t

Bitwise nand.

Sourceval nor : int -> t

Bitwise nor.

Sourceval xor : int -> t

Bitwise xor.

Sourceval xnor : int -> t

Bitwise xnor.

Sourceval comp : int -> t

Bitwise comparison.

Sourceval neg : int -> t

Arithmetic complement on bitvectors.

Sourceval add : int -> t

Arithmetic addition on bitvectors.

Sourceval sub : int -> t

Arithmetic substraction on bitvectors.

Sourceval mul : int -> t

Arithmetic multiplication on bitvectors.

Sourceval udiv : int -> t

Arithmetic euclidian integer division on bitvectors.

Sourceval urem : int -> t

Arithmetic euclidian integer remainder on bitvectors.

Sourceval sdiv : int -> t

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

Sourceval srem : int -> t

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

Sourceval smod : int -> t

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

Sourceval shl : int -> t

Logical shift left.

Sourceval lshr : int -> t

Logical shift right.

Sourceval ashr : int -> t

Arithmetic shift right.

Sourceval ult : int -> t

Boolean arithmetic comparison (less than).

Sourceval ule : int -> t

Boolean arithmetic comparison (less or equal than).

Sourceval ugt : int -> t

Boolean arithmetic comparison (greater than).

Sourceval uge : int -> t

Boolean arithmetic comparison (greater or equal than).

Sourceval slt : int -> t

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

Sourceval sle : int -> t

Boolean signed arithmetic comparison (less or equal than).

Sourceval sgt : int -> t

Boolean signed arithmetic comparison (greater than).

Sourceval sge : int -> t

Boolean signed arithmetic comparison (greater or equal than).