package bitwuzla

  1. Overview
  2. Docs

Module Term.FpSource

Floating-point

Sourcetype t = fp term

A floating-point term.

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

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

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

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

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

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

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

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

Sourcetype ieee_754 = private {
  1. sign : bv term;
  2. exponent : bv term;
  3. significand : bv term;
}

Floating-point IEEE 754 representation.

Sourcetype (!'a, !'b, !'c) operator =
  1. | Abs : (t -> t, t, fp) operator
    (*

    Floating-point absolute value.

    SMT-LIB: fp.abs

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

    Floating-point addition.

    SMT-LIB: fp.add

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

    Floating-point division.

    SMT-LIB: fp.div

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

    Floating-point equality.

    SMT-LIB: fp.eq

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

    Floating-point fused multiplcation and addition.

    SMT-LIB: fp.fma

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

    Floating-point IEEE 754 value.

    SMT-LIB: fp

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

    Floating-point greater than or equal.

    SMT-LIB: fp.geq

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

    Floating-point greater than.

    SMT-LIB: fp.gt

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

    Floating-point is infinity tester.

    SMT-LIB: fp.isInfinite

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

    Floating-point is Nan tester.

    SMT-LIB: fp.isNaN

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

    Floating-point is negative tester.

    SMT-LIB: fp.isNegative

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

    Floating-point is normal tester.

    SMT-LIB: fp.isNormal

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

    Floating-point is positive tester.

    SMT-LIB: fp.isPositive

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

    Floating-point is subnormal tester.

    SMT-LIB: fp.isSubnormal

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

    Floating-point is zero tester.

    SMT-LIB: fp.isZero

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

    Floating-point less than or equal.

    SMT-LIB: fp.leq

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

    Floating-point less than.

    SMT-LIB: fp.lt

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

    Floating-point max.

    SMT-LIB: fp.max

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

    Floating-point min.

    SMT-LIB: fp.min

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

    Floating-point multiplcation.

    SMT-LIB: fp.mul

    *)
  21. | Neg : (t -> t, t, fp) operator
    (*

    Floating-point negation.

    SMT-LIB: fp.neg

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

    Floating-point remainder.

    SMT-LIB: fp.rem

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

    Floating-point round to integral.

    SMT-LIB: fp.roundToIntegral

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

    Floating-point round to square root.

    SMT-LIB: fp.sqrt

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

    Floating-point round to subtraction.

    SMT-LIB: fp.sqrt

    *)
  26. | 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)

    *)
  27. | 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)

    *)
  28. | 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)

    *)
  29. | 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)

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

    Floating-point to_sbv.

    SMT-LIB: fp.to_sbv (indexed)

    *)
  31. | 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.

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

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

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

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

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

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

Sourceval abs : t -> t

abs t create a floatingt-point absolute value.

  • parameter t

    The floating-point term.

  • returns

    SMT-LIB: fp.abs

Sourceval neg : t -> t

neg t create a floatingt-point negation.

  • parameter t

    The floating-point term.

  • returns

    SMT-LIB: fp.neg

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

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

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

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