package dolmen

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

Satisfy the required interface for typing smtlib floating points.

include Dolmen_intf.Term.Smtlib_Float_Float with type t := t
val fp : t -> t -> t -> t

Construct a floating point from bitvector literals (sign, exponent, significand). The sign should be of size 1.

val roundNearestTiesToEven : t

constant for rounding mode RNE

val roundNearestTiesToAway : t

constant for rounding mode RNA

val roundTowardPositive : t

constant for rounding mode RTP

val roundTowardNegative : t

constant for rounding mode RTN

val roundTowardZero : t

constant for rounding mode RTZ

val plus_infinity : int -> int -> t

The constant plus infinity, it is also equivalent to a literal

val minus_infinity : int -> int -> t

The constant minus infinity, it is also equivalent to a literal

val plus_zero : int -> int -> t

The constant plus zero, it is also equivalent to a literal

val minus_zero : int -> int -> t

The constant minus zero, it is also equivalent to a literal

val nan : int -> int -> t

The constant Non-numbers, it is also equivalent to many literals which are equivalent together

val abs : t -> t

absolute value

val neg : t -> t

negation

val add : t -> t -> t -> t

add rm f1 f2 addition

val sub : t -> t -> t -> t

sub rm f1 f2 subtraction

val mul : t -> t -> t -> t

mul rm f1 f2 multiplication

val div : t -> t -> t -> t

mul rm f1 f2 division

val fma : t -> t -> t -> t -> t

mul rm f1 f2 fused multiplication and addition

val sqrt : t -> t -> t

sqrt rm f square root

val rem : t -> t -> t

rem f1 f2 remainder

val roundToIntegral : t -> t -> t

roundToIntegral rm f rounding to integral

val min : t -> t -> t

min f1 f2 minimum

val max : t -> t -> t

max f1 f2 maximum

val leq : t -> t -> t

leq f1 f2 less or equal floating point comparison

val lt : t -> t -> t

lt f1 f2 less than floating point comparison

val geq : t -> t -> t

geq f1 f2 greater or equal floating point comparison

val gt : t -> t -> t

lt f1 f2 greater than floating point comparison

val eq : t -> t -> t

eq f1 f2 floating point equality

val isNormal : t -> t

isNormal f test if it is a normal floating point

val isSubnormal : t -> t

isSubnormal f test if it is a subnormal floating point

val isZero : t -> t

isZero f test if it is a zero

val isInfinite : t -> t

isInfinite f test if it is an infinite

val isNaN : t -> t

isNaN f test if it is NaN

val isNegative : t -> t

isNegative f test if it is a negative floating point

val isPositive : t -> t

isPositive f test if it is a positive floating point

val ieee_format_to_fp : int -> int -> t -> t

ieee_format_to_fp e s bv Convert a bitvector into a floating point using IEEE 754-2008 interchange format. (reinterpret the bitvector into floating-point)

val to_fp : int -> int -> t -> t -> t

to_fp e s rm f convert from one floating point format to another

val real_to_fp : int -> int -> t -> t -> t

real_to_fp e s rm r convert from a real

val sbv_to_fp : int -> int -> t -> t -> t

sbv_to_fp e s rm bv convert from a signed integer

val ubv_to_fp : int -> int -> t -> t -> t

ubv_to_fp e s rm bv convert from an unsigned integer

val to_ubv : int -> t -> t -> t

to_ubv m rm f convert to an unsigned integer (bitvector of size m)

val to_sbv : int -> t -> t -> t

to_ubv m rm f convert to a signed integer (bitvector of size m)

val to_real : t -> t

to_real f convert to a 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