"/>

Module Term.Fp

Floating-point

type t = fp term

A floating-point term.

val pos_zero : fp sort -> t

pos_zero sort create a floating-point positive zero value (SMT-LIB: +zero).

parameter sort

The sort of the value.

returns

A term representing the floating-point positive zero value of given floating-point sort.

val neg_zero : fp sort -> t

neg_zero sort create a floating-point negative zero value (SMT-LIB: -zero).

parameter sort

The sort of the value.

returns

A term representing the floating-point negative zero value of given floating-point sort.

val pos_inf : fp sort -> t

pos_inf sort create a floating-point positive infinity value (SMT-LIB: +oo).

parameter sort

The sort of the value.

returns

A term representing the floating-point positive infinity value of given floating-point sort.

val neg_inf : fp sort -> t

neg_inf sort create a floating-point negative infinity value (SMT-LIB: -oo).

parameter sort

The sort of the value.

returns

A term representing the floating-point negative infinity value of given floating-point sort.

val nan : fp sort -> t

nan sort create a floating-point NaN value.

parameter sort

The sort of the value.

returns

A term representing the floating-point NaN value of given floating-point sort.

val of_float : fp sort -> rm term Rm.operator -> float -> t

of_float sort rm value create a floating-point value from its float representation, with respect to given rounding mode.

parameter sort

The sort of the value.

parameter rm

The rounding mode.

parameter value

The floating-point value.

returns

A term representing the floating-point value of given sort.

val of_real : fp sort -> rm term Rm.operator -> string -> t

of_real sort rm real create a floating-point value from its real representation, given as a decimal string, with respect to given rounding mode.

parameter sort

The sort of the value.

parameter rm

The rounding mode.

parameter real

The decimal string representing a real value.

returns

A term representing the floating-point value of given sort.

val of_rational : fp sort -> rm term Rm.operator -> num:string -> den:string -> t

from_rational sort rm num den create a floating-point value from its rational representation, given as a two decimal strings representing the numerator and denominator, with respect to given rounding mode.

parameter sort

The sort of the value.

parameter rm

The rounding mode.

parameter num

The decimal string representing the numerator.

parameter den

The decimal string representing the denominator.

returns

A term representing the floating-point value of given sort.

type ieee_754 = private {
sign : bv term;
exponent : bv term;
significand : bv term;
}

Floating-point IEEE 754 representation.

type (!'a, !'b, !'c) operator =
| Abs : (t -> t, t, fp) operator

Floating-point absolute value.

SMT-LIB: fp.abs

| Add : (rm term -> t -> t -> t, rm term * t * t, fp) operator

Floating-point addition.

SMT-LIB: fp.add

| Div : (rm term -> t -> t -> t, rm term * t * t, fp) operator

Floating-point division.

SMT-LIB: fp.div

| Eq : (t -> t -> bv term, t * t, bv) operator

Floating-point equality.

SMT-LIB: fp.eq

| Fma : (rm term -> t -> t -> t -> t, rm term * t * t * t, fp) operator

Floating-point fused multiplcation and addition.

SMT-LIB: fp.fma

| Fp : (sign:bv term -> exponent:bv term -> bv term -> t, ieee_754, fp) operator

Floating-point IEEE 754 value.

SMT-LIB: fp

| Geq : (t -> t -> bv term, t * t, bv) operator

Floating-point greater than or equal.

SMT-LIB: fp.geq

| Gt : (t -> t -> bv term, t * t, bv) operator

Floating-point greater than.

SMT-LIB: fp.gt

| Is_inf : (t -> bv term, t, bv) operator

Floating-point is infinity tester.

SMT-LIB: fp.isInfinite

| Is_nan : (t -> bv term, t, bv) operator

Floating-point is Nan tester.

SMT-LIB: fp.isNaN

| Is_neg : (t -> bv term, t, bv) operator

Floating-point is negative tester.

SMT-LIB: fp.isNegative

| Is_normal : (t -> bv term, t, bv) operator

Floating-point is normal tester.

SMT-LIB: fp.isNormal

| Is_pos : (t -> bv term, t, bv) operator

Floating-point is positive tester.

SMT-LIB: fp.isPositive

| Is_subnormal : (t -> bv term, t, bv) operator

Floating-point is subnormal tester.

SMT-LIB: fp.isSubnormal

| Is_zero : (t -> bv term, t, bv) operator

Floating-point is zero tester.

SMT-LIB: fp.isZero

| Leq : (t -> t -> bv term, t * t, bv) operator

Floating-point less than or equal.

SMT-LIB: fp.leq

| Lt : (t -> t -> bv term, t * t, bv) operator

Floating-point less than.

SMT-LIB: fp.lt

| Max : (t -> t -> t, t * t, fp) operator

Floating-point max.

SMT-LIB: fp.max

| Min : (t -> t -> t, t * t, fp) operator

Floating-point min.

SMT-LIB: fp.min

| Mul : (rm term -> t -> t -> t, rm term * t * t, fp) operator

Floating-point multiplcation.

SMT-LIB: fp.mul

| Neg : (t -> t, t, fp) operator

Floating-point negation.

SMT-LIB: fp.neg

| Rem : (t -> t -> t, t * t, fp) operator

Floating-point remainder.

SMT-LIB: fp.rem

| Rti : (rm term -> t -> t, rm term * t, fp) operator

Floating-point round to integral.

SMT-LIB: fp.roundToIntegral

| Sqrt : (rm term -> t -> t, rm term * t, fp) operator

Floating-point round to square root.

SMT-LIB: fp.sqrt

| Sub : (rm term -> t -> t -> t, rm term * t * t, fp) operator

Floating-point round to subtraction.

SMT-LIB: fp.sqrt

| From_bv : (exponent:int -> int -> bv term -> t, int * int * bv term, fp) operator

Floating-point to_fp from IEEE 754 bit-vector.

SMT-LIB: to_fp (indexed)

| From_fp : (exponent:int -> int -> rm term -> t -> t, int * int * rm term * t, fp) operator

Floating-point to_fp from floating-point.

SMT-LIB: to_fp (indexed)

| From_sbv : (exponent:int -> int -> rm term -> bv term -> t, int * int * rm term * bv term, fp) operator

Floating-point to_fp from signed bit-vector value.

SMT-LIB: to_fp (indexed)

| From_ubv : (exponent:int -> int -> rm term -> bv term -> t, int * int * rm term * bv term, fp) operator

Floating-point to_fp from unsigned bit-vector value.

SMT-LIB: to_fp_unsigned (indexed)

| To_sbv : (int -> rm term -> t -> bv term, int * rm term * t, bv) operator

Floating-point to_sbv.

SMT-LIB: fp.to_sbv (indexed)

| To_ubv : (int -> rm term -> t -> bv term, int * rm term * t, bv) operator

Floating-point to_ubv.

SMT-LIB: fp.to_ubv (indexed)

The term operator.

val term : ('a, 'b, 'c) operator -> 'a

term op .. create a floating-point term constructor of given kind.

parameter op

The operator kind.

returns

A function to build a term representing an operation of given kind.

val make : sign:bv term -> exponent:bv term -> bv term -> t

make ~sign ~exponent significand create a floating-point value from its IEEE 754 standard representation given as three bitvectors representing the sign bit, the exponent and the significand.

parameter sign

The sign bit.

parameter exponent

The exponent bit-vector.

parameter significand

The significand bit-vector.

returns

A term representing the floating-point value.

val of_sbv : exponent:int -> int -> rm term -> bv term -> t

of_sbv ~exponent size rm t create a floatingt-point to_fp from signed bit-vector value.

parameter exponent

The size of the exponent.

parameter size

The total size of the floating-point.

parameter rm

The rounding-mode.

parameter t

The bit-vector term.

returns

SMT-LIB: to_fp (indexed)

val of_ubv : exponent:int -> int -> rm term -> bv term -> t

of_ubv ~exponent size rm t create a floatingt-point to_fp from unsigned bit-vector value.

parameter exponent

The size of the exponent.

parameter size

The total size of the floating-point.

parameter rm

The rounding-mode.

parameter t

The bit-vector term.

returns

SMT-LIB: to_fp (indexed)

val of_bv : exponent:int -> int -> bv term -> t

of_bv ~exponent size rm t create a floatingt-point to_fp from IEEE 754 bit-vector.

parameter exponent

The size of the exponent.

parameter size

The total size of the floating-point.

parameter rm

The rounding-mode.

parameter t

The bit-vector term.

returns

SMT-LIB: to_fp (indexed)

val of_fp : exponent:int -> int -> rm term -> fp term -> t

of_fp ~exponent size rm t create a floatingt-point to_fp from floating-point.

parameter exponent

The size of the exponent.

parameter size

The total size of the floating-point.

parameter rm

The rounding-mode.

parameter t

The floating-point term.

returns

SMT-LIB: to_fp (indexed)

val abs : t -> t

abs t create a floatingt-point absolute value.

parameter t

The floating-point term.

returns

SMT-LIB: fp.abs

val neg : t -> t

neg t create a floatingt-point negation.

parameter t

The floating-point term.

returns

SMT-LIB: fp.neg

val add : rm term -> t -> t -> t

add rm t0 t1 create a floating-point addition.

parameter rm

The roundint-mode.

parameter t0

The first floating-point term.

parameter t1

The second floating-point term.

returns

SMT-LIB: fp.add

val sub : rm term -> t -> t -> t

sub rm t0 t1 create a floating-point substraction.

parameter rm

The roundint-mode.

parameter t0

The first floating-point term.

parameter t1

The second floating-point term.

returns

SMT-LIB: fp.sub

val mul : rm term -> t -> t -> t

mul rm t0 t1 create a floating-point multiplication.

parameter rm

The roundint-mode.

parameter t0

The first floating-point term.

parameter t1

The second floating-point term.

returns

SMT-LIB: fp.mul

val div : rm term -> t -> t -> t

div rm t0 t1 create a floating-point division.

parameter rm

The roundint-mode.

parameter t0

The first floating-point term.

parameter t1

The second floating-point term.

returns

SMT-LIB: fp.div

val fma : rm term -> t -> t -> t -> t

fma rm t0 t1 t2 create a floating-point fused multiplication and addition.

parameter rm

The roundint-mode.

parameter t0

The first floating-point term.

parameter t1

The second floating-point term.

parameter t2

The third floating-point term.

returns

SMT-LIB: fp.fma

val sqrt : rm term -> t -> t

sqrt rm t create a floating-point round to square root.

parameter rm

The roundint-mode.

parameter t0

The floating-point term.

returns

SMT-LIB: fp.sqrt

val rem : t -> t -> t

rem t0 t1 create a floating-point remainder.

parameter t0

The first floating-point term.

parameter t1

The second floating-point term.

returns

SMT-LIB: fp.rem

val rti : rm term -> t -> t

rti rm t create a floating-point round to integral.

parameter rm

The roundint-mode.

parameter t0

The floating-point term.

returns

SMT-LIB: fp.roundToIntegral

val min : t -> t -> t

min t0 t1 create a floating-point min.

parameter t0

The first floating-point term.

parameter t1

The second floating-point term.

returns

SMT-LIB: fp.min

val max : t -> t -> t

max t0 t1 create a floating-point max.

parameter t0

The first floating-point term.

parameter t1

The second floating-point term.

returns

SMT-LIB: fp.max

val leq : t -> t -> bv term

leq t0 t1 create a floating-point less than or equal.

parameter t0

The first floating-point term.

parameter t1

The second floating-point term.

returns

SMT-LIB: fp.leq

val lt : t -> t -> bv term

lt t0 t1 create a floating-point less than.

parameter t0

The first floating-point term.

parameter t1

The second floating-point term.

returns

SMT-LIB: fp.lt

val geq : t -> t -> bv term

geq t0 t1 create a floating-point greater than or equal.

parameter t0

The first floating-point term.

parameter t1

The second floating-point term.

returns

SMT-LIB: fp.geq

val gt : t -> t -> bv term

gt t0 t1 create a floating-point greater than.

parameter t0

The first floating-point term.

parameter t1

The second floating-point term.

returns

SMT-LIB: fp.gt

val eq : t -> t -> bv term

eq t0 t1 create a floating-point equality.

parameter t0

The first floating-point term.

parameter t1

The second floating-point term.

returns

SMT-LIB: fp.eq

val is_normal : t -> bv term

is_normal t create a floatingt-point is normal tester.

parameter t

The floating-point term.

returns

SMT-LIB: fp.isNormal

val is_subnormal : t -> bv term

is_subnormal t create a floatingt-point is subnormal tester.

parameter t

The floating-point term.

returns

SMT-LIB: fp.isSubnormal

val is_zero : t -> bv term

is_zero t create a floatingt-point is zero tester.

parameter t

The floating-point term.

returns

SMT-LIB: fp.isZero

val is_infinite : t -> bv term

is_infinite t create a floatingt-point is infinite tester.

parameter t

The floating-point term.

returns

SMT-LIB: fp.isInfinite

val is_nan : t -> bv term

is_nan t create a floatingt-point is Nan tester.

parameter t

The floating-point term.

returns

SMT-LIB: fp.isNan

val is_negative : t -> bv term

is_negative t create a floatingt-point is negative tester.

parameter t

The floating-point term.

returns

SMT-LIB: fp.isNegative

val is_positive : t -> bv term

is_positive t create a floatingt-point is positive tester.

parameter t

The floating-point term.

returns

SMT-LIB: fp.isPositive

val to_sbv : int -> rm term -> t -> bv term

to_sbv t create a floatingt-point is to_sbv term.

parameter t

The floating-point term.

returns

SMT-LIB: fp.to_sbv (indexed)

val to_ubv : int -> rm term -> t -> bv term

to_ubv t create a floatingt-point is to_ubv term.

parameter t

The floating-point term.

returns

SMT-LIB: fp.to_ubv (indexed)

val assignment : rm term Rm.operator -> fp value -> float

assignement t get floatint-point representation of the current model value of given floating-point term.

parameter term

The term to query a model value for.

returns

Floating-point representations of the given term.