M_with_make.Int
val neg : term -> term
neg t constructs the negation of the integer term t.
neg t
t
val to_real : term -> term
to_real t converts the integer term t to a real number term.
to_real t
val to_bv : int -> term -> term
to_bv m t convertes integer t term into a bitvector of size m.
to_bv m t
m
val add : term -> term -> term
add t1 t2 constructs the sum of the integer terms t1 and t2.
add t1 t2
t1
t2
val sub : term -> term -> term
sub t1 t2 constructs the difference of the integer terms t1 and t2.
sub t1 t2
val mul : term -> term -> term
mul t1 t2 constructs the product of the integer terms t1 and t2.
mul t1 t2
val div : term -> term -> term
div t1 t2 constructs the quotient of the integer terms t1 and t2.
div t1 t2
val rem : term -> term -> term
rem t1 t2 constructs the remainder of the integer terms t1 and t2.
rem t1 t2
val mod_ : term -> term -> term
mod t1 t2 constructs the modules operator
mod t1 t2
val pow : term -> term -> term
pow t1 t2 constructs the power of the integer terms t1 and t2.
pow t1 t2
val lt : term -> term -> term
lt t1 t2 constructs the less-than relation between t1 and t2.
lt t1 t2
val le : term -> term -> term
le t1 t2 constructs the less-than-or-equal relation between t1 and t2.
le t1 t2
val gt : term -> term -> term
gt t1 t2 constructs the greater-than relation between t1 and t2.
gt t1 t2
val ge : term -> term -> term
ge t1 t2 constructs the greater-than-or-equal relation between t1 and t2.
ge t1 t2