package dolmen

  1. Overview
  2. Docs
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 and type cst := term_cst
include Dolmen_intf.Term.Smtlib_Arith_Common with type t := t with type cst := term_cst
val div' : term_cst

Constant for the division.

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

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