package smtml

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.

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.

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.

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.