bitwuzla 1.0.4 · OCaml Package

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.

package bitwuzla