feat(FPA): Add ae.float{16,32,64,128} SMT-LIB builtins

This patch adds `ae.float16`, `ae.float32`, `ae.float64` and
`ae.float128` as abbreviations for `(_ ae.round 11 24)`,
`(_ ae.round 24 149)`, `(_ ae.round 53 1074)` and
`(_ ae.round 113 16494)` respectively.

These serve a similar purpose as `float32` and `float64` in the native
format: allow short names for common floating point sorts without
requiring users to remember the appropriate parameters to `ae.round`.

(Note that `ae.float16` and `ae.float128` are not available in the
native format; they are added for consistency with the `FloatXX` sorts
provided by the FloatingPoint theory in the SMT-LIB.)

docs/sphinx_docs/Input_file_formats/Native/05_theories.md

@@ -77,10 +77,26 @@ type fpa_rounding_mode =
   | NearestTiesToAway
     (** To nearest, tie breaking away from zero *)
 
-(** The first int is the mantissa's size, including the implicit bit.
+(** The first int [prec] is the mantissa's size, including the implicit bit.
 
-    The second int is the exponent of the minimal representable normalized
-    number. *)
+    The second int [exp] is the absolute value of the exponent of the smallest
+    representable positive number. Note that this is not the `emin` value
+    defined in IEEE-754, which represents the minimum exponent of the smallest
+    normal positive number.
+
+    The result of a call to [float(prec, exp, rm, x)] is always of the form:
+
+      (-1)^s * c * 2^q
+
+    where [s] is [0] or [1], [c] is an integer with at most [prec - 1] binary
+    digits (that is, [0 <= c < 2^(prec - 1)]), and [q >= exp] is an integer.
+
+    Given `eb` the number of bits of the exponent and `sb` the number of bits
+    of the significand (including the hidden bit), `prec` and `exp` are
+    computed as follows:
+
+      prec = sb
+      exp = (1 lsl (eb - 1)) + sb - 3 *)
 logic float: int, int, fpa_rounding_mode, real -> real
 ```
 

docs/sphinx_docs/Input_file_formats/SMT-LIB2/index.md

@@ -17,3 +17,46 @@ available, although reasoning using them is limited and incomplete for now.
 The non-standard symbols `bv2nat` and `(_ int2bv n)` (where `n >
 0` is a natural number representing the target bit-vector size) for conversion
 between integers and bit-vectors are supported.
+
+## Floating-Point Arithmetic
+
+Alt-Ergo does not currently support the `FloatingPoint` SMT-LIB theory.
+Instead, Alt-Ergo implements the second and third layers described in the paper
+"[A Three-tier Strategy for Reasoning about Floating-Point Numbers in
+SMT](https://inria.hal.science/hal-01522770)" by Conchon et al.
+
+Alt-Ergo provides the rounding function described in the paper by making
+available all functions symbols with declarations of the form below, where
+`prec` and `exp` are numerals greater than 1 and `RoundingMode` is defined in
+the FloatingPoint SMT-LIB theory.
+
+```smt-lib
+((_ ae.round prec exp) RoundingMode Real Real)
+```
+
+*Note*: While Alt-Ergo has built-in support for **computing** with `ae.round`
+on known arguments, reasoning capabilities involving `ae.round` on non-constant
+arguments are disabled by default and currently requires to use the flag
+`--enable-theories fpa`.
+
+`prec` defines the number of bits in the significand, including the hidden bit,
+and is equivalent to the `sb` parameter of the `(_ FloatingPoint eb sb)` sort
+in the FloatingPoint SMT-LIB theory.
+
+`exp` defines the absolute value of the exponent of the smallest representable
+positive number (this is not the same as the `emin` value defined in IEEE-754,
+which is the minimum exponent of the smallest *normal* positive number). An
+appropriate value for `exp` can be computed from the `eb` and `sb` parameters
+of the `(_ FloatingPoint eb sb)` sort as `exp = 2^(eb - 1) + sb - 3`.
+
+The result of `(_ ae.round prec exp)` is always of the form `(-1)^s * c * 2^q`
+where `s` is a sign (`0` or `1`), `c` is an integer with at most `prec - 1`
+binary digits (i.e. `0 <= c < 2^(prec - 1)`) and `q >= exp` is an integer.
+
+The following function symbols are provided as short synonyms for common
+floating point representations:
+
+ - `ae.float16` is a synonym for `(_ ae.round 11 24)`
+ - `ae.float32` is a synonym for `(_ ae.round 24 149)`
+ - `ae.float64` is a synonym for `(_ ae.round 53 1074)`
+ - `ae.float128` is a synonym for `(_ ae.round 113 16494)`

src/lib/frontend/d_cnf.ml

@@ -429,6 +429,14 @@ let smt_fpa_builtins =
         | n, m -> term_app env s (smt_round n m)
         | exception Failure _ -> `Not_found
       end
+    | Id { ns = Term ; name = Simple "ae.float16" } ->
+      term_app env s (smt_round 11 24)
+    | Id { ns = Term ; name = Simple "ae.float32" } ->
+      term_app env s (smt_round 24 149)
+    | Id { ns = Term ; name = Simple "ae.float64" } ->
+      term_app env s (smt_round 53 1074)
+    | Id { ns = Term ; name = Simple "ae.float128" } ->
+      term_app env s (smt_round 113 16494)
     | Dl.Typer.T.Id id -> begin
         match DStd.Id.Map.find_exn id other_builtins env s with
         | e -> e