package smtml

  1. Overview
  2. Docs
package smtml
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module M_with_make.Int

val neg : term -> term

neg t constructs the negation of the integer term t.

val to_real : term -> term

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

val to_bv : int -> term -> term

to_bv m t convertes integer t term into a bitvector of size m.

val add : term -> term -> term

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

val sub : term -> term -> term

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

val mul : term -> term -> term

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

val div : term -> term -> term

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

val rem : term -> term -> term

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

val mod_ : term -> term -> term

mod t1 t2 constructs the modules operator

val pow : term -> term -> term

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

val lt : term -> term -> term

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

val le : term -> term -> term

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

val gt : term -> term -> term

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

val ge : term -> term -> term

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