package smtml

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

Module Mappings.IntSource

Sourceval neg : term -> term

neg t constructs the negation of the integer term t.

Sourceval to_real : term -> term

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

Sourceval to_bv : int -> term -> term

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

Sourceval add : term -> term -> term

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

Sourceval sub : term -> term -> term

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

Sourceval mul : term -> term -> term

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

Sourceval div : term -> term -> term

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

Sourceval rem : term -> term -> term

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

Sourceval mod_ : term -> term -> term

mod t1 t2 constructs the modules operator

Sourceval pow : term -> term -> term

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

Sourceval lt : term -> term -> term

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

Sourceval le : term -> term -> term

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

Sourceval gt : term -> term -> term

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

Sourceval ge : term -> term -> term

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