Module Term.IntSource

Integer operations.

Satisfy the required interface for the typing of smtlib integers.

include Dolmen_intf.Term.Smtlib_Int with type t := t and type cst := term_cst
include Dolmen_intf.Term.Smtlib_Arith_Common with type t := t with type cst := term_cst
Sourceval mk : string -> t

Build a constant. The literal is passed as a string to avoid overflow caused by the limited precision of native number formats.

Sourceval div_zero : term_cst

A symbol used to denote the interpretation of division by zero in a particular model. Has no semantics by itself, and instead is used as index in the environment of model verification.

Sourceval rem_zero : term_cst

A symbol used to denote the interpretation of modulo by zero in a particular model. Has no semantics by itself, and instead is used as index in the environment of model verification.

Sourceval abs : t -> t

Arithmetic absolute value.

Sourceval divisible : string -> t -> t

Arithmetic divisibility predicate. Indexed over constant integers (represented as strings, see int).

Satisfy the common interface for TPTP's arithmetic on integers.

include Dolmen_intf.Term.Tptp_Tff_Arith_Common with type t := t
Sourceval div_e : t -> t -> t

Euclidian division quotient

Sourceval rem_e : t -> t -> t

Euclidian division remainder

Sourceval floor : t -> t

Floor function.

Sourceval ceiling : t -> t

Ceiling

Sourceval truncate : t -> t

Truncation.

Sourceval round : t -> t

Rounding to the nearest integer.

Sourceval is_int : t -> t

Integer testing

Sourceval is_rat : t -> t

Rationality testing.

Sourceval to_int : t -> t

Convesion to an integer.

Sourceval to_rat : t -> t

Conversion to a rational.

Sourceval to_real : t -> t

Conversion to a real.

Satisfy the common interface for Alt-Ergo's arithmetic types.

include Dolmen_intf.Term.Ae_Arith_Common with type t := t
Sourceval minus : t -> t

Arithmetic unary minus/negation.

Sourceval add : t -> t -> t

Arithmetic addition.

Sourceval sub : t -> t -> t

Arithmetic substraction

Sourceval mul : t -> t -> t

Arithmetic multiplication

Sourceval pow : t -> t -> t

Arithmetic exponentiation

Sourceval lt : t -> t -> t

Arithmetic "less than" comparison.

Sourceval le : t -> t -> t

Arithmetic "less or equal" comparison.

Sourceval gt : t -> t -> t

Arithmetic "greater than" comparison.

Sourceval ge : t -> t -> t

Arithmetic "greater or equal" comparison.

Sourceval div : t -> t -> t

Euclidian division quotient

Sourceval div_t : t -> t -> t

Truncation of the rational/real division.

Sourceval div_f : t -> t -> t

Floor of the ration/real division.

Sourceval rem : t -> t -> t

Euclidian division remainder

Sourceval rem_t : t -> t -> t

Remainder for the truncation of the rational/real division.

Sourceval rem_f : t -> t -> t

Remaidner for the floor of the ration/real division.