module BitVector:sig
..end
val mk_sort : context -> int -> Sort.sort
val is_bv : Expr.expr -> bool
val is_bv_numeral : Expr.expr -> bool
val is_bv_bit1 : Expr.expr -> bool
val is_bv_bit0 : Expr.expr -> bool
val is_bv_uminus : Expr.expr -> bool
val is_bv_add : Expr.expr -> bool
val is_bv_sub : Expr.expr -> bool
val is_bv_mul : Expr.expr -> bool
val is_bv_sdiv : Expr.expr -> bool
val is_bv_udiv : Expr.expr -> bool
val is_bv_SRem : Expr.expr -> bool
val is_bv_urem : Expr.expr -> bool
val is_bv_smod : Expr.expr -> bool
val is_bv_sdiv0 : Expr.expr -> bool
val is_bv_udiv0 : Expr.expr -> bool
val is_bv_srem0 : Expr.expr -> bool
val is_bv_urem0 : Expr.expr -> bool
val is_bv_smod0 : Expr.expr -> bool
val is_bv_ule : Expr.expr -> bool
val is_bv_sle : Expr.expr -> bool
val is_bv_uge : Expr.expr -> bool
val is_bv_sge : Expr.expr -> bool
val is_bv_ult : Expr.expr -> bool
val is_bv_slt : Expr.expr -> bool
val is_bv_ugt : Expr.expr -> bool
val is_bv_sgt : Expr.expr -> bool
val is_bv_and : Expr.expr -> bool
val is_bv_or : Expr.expr -> bool
val is_bv_not : Expr.expr -> bool
val is_bv_xor : Expr.expr -> bool
val is_bv_nand : Expr.expr -> bool
val is_bv_nor : Expr.expr -> bool
val is_bv_xnor : Expr.expr -> bool
val is_bv_concat : Expr.expr -> bool
val is_bv_signextension : Expr.expr -> bool
val is_bv_zeroextension : Expr.expr -> bool
val is_bv_extract : Expr.expr -> bool
val is_bv_repeat : Expr.expr -> bool
val is_bv_reduceor : Expr.expr -> bool
val is_bv_reduceand : Expr.expr -> bool
val is_bv_comp : Expr.expr -> bool
val is_bv_shiftleft : Expr.expr -> bool
val is_bv_shiftrightlogical : Expr.expr -> bool
val is_bv_shiftrightarithmetic : Expr.expr -> bool
val is_bv_rotateleft : Expr.expr -> bool
val is_bv_rotateright : Expr.expr -> bool
val is_bv_rotateleftextended : Expr.expr -> bool
val is_bv_rotaterightextended : Expr.expr -> bool
val is_int2bv : Expr.expr -> bool
val is_bv2int : Expr.expr -> bool
val is_bv_carry : Expr.expr -> bool
val is_bv_xor3 : Expr.expr -> bool
val get_size : Sort.sort -> int
val get_int : Expr.expr -> int
val numeral_to_string : Expr.expr -> string
val mk_const : context -> Symbol.symbol -> int -> Expr.expr
val mk_const_s : context -> string -> int -> Expr.expr
val mk_not : context -> Expr.expr -> Expr.expr
val mk_redand : context -> Expr.expr -> Expr.expr
val mk_redor : context -> Expr.expr -> Expr.expr
val mk_and : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_or : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_xor : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_nand : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_nor : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_xnor : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_neg : context -> Expr.expr -> Expr.expr
val mk_add : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_sub : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_mul : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_udiv : context -> Expr.expr -> Expr.expr -> Expr.expr
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
It is defined in the following way:
t1/t2
if \c t2 is different from zero, and t1*t2 >= 0
.t1/t2
if \c t2 is different from zero, and t1*t2 < 0
.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
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
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
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
The arguments must have the same bit-vector sort.
val mk_slt : context -> Expr.expr -> Expr.expr -> Expr.expr
The arguments must have the same bit-vector sort.
val mk_ule : context -> Expr.expr -> Expr.expr -> Expr.expr
The arguments must have the same bit-vector sort.
val mk_sle : context -> Expr.expr -> Expr.expr -> Expr.expr
The arguments must have the same bit-vector sort.
val mk_uge : context -> Expr.expr -> Expr.expr -> Expr.expr
The arguments must have the same bit-vector sort.
val mk_sge : context -> Expr.expr -> Expr.expr -> Expr.expr
The arguments must have the same bit-vector sort.
val mk_ugt : context -> Expr.expr -> Expr.expr -> Expr.expr
The arguments must have the same bit-vector sort.
val mk_sgt : context -> Expr.expr -> Expr.expr -> Expr.expr
The arguments must have the same bit-vector sort.
val mk_concat : context -> Expr.expr -> Expr.expr -> Expr.expr
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
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
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
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
val mk_shl : context -> Expr.expr -> Expr.expr -> Expr.expr
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
It is equivalent to unsigned division by 2^x
where \c x is the value of the 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.
The arguments must have a bit-vector sort.
val mk_ashr : context -> Expr.expr -> Expr.expr -> Expr.expr
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.
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.
The arguments must have a bit-vector sort.
val mk_rotate_left : context -> int -> Expr.expr -> Expr.expr
val mk_rotate_right : context -> int -> Expr.expr -> Expr.expr
val mk_ext_rotate_left : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_ext_rotate_right : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_bv2int : context -> Expr.expr -> bool -> Expr.expr
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
The arguments must be of bit-vector sort.
val mk_add_no_underflow : context -> Expr.expr -> Expr.expr -> Expr.expr
The arguments must be of bit-vector sort.
val mk_sub_no_overflow : context -> Expr.expr -> Expr.expr -> Expr.expr
The arguments must be of bit-vector sort.
val mk_sub_no_underflow : context -> Expr.expr -> Expr.expr -> bool -> Expr.expr
The arguments must be of bit-vector sort.
val mk_sdiv_no_overflow : context -> Expr.expr -> Expr.expr -> Expr.expr
The arguments must be of bit-vector sort.
val mk_neg_no_overflow : context -> Expr.expr -> Expr.expr
The arguments must be of bit-vector sort.
val mk_mul_no_overflow : context -> Expr.expr -> Expr.expr -> bool -> Expr.expr
The arguments must be of bit-vector sort.
val mk_mul_no_underflow : context -> Expr.expr -> Expr.expr -> Expr.expr
The arguments must be of bit-vector sort.
val mk_numeral : context -> string -> int -> Expr.expr