package dolmen

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

Module Term.RealSource

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
Sourceval div' : term_cst

Constant for the division.

Sourceval 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
Sourceval div_e : 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_e : 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.

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.

Satisfy the real part of the SMTLIB's Float requirements

include Dolmen_intf.Term.Smtlib_Float_Real with type t := t
Sourceval 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
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 pow : t -> t -> t

Arithmetic exponentiation

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