package smtml

neg t constructs the negation of the integer term t.

to_real t converts the integer term t to a real number term.

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

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

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

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

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

pow t1 t2 constructs the power of the integer terms t1 and t2.

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

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

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

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