package dolmen
Legend:
Library
Module
Module type
Parameter
Class
Class type

Real operations

Satisfy the required interface for the typing of smtlib's reals

include Dolmen_intf.Term.Smtlib_Real with type t := t
include Dolmen_intf.Term.Smtlib_Arith_Common with type t := t
val div : t -> t -> t

Real division. See Smtlib theory for a full description.

Satisfy the common interface for TPTP's arithmetic over reals

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

Euclidian division quotient

val div_t : t -> t -> t

Truncation of the rational/real division.

val div_f : t -> t -> t

Floor of the ration/real division.

val rem_e : t -> t -> t

Euclidian division remainder

val rem_t : t -> t -> t

Remainder for the truncation of the rational/real division.

val rem_f : t -> t -> t

Remaidner for the floor of the ration/real division.

val floor : t -> t

Floor function.

val ceiling : t -> t

Ceiling

val truncate : t -> t

Truncation.

val round : t -> t

Rounding to the nearest integer.

val is_int : t -> t

Integer testing

val is_rat : t -> t

Rationality testing.

val to_int : t -> t

Convesion to an integer.

val to_rat : t -> t

Conversion to a rational.

val to_real : t -> t

Conversion to a real.

Satisfy the real part of the SMTLIB's Float requirements

include Dolmen_intf.Term.Smtlib_Float_Real with type t := t
val mk : string -> t

Bitvector litteral.

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

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

Arithmetic unary minus/negation.

val add : t -> t -> t

Arithmetic addition.

val sub : t -> t -> t

Arithmetic substraction

val mul : t -> t -> t

Arithmetic multiplication

val pow : t -> t -> t

Arithmetic exponentiation

val lt : t -> t -> t

Arithmetic "less than" comparison.

val le : t -> t -> t

Arithmetic "less or equal" comparison.

val gt : t -> t -> t

Arithmetic "greater than" comparison.

val ge : t -> t -> t

Arithmetic "greater or equal" comparison.

val floor_to_int : t -> t

Greatest integer smaller than the given real