package dolmen

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

Module Term.FloatSource

Satisfy the required interface for typing smtlib floating points.

include Dolmen_intf.Term.Smtlib_Float_Float with type t := t and type cst := term_cst
Sourceval fp : t -> t -> t -> t

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

Sourceval roundNearestTiesToEven : t

constant for rounding mode RNE

Sourceval roundNearestTiesToAway : t

constant for rounding mode RNA

Sourceval roundTowardPositive : t

constant for rounding mode RTP

Sourceval roundTowardNegative : t

constant for rounding mode RTN

Sourceval roundTowardZero : t

constant for rounding mode RTZ

Sourceval plus_infinity : int -> int -> t

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

Sourceval minus_infinity : int -> int -> t

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

Sourceval plus_zero : int -> int -> t

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

Sourceval minus_zero : int -> int -> t

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

Sourceval nan : int -> int -> t

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

Sourceval abs : t -> t

absolute value

Sourceval neg : t -> t

negation

Sourceval add : t -> t -> t -> t

add rm f1 f2 addition

Sourceval sub : t -> t -> t -> t

sub rm f1 f2 subtraction

Sourceval mul : t -> t -> t -> t

mul rm f1 f2 multiplication

Sourceval div : t -> t -> t -> t

mul rm f1 f2 division

Sourceval fma : t -> t -> t -> t -> t

mul rm f1 f2 fused multiplication and addition

Sourceval sqrt : t -> t -> t

sqrt rm f square root

Sourceval rem : t -> t -> t

rem f1 f2 remainder

Sourceval roundToIntegral : t -> t -> t

roundToIntegral rm f rounding to integral

Sourceval min : t -> t -> t

min f1 f2 minimum

Sourceval min' : (int * int) -> term_cst

Constant for float min.

Sourceval max : t -> t -> t

max f1 f2 maximum

Sourceval max' : (int * int) -> term_cst

Constant for float max.

Sourceval leq : t -> t -> t

leq f1 f2 less or equal floating point comparison

Sourceval lt : t -> t -> t

lt f1 f2 less than floating point comparison

Sourceval geq : t -> t -> t

geq f1 f2 greater or equal floating point comparison

Sourceval gt : t -> t -> t

lt f1 f2 greater than floating point comparison

Sourceval eq : t -> t -> t

eq f1 f2 floating point equality

Sourceval isNormal : t -> t

isNormal f test if it is a normal floating point

Sourceval isSubnormal : t -> t

isSubnormal f test if it is a subnormal floating point

Sourceval isZero : t -> t

isZero f test if it is a zero

Sourceval isInfinite : t -> t

isInfinite f test if it is an infinite

Sourceval isNaN : t -> t

isNaN f test if it is NaN

Sourceval isNegative : t -> t

isNegative f test if it is a negative floating point

Sourceval isPositive : t -> t

isPositive f test if it is a positive floating point

Sourceval 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)

Sourceval to_fp : int -> int -> t -> t -> t

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

Sourceval real_to_fp : int -> int -> t -> t -> t

real_to_fp e s rm r convert from a real

Sourceval sbv_to_fp : int -> int -> t -> t -> t

sbv_to_fp e s rm bv convert from a signed integer

Sourceval ubv_to_fp : int -> int -> t -> t -> t

ubv_to_fp e s rm bv convert from an unsigned integer

Sourceval to_ubv : int -> t -> t -> t

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

Sourceval to_ubv' : int -> (int * int) -> term_cst

constant for to_ubv

Sourceval to_sbv : int -> t -> t -> t

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

Sourceval to_sbv' : int -> (int * int) -> term_cst

constant for to_sbv

Sourceval 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