Module M.Bitv

v s n constructs a bitvector term from the string s of width n.

neg t constructs the negation of the bitvector term t.

lognot t constructs the bitwise NOT of the bitvector term t.

to_int ~signed t convertes the bitvector term t into an integer.

add t1 t2 constructs the sum of the bitvector terms t1 and t2.

sub t1 t2 constructs the difference of the bitvector terms t1 and t2.

mul t1 t2 constructs the product of the bitvector terms t1 and t2.

div t1 t2 constructs the quotient of the bitvector terms t1 and t2.

div_u t1 t2 constructs the unsigned quotient of the bitvector terms t1 and t2.

logor t1 t2 constructs the bitwise OR of the bitvector terms t1 and t2.

logand t1 t2 constructs the bitwise AND of the bitvector terms t1 and t2.

logxor t1 t2 constructs the bitwise XOR of the bitvector terms t1 and t2.

shl t1 t2 constructs the left shift of t1 by t2.

ashr t1 t2 constructs the arithmetic right shift of t1 by t2.

lshr t1 t2 constructs the logical right shift of t1 by t2.

smod t1 t2 two's complement signed remainder (sign follows divisor).

rem t1 t2 constructs the remainder of the bitvector terms t1 and t2.

rem_u t1 t2 constructs the unsigned remainder of the bitvector terms t1 and t2.

rotate_left t1 t2 constructs the left rotation of t1 by t2.

rotate_right t1 t2 constructs the right rotation of t1 by t2.

nego t constructs a predicate that checks that whether the bit-wise negation of t does not overflow.

addo ~signed t1 t2 constructs a predicate that checks whether the bitwise addition of t1 and t2 does not overflow.

The signed argument is a boolean:

• true -> for signed addition
• false -> for unsigned addition

subo ~signed t1 t2 constructs a predicate that checks whether the bitwise subtraction of t1 and t2 does not overflow.

The signed argument is a boolean:

• true -> for signed subtraction
• false -> for unsigned subtraction

mulo ~signed t1 t2 constructs a predicate that checks whether the bitwise multiplication of t1 and t2 does not overflow.

The signed argument is a boolean:

• true -> for signed multiplication
• false -> for unsigned multiplication

divo t1 t2 constructs a predicate that checks whether the bitwise division of t1 and t2 does not overflow.

lt t1 t2 constructs the less-than relation between bitvector terms t1 and t2.

lt_u t1 t2 constructs the unsigned less-than relation between bitvector terms t1 and t2.

le t1 t2 constructs the less-than-or-equal relation between bitvector terms t1 and t2.

le_u t1 t2 constructs the unsigned less-than-or-equal relation between bitvector terms t1 and t2.

gt t1 t2 constructs the greater-than relation between bitvector terms t1 and t2.

gt_u t1 t2 constructs the unsigned greater-than relation between bitvector terms t1 and t2.

ge t1 t2 constructs the greater-than-or-equal relation between bitvector terms t1 and t2.

ge_u t1 t2 constructs the unsigned greater-than-or-equal relation between bitvector terms t1 and t2.

concat t1 t2 constructs the concatenation of the bitvector terms t1 and t2.

extract t ~high ~low extracts a bit range from t between high and low.

zero_extend n t zero-extends the bitvector term t by n bits.

sign_extend n t sign-extends the bitvector term t by n bits.