package dolmen

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

include Smtlib_Real with type t := t

include Smtlib_Arith_Common with type t := t

val 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.

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 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 div : t -> t -> t

Real division. See Smtlib theory for a full description.

val is_int : t -> t

Arithmetic predicate, true on reals that are also integers.

val floor_to_int : t -> t

Greatest integer smaller than the given real