package dolmen

  1. Overview
  2. Docs
package dolmen
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

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

val abs : t -> t

Arithmetic absolute value.

val 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
val div_e : t -> t -> t

Euclidian division quotient

val rem_e : t -> t -> t

Euclidian division remainder

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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct