package dolmen

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

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
include Dolmen_intf.Term.Smtlib_Arith_Common with type t := t
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 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 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 div_e : t -> t -> t

Euclidian division quotient

Sourceval rem_e : t -> t -> t

Euclidian division remainder

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

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.

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