package bitwuzla-cxx

You can search for identifiers within the package.

in-package search v0.2.0

SMT solver for AUFBVFP (C++ API)

Install

Dune Dependency

bitwuzla.github.io Readme Changelog MIT License Edit opam file Versions (8)

Authors

F

Frédéric Recoules

Maintainers

F

Frédéric Recoules <frederic.recoules@cea.fr>

Sources

bitwuzla-cxx-0.5.0.tbz

sha256=aa1c32619e7e4a50467da1b7ba0a8e2629a245713a498e0bf4fc8bf68355895d

sha512=5e11656a0a41c6102352671b95d4fb347dbeb72925d1cefedbad7f708cee26e9f548bc5f06c5eed1cc52545bd4aa13ffc8ba8ea57a4bcb420c49d1a2412a121c

doc/bitwuzla-cxx/Bitwuzla_cxx/RoundingMode/index.html

Module `Bitwuzla_cxx.RoundingMode`Source

Sourcetype t =

| Rne
(*
Round to the nearest even number. If the two nearest floating-point numbers bracketing an unrepresentable infinitely precise result are equally near, the one with an even least significant digit will be delivered.
SMT-LIB: RNE roundNearestTiesToEven
*)
| Rna
(*
Round to the nearest number away from zero. If the two nearest floating-point numbers bracketing an unrepresentable infinitely precise result are equally near, the one with larger magnitude will be selected.
SMT-LIB: RNA roundNearestTiesToAway
*)
| Rtn
(*
Round towards negative infinity (-oo). The result shall be the format’s floating-point number (possibly -oo) closest to and no less than the infinitely precise result.
SMT-LIB: RTN roundTowardNegative
*)
| Rtp
(*
Round towards positive infinity (+oo). The result shall be the format’s floating-point number (possibly +oo) closest to and no less than the infinitely precise result.
SMT-LIB: RTP roundTowardPositive
*)
| Rtz
(*
Round towards zero. The result shall be the format’s floating-point number closest to and no greater in magnitude than the infinitely precise result.
SMT-LIB: RTZ roundTowardZero
*)

Rounding mode for floating-point operations.

For some floating-point operations, infinitely precise results may not be representable in a given format. Hence, they are rounded modulo one of five rounding modes to a representable floating-point number.

The following rounding modes follow the SMT-LIB theory for floating-point arithmetic, which in turn is based on IEEE Standard 754. The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE Standard 754.

Sourceval to_string : t -> string

to_string t get string representation of this rounding mode.

returns
String representation of this rounding mode.