dolmen_type

A typechecker for automated deduction languages
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library dolmen_type
Module Dolmen_type . Arith . Smtlib2 . Real_Int . Tff . T . Real
include Dolmen.Intf.Term.Smtlib_Real with type t := Type.T.t
include Dolmen.Intf.Term.Smtlib_Arith_Common with type t := Type.T.t
val mk : string -> Type.T.t

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

val minus : Type.T.t -> Type.T.t

Arithmetic unary minus/negation.

val add : Type.T.t -> Type.T.t -> Type.T.t

Arithmetic addition.

val sub : Type.T.t -> Type.T.t -> Type.T.t

Arithmetic substraction

val mul : Type.T.t -> Type.T.t -> Type.T.t

Arithmetic multiplication

val lt : Type.T.t -> Type.T.t -> Type.T.t

Arithmetic "less than" comparison.

val le : Type.T.t -> Type.T.t -> Type.T.t

Arithmetic "less or equal" comparison.

val gt : Type.T.t -> Type.T.t -> Type.T.t

Arithmetic "greater than" comparison.

val ge : Type.T.t -> Type.T.t -> Type.T.t

Arithmetic "greater or equal" comparison.

val div : Type.T.t -> Type.T.t -> Type.T.t

Real division. See Smtlib theory for a full description.

val is_int : Type.T.t -> Type.T.t

Arithmetic predicate, true on reals that are also integers.

val floor_to_int : Type.T.t -> Type.T.t

Greatest integer smaller than the given real