Module Z3.BitVector

module BitVector: sig .. end

Functions to manipulate bit-vector expressions

val mk_sort : context -> int -> Sort.sort

Create a new bit-vector sort.

val is_bv : Expr.expr -> bool

Indicates whether the terms is of bit-vector sort.

val is_bv_numeral : Expr.expr -> bool

Indicates whether the term is a bit-vector numeral

val is_bv_bit1 : Expr.expr -> bool

Indicates whether the term is a one-bit bit-vector with value one

val is_bv_bit0 : Expr.expr -> bool

Indicates whether the term is a one-bit bit-vector with value zero

val is_bv_uminus : Expr.expr -> bool

Indicates whether the term is a bit-vector unary minus

val is_bv_add : Expr.expr -> bool

Indicates whether the term is a bit-vector addition (binary)

val is_bv_sub : Expr.expr -> bool

Indicates whether the term is a bit-vector subtraction (binary)

val is_bv_mul : Expr.expr -> bool

Indicates whether the term is a bit-vector multiplication (binary)

val is_bv_sdiv : Expr.expr -> bool

Indicates whether the term is a bit-vector signed division (binary)

val is_bv_udiv : Expr.expr -> bool

Indicates whether the term is a bit-vector unsigned division (binary)

val is_bv_SRem : Expr.expr -> bool

Indicates whether the term is a bit-vector signed remainder (binary)

val is_bv_urem : Expr.expr -> bool

Indicates whether the term is a bit-vector unsigned remainder (binary)

val is_bv_smod : Expr.expr -> bool

Indicates whether the term is a bit-vector signed modulus

val is_bv_sdiv0 : Expr.expr -> bool

Indicates whether the term is a bit-vector signed division by zero

val is_bv_udiv0 : Expr.expr -> bool

Indicates whether the term is a bit-vector unsigned division by zero

val is_bv_srem0 : Expr.expr -> bool

Indicates whether the term is a bit-vector signed remainder by zero

val is_bv_urem0 : Expr.expr -> bool

Indicates whether the term is a bit-vector unsigned remainder by zero

val is_bv_smod0 : Expr.expr -> bool

Indicates whether the term is a bit-vector signed modulus by zero

val is_bv_ule : Expr.expr -> bool

Indicates whether the term is an unsigned bit-vector less-than-or-equal

val is_bv_sle : Expr.expr -> bool

Indicates whether the term is a signed bit-vector less-than-or-equal

val is_bv_uge : Expr.expr -> bool

Indicates whether the term is an unsigned bit-vector greater-than-or-equal

val is_bv_sge : Expr.expr -> bool

Indicates whether the term is a signed bit-vector greater-than-or-equal

val is_bv_ult : Expr.expr -> bool

Indicates whether the term is an unsigned bit-vector less-than

val is_bv_slt : Expr.expr -> bool

Indicates whether the term is a signed bit-vector less-than

val is_bv_ugt : Expr.expr -> bool

Indicates whether the term is an unsigned bit-vector greater-than

val is_bv_sgt : Expr.expr -> bool

Indicates whether the term is a signed bit-vector greater-than

val is_bv_and : Expr.expr -> bool

Indicates whether the term is a bit-wise AND

val is_bv_or : Expr.expr -> bool

Indicates whether the term is a bit-wise OR

val is_bv_not : Expr.expr -> bool

Indicates whether the term is a bit-wise NOT

val is_bv_xor : Expr.expr -> bool

Indicates whether the term is a bit-wise XOR

val is_bv_nand : Expr.expr -> bool

Indicates whether the term is a bit-wise NAND

val is_bv_nor : Expr.expr -> bool

Indicates whether the term is a bit-wise NOR

val is_bv_xnor : Expr.expr -> bool

Indicates whether the term is a bit-wise XNOR

val is_bv_concat : Expr.expr -> bool

Indicates whether the term is a bit-vector concatenation (binary)

val is_bv_signextension : Expr.expr -> bool

Indicates whether the term is a bit-vector sign extension

val is_bv_zeroextension : Expr.expr -> bool

Indicates whether the term is a bit-vector zero extension

val is_bv_extract : Expr.expr -> bool

Indicates whether the term is a bit-vector extraction

val is_bv_repeat : Expr.expr -> bool

Indicates whether the term is a bit-vector repetition

val is_bv_reduceor : Expr.expr -> bool

Indicates whether the term is a bit-vector reduce OR

val is_bv_reduceand : Expr.expr -> bool

Indicates whether the term is a bit-vector reduce AND

val is_bv_comp : Expr.expr -> bool

Indicates whether the term is a bit-vector comparison

val is_bv_shiftleft : Expr.expr -> bool

Indicates whether the term is a bit-vector shift left

val is_bv_shiftrightlogical : Expr.expr -> bool

Indicates whether the term is a bit-vector logical shift right

val is_bv_shiftrightarithmetic : Expr.expr -> bool

Indicates whether the term is a bit-vector arithmetic shift left

val is_bv_rotateleft : Expr.expr -> bool

Indicates whether the term is a bit-vector rotate left

val is_bv_rotateright : Expr.expr -> bool

Indicates whether the term is a bit-vector rotate right

val is_bv_rotateleftextended : Expr.expr -> bool

Indicates whether the term is a bit-vector rotate left (extended) Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one.

val is_bv_rotaterightextended : Expr.expr -> bool

Indicates whether the term is a bit-vector rotate right (extended) Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one.

val is_int2bv : Expr.expr -> bool

Indicates whether the term is a coercion from bit-vector to integer This function is not supported by the decision procedures. Only the most rudimentary simplification rules are applied to this function.

val is_bv2int : Expr.expr -> bool

Indicates whether the term is a coercion from integer to bit-vector This function is not supported by the decision procedures. Only the most rudimentary simplification rules are applied to this function.

val is_bv_carry : Expr.expr -> bool

Indicates whether the term is a bit-vector carry Compute the carry bit in a full-adder. The meaning is given by the equivalence (carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3)))

val is_bv_xor3 : Expr.expr -> bool

Indicates whether the term is a bit-vector ternary XOR The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3)

val get_size : Sort.sort -> int

The size of a bit-vector sort.

val get_int : Expr.expr -> int

Retrieve the int value.

val numeral_to_string : Expr.expr -> string

Returns a string representation of a numeral.

val mk_const : context -> Symbol.symbol -> int -> Expr.expr

Creates a bit-vector constant.

val mk_const_s : context -> string -> int -> Expr.expr

Creates a bit-vector constant.

val mk_not : context -> Expr.expr -> Expr.expr

Bitwise negation. The argument must have a bit-vector sort.

val mk_redand : context -> Expr.expr -> Expr.expr

Take conjunction of bits in a vector,vector of length 1. The argument must have a bit-vector sort.

val mk_redor : context -> Expr.expr -> Expr.expr

Take disjunction of bits in a vector,vector of length 1. The argument must have a bit-vector sort.

val mk_and : context -> Expr.expr -> Expr.expr -> Expr.expr

Bitwise conjunction. The arguments must have a bit-vector sort.

val mk_or : context -> Expr.expr -> Expr.expr -> Expr.expr

Bitwise disjunction. The arguments must have a bit-vector sort.

val mk_xor : context -> Expr.expr -> Expr.expr -> Expr.expr

Bitwise XOR. The arguments must have a bit-vector sort.

val mk_nand : context -> Expr.expr -> Expr.expr -> Expr.expr

Bitwise NAND. The arguments must have a bit-vector sort.

val mk_nor : context -> Expr.expr -> Expr.expr -> Expr.expr

Bitwise NOR. The arguments must have a bit-vector sort.

val mk_xnor : context -> Expr.expr -> Expr.expr -> Expr.expr

Bitwise XNOR. The arguments must have a bit-vector sort.

val mk_neg : context -> Expr.expr -> Expr.expr

Standard two's complement unary minus. The arguments must have a bit-vector sort.

val mk_add : context -> Expr.expr -> Expr.expr -> Expr.expr

Two's complement addition. The arguments must have the same bit-vector sort.

val mk_sub : context -> Expr.expr -> Expr.expr -> Expr.expr

Two's complement subtraction. The arguments must have the same bit-vector sort.

val mk_mul : context -> Expr.expr -> Expr.expr -> Expr.expr

Two's complement multiplication. The arguments must have the same bit-vector sort.

val mk_udiv : context -> Expr.expr -> Expr.expr -> Expr.expr

Unsigned division.

It is defined as the floor of t1/t2 if \c t2 is different from zero. If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.

val mk_sdiv : context -> Expr.expr -> Expr.expr -> Expr.expr

Signed division.

It is defined in the following way:

The \c floor of t1/t2 if \c t2 is different from zero, and t1*t2 >= 0.

The \c ceiling of t1/t2 if \c t2 is different from zero, and t1*t2 < 0.

If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.

val mk_urem : context -> Expr.expr -> Expr.expr -> Expr.expr

Unsigned remainder.

It is defined as t1 - (t1 /u t2) * t2, where /u represents unsigned division. If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.

val mk_srem : context -> Expr.expr -> Expr.expr -> Expr.expr

Signed remainder.

It is defined as t1 - (t1 /s t2) * t2, where /s represents signed division. The most significant bit (sign) of the result is equal to the most significant bit of \c t1.

If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.

val mk_smod : context -> Expr.expr -> Expr.expr -> Expr.expr

Two's complement signed remainder (sign follows divisor).

If t2 is zero, then the result is undefined. The arguments must have the same bit-vector sort.

val mk_ult : context -> Expr.expr -> Expr.expr -> Expr.expr

Unsigned less-than

The arguments must have the same bit-vector sort.

val mk_slt : context -> Expr.expr -> Expr.expr -> Expr.expr

Two's complement signed less-than

The arguments must have the same bit-vector sort.

val mk_ule : context -> Expr.expr -> Expr.expr -> Expr.expr

Unsigned less-than or equal to.

The arguments must have the same bit-vector sort.

val mk_sle : context -> Expr.expr -> Expr.expr -> Expr.expr

Two's complement signed less-than or equal to.

The arguments must have the same bit-vector sort.

val mk_uge : context -> Expr.expr -> Expr.expr -> Expr.expr

Unsigned greater than or equal to.

The arguments must have the same bit-vector sort.

val mk_sge : context -> Expr.expr -> Expr.expr -> Expr.expr

Two's complement signed greater than or equal to.

The arguments must have the same bit-vector sort.

val mk_ugt : context -> Expr.expr -> Expr.expr -> Expr.expr

Unsigned greater-than.

The arguments must have the same bit-vector sort.

val mk_sgt : context -> Expr.expr -> Expr.expr -> Expr.expr

Two's complement signed greater-than.

The arguments must have the same bit-vector sort.

val mk_concat : context -> Expr.expr -> Expr.expr -> Expr.expr

Bit-vector concatenation.

The arguments must have a bit-vector sort.
Returns The result is a bit-vector of size n1+n2, where n1 (n2) is the size of t1 (t2).

val mk_extract : context -> int -> int -> Expr.expr -> Expr.expr

Bit-vector extraction.

Extract the bits between two limits from a bitvector of size m to yield a new bitvector of size n, where n = high - low + 1.

val mk_sign_ext : context -> int -> Expr.expr -> Expr.expr

Bit-vector sign extension.

Sign-extends the given bit-vector to the (signed) equivalent bitvector of size m+i, where \c m is the size of the given bit-vector.

val mk_zero_ext : context -> int -> Expr.expr -> Expr.expr

Bit-vector zero extension.

Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where \c m is the size of the given bit-vector.

val mk_repeat : context -> int -> Expr.expr -> Expr.expr

Bit-vector repetition.

val mk_shl : context -> Expr.expr -> Expr.expr -> Expr.expr

Shift left.

It is equivalent to multiplication by 2^x where \c x is the value of third argument.

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

val mk_lshr : context -> Expr.expr -> Expr.expr -> Expr.expr

Logical shift right

It is equivalent to unsigned division by 2^x where \c x is the value of the third argument.

The arguments must have a bit-vector sort.

val mk_ashr : context -> Expr.expr -> Expr.expr -> Expr.expr

Arithmetic shift right

It is like logical shift right except that the most significant bits of the result always copy the most significant bit of the second argument.

The arguments must have a bit-vector sort.

val mk_rotate_left : context -> int -> Expr.expr -> Expr.expr

Rotate Left. Rotate bits of \c t to the left \c i times.

val mk_rotate_right : context -> int -> Expr.expr -> Expr.expr

Rotate Right. Rotate bits of \c t to the right \c i times.

val mk_ext_rotate_left : context -> Expr.expr -> Expr.expr -> Expr.expr

Rotate Left. Rotate bits of the second argument to the left.

val mk_ext_rotate_right : context -> Expr.expr -> Expr.expr -> Expr.expr

Rotate Right. Rotate bits of the second argument to the right.

val mk_bv2int : context -> Expr.expr -> bool -> Expr.expr

Create an integer from the bit-vector argument

If \c is_signed is false, then the bit-vector \c t1 is treated as unsigned. So the result is non-negative and in the range [0..2^N-1], where N are the number of bits in the argument. If \c is_signed is true, \c t1 is treated as a signed bit-vector.

NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.

val mk_add_no_overflow : context -> Expr.expr -> Expr.expr -> bool -> Expr.expr

Create a predicate that checks that the bit-wise addition does not overflow.