module BitVector:sig..end
Functions to manipulate bit-vector expressions
val mk_sort : context -> int -> Sort.sortCreate a new bit-vector sort.
val is_bv : Expr.expr -> boolIndicates whether the terms is of bit-vector sort.
val is_bv_numeral : Expr.expr -> boolIndicates whether the term is a bit-vector numeral
val is_bv_bit1 : Expr.expr -> boolIndicates whether the term is a one-bit bit-vector with value one
val is_bv_bit0 : Expr.expr -> boolIndicates whether the term is a one-bit bit-vector with value zero
val is_bv_uminus : Expr.expr -> boolIndicates whether the term is a bit-vector unary minus
val is_bv_add : Expr.expr -> boolIndicates whether the term is a bit-vector addition (binary)
val is_bv_sub : Expr.expr -> boolIndicates whether the term is a bit-vector subtraction (binary)
val is_bv_mul : Expr.expr -> boolIndicates whether the term is a bit-vector multiplication (binary)
val is_bv_sdiv : Expr.expr -> boolIndicates whether the term is a bit-vector signed division (binary)
val is_bv_udiv : Expr.expr -> boolIndicates whether the term is a bit-vector unsigned division (binary)
val is_bv_SRem : Expr.expr -> boolIndicates whether the term is a bit-vector signed remainder (binary)
val is_bv_urem : Expr.expr -> boolIndicates whether the term is a bit-vector unsigned remainder (binary)
val is_bv_smod : Expr.expr -> boolIndicates whether the term is a bit-vector signed modulus
val is_bv_sdiv0 : Expr.expr -> boolIndicates whether the term is a bit-vector signed division by zero
val is_bv_udiv0 : Expr.expr -> boolIndicates whether the term is a bit-vector unsigned division by zero
val is_bv_srem0 : Expr.expr -> boolIndicates whether the term is a bit-vector signed remainder by zero
val is_bv_urem0 : Expr.expr -> boolIndicates whether the term is a bit-vector unsigned remainder by zero
val is_bv_smod0 : Expr.expr -> boolIndicates whether the term is a bit-vector signed modulus by zero
val is_bv_ule : Expr.expr -> boolIndicates whether the term is an unsigned bit-vector less-than-or-equal
val is_bv_sle : Expr.expr -> boolIndicates whether the term is a signed bit-vector less-than-or-equal
val is_bv_uge : Expr.expr -> boolIndicates whether the term is an unsigned bit-vector greater-than-or-equal
val is_bv_sge : Expr.expr -> boolIndicates whether the term is a signed bit-vector greater-than-or-equal
val is_bv_ult : Expr.expr -> boolIndicates whether the term is an unsigned bit-vector less-than
val is_bv_slt : Expr.expr -> boolIndicates whether the term is a signed bit-vector less-than
val is_bv_ugt : Expr.expr -> boolIndicates whether the term is an unsigned bit-vector greater-than
val is_bv_sgt : Expr.expr -> boolIndicates whether the term is a signed bit-vector greater-than
val is_bv_and : Expr.expr -> boolIndicates whether the term is a bit-wise AND
val is_bv_or : Expr.expr -> boolIndicates whether the term is a bit-wise OR
val is_bv_not : Expr.expr -> boolIndicates whether the term is a bit-wise NOT
val is_bv_xor : Expr.expr -> boolIndicates whether the term is a bit-wise XOR
val is_bv_nand : Expr.expr -> boolIndicates whether the term is a bit-wise NAND
val is_bv_nor : Expr.expr -> boolIndicates whether the term is a bit-wise NOR
val is_bv_xnor : Expr.expr -> boolIndicates whether the term is a bit-wise XNOR
val is_bv_concat : Expr.expr -> boolIndicates whether the term is a bit-vector concatenation (binary)
val is_bv_signextension : Expr.expr -> boolIndicates whether the term is a bit-vector sign extension
val is_bv_zeroextension : Expr.expr -> boolIndicates whether the term is a bit-vector zero extension
val is_bv_extract : Expr.expr -> boolIndicates whether the term is a bit-vector extraction
val is_bv_repeat : Expr.expr -> boolIndicates whether the term is a bit-vector repetition
val is_bv_reduceor : Expr.expr -> boolIndicates whether the term is a bit-vector reduce OR
val is_bv_reduceand : Expr.expr -> boolIndicates whether the term is a bit-vector reduce AND
val is_bv_comp : Expr.expr -> boolIndicates whether the term is a bit-vector comparison
val is_bv_shiftleft : Expr.expr -> boolIndicates whether the term is a bit-vector shift left
val is_bv_shiftrightlogical : Expr.expr -> boolIndicates whether the term is a bit-vector logical shift right
val is_bv_shiftrightarithmetic : Expr.expr -> boolIndicates whether the term is a bit-vector arithmetic shift left
val is_bv_rotateleft : Expr.expr -> boolIndicates whether the term is a bit-vector rotate left
val is_bv_rotateright : Expr.expr -> boolIndicates whether the term is a bit-vector rotate right
val is_bv_rotateleftextended : Expr.expr -> boolIndicates 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 -> boolIndicates 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 -> boolIndicates 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 -> boolIndicates 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 -> boolIndicates 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 -> boolIndicates 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 -> intThe size of a bit-vector sort.
val numeral_to_string : Expr.expr -> stringReturns a string representation of a numeral.
val mk_const : context -> Symbol.symbol -> int -> Expr.exprCreates a bit-vector constant.
val mk_const_s : context -> string -> int -> Expr.exprCreates a bit-vector constant.
val mk_not : context -> Expr.expr -> Expr.exprBitwise negation. The argument must have a bit-vector sort.
val mk_redand : context -> Expr.expr -> Expr.exprTake 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.exprTake 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.exprBitwise conjunction. The arguments must have a bit-vector sort.
val mk_or : context -> Expr.expr -> Expr.expr -> Expr.exprBitwise disjunction. The arguments must have a bit-vector sort.
val mk_xor : context -> Expr.expr -> Expr.expr -> Expr.exprBitwise XOR. The arguments must have a bit-vector sort.
val mk_nand : context -> Expr.expr -> Expr.expr -> Expr.exprBitwise NAND. The arguments must have a bit-vector sort.
val mk_nor : context -> Expr.expr -> Expr.expr -> Expr.exprBitwise NOR. The arguments must have a bit-vector sort.
val mk_xnor : context -> Expr.expr -> Expr.expr -> Expr.exprBitwise XNOR. The arguments must have a bit-vector sort.
val mk_neg : context -> Expr.expr -> Expr.exprStandard two's complement unary minus. The arguments must have a bit-vector sort.
val mk_add : context -> Expr.expr -> Expr.expr -> Expr.exprTwo's complement addition. The arguments must have the same bit-vector sort.
val mk_sub : context -> Expr.expr -> Expr.expr -> Expr.exprTwo's complement subtraction. The arguments must have the same bit-vector sort.
val mk_mul : context -> Expr.expr -> Expr.expr -> Expr.exprTwo's complement multiplication. The arguments must have the same bit-vector sort.
val mk_udiv : context -> Expr.expr -> Expr.expr -> Expr.exprUnsigned 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 not uniquely specified. It can be set to any value
that satisfies the constraints where unsigned division is used.
The arguments must have the same bit-vector sort.
val mk_sdiv : context -> Expr.expr -> Expr.expr -> Expr.exprSigned division.
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.If t2 is zero, then the result is is not uniquely specified.
It can be set to any value that satisfies the constraints
where signed division is used.
The arguments must have the same bit-vector sort.
val mk_urem : context -> Expr.expr -> Expr.expr -> Expr.exprUnsigned remainder.
It is defined as t1 - (t1 /u t2) * t2, where /u represents unsigned division.
If t2 is zero, then the result is not uniquely specified.
It can be set to any value that satisfies the constraints
where unsigned remainder is used.
The arguments must have the same bit-vector sort.
val mk_srem : context -> Expr.expr -> Expr.expr -> Expr.exprSigned 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 not uniquely specified.
It can be set to any value that satisfies the constraints
where signed remainder is used.
The arguments must have the same bit-vector sort.
val mk_smod : context -> Expr.expr -> Expr.expr -> Expr.exprTwo's complement signed remainder (sign follows divisor).
If t2 is zero, then the result is not uniquely specified.
It can be set to any value that satisfies the constraints
where two's complement signed remainder is used.
The arguments must have the same bit-vector sort.
val mk_ult : context -> Expr.expr -> Expr.expr -> Expr.exprUnsigned less-than
The arguments must have the same bit-vector sort.
val mk_slt : context -> Expr.expr -> Expr.expr -> Expr.exprTwo's complement signed less-than
The arguments must have the same bit-vector sort.
val mk_ule : context -> Expr.expr -> Expr.expr -> Expr.exprUnsigned less-than or equal to.
The arguments must have the same bit-vector sort.
val mk_sle : context -> Expr.expr -> Expr.expr -> Expr.exprTwo'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.exprUnsigned greater than or equal to.
The arguments must have the same bit-vector sort.
val mk_sge : context -> Expr.expr -> Expr.expr -> Expr.exprTwo'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.exprUnsigned greater-than.
The arguments must have the same bit-vector sort.
val mk_sgt : context -> Expr.expr -> Expr.expr -> Expr.exprTwo's complement signed greater-than.
The arguments must have the same bit-vector sort.
val mk_concat : context -> Expr.expr -> Expr.expr -> Expr.exprBit-vector concatenation.
The arguments must have a bit-vector sort.
n1+n2, where n1 (n2)
is the size of t1 (t2).val mk_extract : context -> int -> int -> Expr.expr -> Expr.exprBit-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.exprBit-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.exprBit-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.exprBit-vector repetition.
val mk_shl : context -> Expr.expr -> Expr.expr -> Expr.exprShift 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.exprLogical shift right
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.exprArithmetic 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.
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.exprRotate Left. Rotate bits of \c t to the left \c i times.
val mk_rotate_right : context -> int -> Expr.expr -> Expr.exprRotate Right. Rotate bits of \c t to the right \c i times.
val mk_ext_rotate_left : context -> Expr.expr -> Expr.expr -> Expr.exprRotate Left. Rotate bits of the second argument to the left.
val mk_ext_rotate_right : context -> Expr.expr -> Expr.expr -> Expr.exprRotate Right. Rotate bits of the second argument to the right.
val mk_bv2int : context -> Expr.expr -> bool -> Expr.exprCreate 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.exprCreate a predicate that checks that the bit-wise addition does not overflow.
The arguments must be of bit-vector sort.
val mk_add_no_underflow : context -> Expr.expr -> Expr.expr -> Expr.exprCreate a predicate that checks that the bit-wise addition does not underflow.
The arguments must be of bit-vector sort.
val mk_sub_no_overflow : context -> Expr.expr -> Expr.expr -> Expr.exprCreate a predicate that checks that the bit-wise subtraction does not overflow.
The arguments must be of bit-vector sort.
val mk_sub_no_underflow : context -> Expr.expr -> Expr.expr -> bool -> Expr.exprCreate a predicate that checks that the bit-wise subtraction does not underflow.
The arguments must be of bit-vector sort.
val mk_sdiv_no_overflow : context -> Expr.expr -> Expr.expr -> Expr.exprCreate a predicate that checks that the bit-wise signed division does not overflow.
The arguments must be of bit-vector sort.
val mk_neg_no_overflow : context -> Expr.expr -> Expr.exprCreate a predicate that checks that the bit-wise negation does not overflow.
The arguments must be of bit-vector sort.
val mk_mul_no_overflow : context -> Expr.expr -> Expr.expr -> bool -> Expr.exprCreate a predicate that checks that the bit-wise multiplication does not overflow.
The arguments must be of bit-vector sort.
val mk_mul_no_underflow : context -> Expr.expr -> Expr.expr -> Expr.exprCreate a predicate that checks that the bit-wise multiplication does not underflow.
The arguments must be of bit-vector sort.
val mk_numeral : context -> string -> int -> Expr.exprCreate a bit-vector numeral.