[doc] Document the floating-point and bitvector primitives (OCamlPro#762

)

docs/sphinx_docs/About/changes.md

@@ -1,4 +1,8 @@
 # Changes
 
+This is the changelog of all the Alt-Ergo releases. The PR numbers reference
+the [official Alt-Ergo repository on
+GitHub](https://github.com/OCamlPro/Alt-Ergo).
+
 ```{include} ../../../CHANGES.md
 ```

docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md

@@ -1,46 +1,44 @@
-# Built-in
-
-## Built-in types
+# Built-in types
 
 Alt-Ergo's native language includes the following built-in types.
 Creation and manipulation of values having those types are covered in [built-in operators](#built-in-operators).
 
-### Boolean types
+## Boolean types
  * `bool`, the preferred type to represent propositional variables. Boolean constants are `true` and `false`.
  * `prop`, an historical type still supported in Alt-Ergo 2.3.0.  
     The historical separation comes from Alt-Ergo origins in the Coq ecosystem: in Coq, `prop` is much richer than `bool`.  
     In Alt-Ergo 2.3.0, `prop` and `bool` have been merged in order to simplify interactions with the [SMT-LIB ](http://smtlib.cs.uiowa.edu/) standard.  
     More information on the `bool`/`prop` conflict can be found in [this section](#the-bool-prop-conflict).
 
-### Numeric types
+## Numeric types
  * `int` for (arbitrary large) integers.
  * `real` for reals. This type actually represents the smallest extension of the rationals which is algebraically closed and closed by exponentiation. Rationals with arbitrary precision are used under the hood. 
 
-### Unit type
+## Unit type
  `unit` is Alt-Ergo native language's [unit type](https://en.wikipedia.org/wiki/Unit_type).
 
-### Bitvectors
+## Bitvectors
  `bitv` are fixed-size binary words of arbitrary length.
  There exists a bitvector type `bitv[n]` for each non-zero positive integer `n`. For example, `bitv[8]` is a bitvector of length `8`.
 
-### Type variables
+## Type variables
  Alt-Ergo's native language's type system supports prenex polymorphism. This allows efficient reasoning about generic data structure.
  Type variables can be created implicitly, and are implicitly universally quantified in all formulas. Any formula which requires a type can accept a type variable.
  Type variable may be used to parametrize datatypes, as we will see when we will create new types, or in the following example of `farray`.
 
  Type variables are indicated by an apostrophe `'`. For example, `'a` is a type variable.
 
-### Polymorphic functional arrays
+## Polymorphic functional arrays
  Alt-Ergo's native language includes functional polymorphic arrays, represented by the `farray` type, and has a built-in theory to reason about them.
 
  The `farray` is parametrized by two types: the type of their indexes (default is `int`) and the type of their values (no default).
  Array can be accessed using any index of valid type.
  Functional polymorphic arrays are persistent structures: they may be updated, but only for the scope of an expression.
 
 
-## Built-in operators
+# Built-in operators
 
-### Logical operators
+## Logical operators
 
 | Operation    | Notation  | Type(s)              |
 |--------------|-----------|----------------------|
@@ -54,7 +52,7 @@ Creation and manipulation of values having those types are covered in [built-in
 For all those operators, `bool` and `prop` are fully interchangeable.
 
 (the-bool-prop-conflict)=
-#### The `bool`/`prop` conflict
+### The `bool`/`prop` conflict
 
 Prior to Alt-Ergo 2.3.0, Alt-Ergo's native language handled differently boolean variables `bool` and propositional variables `prop`.
 The two keywords still exist in Alt-Ergo 2.3.0, but those two types have been made fully compatible: any function or operator taking a `bool` or a `prop` as an argument accepts both.
@@ -72,7 +70,7 @@ In all other cases, it is advised the use `prop` rather than `bool`, because it
 * `prop` and `bool` **can** be the type of an *uninterpreted variable* (`logic` keyword).
 Note that a `predicate` has `prop` output type.
 
-#### Examples
+### Examples
 
 ```
 (* Correct example *)
@@ -90,7 +88,7 @@ axiom a2: B -> C
 goal g: (B->A) and (C->B) -> (A <-> C)
 ```
 
-### Numeric operators
+## Numeric operators
 
 | Operation               | Notation  | Type(s)                                                                                        |
 |-------------------------|-----------|------------------------------------------------------------------------------------------------|
@@ -103,7 +101,7 @@ goal g: (B->A) and (C->B) -> (A <-> C)
 | Exponentiation (`int`)  | `x ** y`  | `int, int -> int`                                                                              |
 | Exponentiation (`real`) | `x **. y` | `real, real -> real`, <br>`real, int -> real`, <br>`int, real -> real`, <br>`int, int -> real` |
 
-### Comparisons
+## Comparisons
 
 | Operation                | Notation                      | Type(s)                                  | Notes                                                                                                            |
 |------------------------- |-------------------------------|------------------------------------------|------------------------------------------------------------------------------------------------------------------|
@@ -129,7 +127,72 @@ goal g:
     x + t = 0
 ```
 
-### Bitvectors
+## Additional numeric primitives
+
+Alt-Ergo provides built-in primitives for mixed integers and real problems,
+along with some limited reasoning support, typically restricted to constants.
+These primitives are only available in the native input format.
+
+### Conversion between integers and reals
+
+```alt-ergo
+logic real_of_int : int -> real
+```
+
+`real_of_int` converts an integer into its representation as a real number.
+
+*Note*: When using the `dolmen` frontend, `real_of_int` is also available in
+the smtlib2 format as the `to_real` function from the `Reals_Ints` theory.
+
+```alt-ergo
+logic int_floor : real -> int
+logic int_ceil : real -> int
+logic real_is_int : real -> bool
+```
+
+`int_floor` and `int_ceil` implement the usual `floor` and `ceil` functions.
+They compute the greatest integer less than a real and the least integer
+greater than a real, respectively.
+
+`real_is_int` is true for reals that are exact integers, and false otherwise.
+
+*Note*: When using the Dolmen frontend, `int_floor` and `real_is_int` are
+also available in the smtlib2 format as the `to_int` and `is_int` functions
+from the `Reals_Ints` theory respectively.
+
+### Square root
+
+```alt-ergo
+logic sqrt_real : real -> real
+```
+
+The `sqrt_real` function denotes the square root of a real number.
+
+### Internal primitives
+
+Alt-Ergo also implements additional primitives that are tuned for specific
+internal use cases. They are only listed here for completeness and adventurous
+users, but their use should be avoided. Support for these primitives may be
+removed without notice in future versions of Alt-Ergo.
+
+In particular, the `abs_real`, `abs_int`, `max_real`, `max_int` and `min_int`
+functions were introduced prior to `if .. then .. else ..` statements in
+Alt-Ergo. They are preserved due to being used internally for floating-point
+reasoning, but should not be used outside of the solver. Prefer defining these
+functions using `if .. then .. else ..` instead.
+
+```alt-ergo
+logic abs_real : real -> real
+logic abs_int : int -> int
+logic max_real : real, real -> real
+logic max_int : int, int -> int
+logic min_int : int, int -> int
+logic sqrt_real_default : real -> real
+logic sqrt_real_excess : real -> real
+logic integer_log2 : real -> int
+```
+
+## Bitvectors
 
 Remember that bitvectors are fixed-size binary words: vectors of `0` and `1`.
 
@@ -144,7 +207,7 @@ Note that bitvectors are indexed from right to left.
 | Extraction of contiguous bits | `x^{p,q}` <br> where 0<=p<=q<len(x)                                  | `bitv[q-p+1]`                 |
 
 
-#### Examples
+### Examples
 
 ```
 (** Usage of bitv types *)
@@ -178,7 +241,7 @@ goal g5 :
     (s^{16,31} = y^{0,15} and s^{0,15} = x^{16,31}) 
 ```
 
-### Type variables
+## Type variables
 
 As type variables and polymorphism have already been described, let's just look at the following example.
 
@@ -202,13 +265,13 @@ goal g3:
    g(f(0.01)) = g(0)
 ```
 
-### Polymorphic functional arrays
+## Polymorphic functional arrays
 
 [TODO: add table?]
 
 Remember that `farray` are parametrized by two types: the type of their indexes (default is `int`) and the type of their values (no default).
 
-#### Syntax
+### Syntax
 ```
 (* Instantiation of a farray type *)
 <farray_type>        ::= <value_type> 'farray'
@@ -221,7 +284,7 @@ Remember that `farray` are parametrized by two types: the type of their indexes
 <farray_update_expr> ::= <array_id> '[' <index> '<-' <new_value> ( ',' <index> '<-' <new_value> )* ']'
 ```
 
-#### Examples
+### Examples
 ```
 (* arr1 is a general polymorphic farray *)
 logic arr1: ('a, 'b) farray

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

@@ -37,12 +37,83 @@ All theories are always considered *modulo equality*.
 * `FPA`: Floating-point arithmetic
 
 
-### About floating-point arithmetic
+## Floating-point Arithmetic
+
+Alt-Ergo implements partial support for floating-point arithmetic. More
+precisely, Alt-Ergo implements the second and third layers from the paper "[A
+Three-tier Strategy for Reasoning about Floating-Point Numbers in
+SMT](https://inria.hal.science/hal-01522770)" by Conchon et al.
+
+*Note*: Support for floating-point arithmetic is enabled by default in
+Alt-Ergo since version 2.5.0.  Previous versions required the use of command
+line flags `--use-fpa` and `--prelude fpa-theory-2019-10-08-19h00.ae` to enable
+it.
+
+This means that Alt-Ergo doesn't actually support a floating-point type (that
+may come in a future release); instead, it supports a rounding function, as
+described in the paper.  The rounding function transforms a real into the
+nearest representable float, according to the standard floating-point rounding
+modes. Unlike actual floats, there are no NaNs or infinites, and there is no
+overflow (but there is underflow): one way to think about the underlying data
+type is as floats with a potentially infinite exponent.
+
+NaNs, infinites, and overflows must be handled outside of Alt-Ergo by an
+implementation of the three-tier strategy described in the paper (this is done
+automatically in Why3 when you use floats).
+
+The rounding function is available as a builtin function called `float`:
+
+```alt-ergo
+type fpa_rounding_mode =
+  | NearestTiesToEven
+    (** To nearest, tie breaking to even mantissa *)
+  | ToZero
+    (** Round toward zero *)
+  | Up
+    (** Round toward plus infinity *)
+  | Down
+    (** Round toward minus infinity *)
+  | NearestTiesToAway
+    (** To nearest, tie breaking away from zero *)
+
+(** The first int is the mantissa's size, including the implicit bit.
+
+    The second int is the exponent of the minimal representable normalized
+    number. *)
+logic float: int, int, fpa_rounding_mode, real -> real
+```
+
+The `float` function *must* be called with concrete values for its first 3
+arguments, using other symbolic expressions is not supported and will result in
+an error (defining functions that call `float` is also possible, as long as the
+corresponding arguments of the wrapping function are only called with concrete
+values).
+
+Alt-Ergo also exposes convenience functions specialized for standard
+floating-point types:
+
+```alt-ergo
+function float32(m: fpa_rounding_mode, x: real): real = float(24, 149, m, x)
+function float32d(x: real): real = float32(NearestTiesToEven, x)
+function float64(m: fpa_rounding_mode, x: real): real = float(53, 1074, m, x)
+function float64d(x: real): real = float64(NearestTiesToEven, x)
+```
 
-Floating-point arithmetic (FPA) is a recent addition to Alt-Ergo, and is not documented here.
-To use it, it is necessary to load the corresponding prelude. The strategy used to handle FPA is based on over-approximation by intervals of reals, and roundings.
-More information on this strategy and the language extension can be found in [this article](https://hal.inria.fr/hal-01522770).
+These functions are currently only available when using the native language;
+they are not available when using the smtlib2 input format.
 
+Finally, the `integer_round` function allows rounding a real to an integer
+using the aforementioned rounding modes:
+
+```alt-ergo
+logic integer_round : fpa_rounding_mode, real -> int
+```
+
+Here is an example:
+
+```alt-ergo
+goal g: integer_round(ToZero, 2.1) = 2
+```
 
 ## User-defined extensions of theories
 

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

@@ -0,0 +1,22 @@
+
+# SMT-LIB Version 2
+
+Alt-Ergo has partial support for the [SMT-LIB
+standard](http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf)
+language from the SMT community.
+
+*Note*: As of version 2.5.0, enhanced support for the SMT-LIB language is
+provided by the new [Dolmen](http://gbury.github.io/dolmen/) frontend. To use
+it, pass the option `--frontend dolmen` to Alt-Ergo. This will become the
+default in a future release.
+
+## Bit-vectors
+
+Since version 2.5.0, Alt-Ergo has partial support for the `FixedSizeBitVectors`
+theory and the `QF_BV` and `BV` logics when used with the Dolmen frontend. All
+the symbols from these logics are 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.

docs/sphinx_docs/Input_file_formats/index.rst

@@ -3,12 +3,11 @@
 Input file formats
 ******************
 
-Alt-ergo supports different input language. The main language is his native language, based on the lamguage of the Why plateform and detailed below. Alt-ergo (partially) supports the standard language of the SMT community, SMT-LIB. It also (partially) supports the input language of Why3.
+Alt-ergo supports different input language. The main language is his native language, based on the lamguage of the Why plateform and detailed below. Alt-ergo (partially) supports the standard language of the SMT community, SMT-LIB. It also (partially) supports the input language of Why3 through the :doc:`AB-Why3 plugin <../Plugins/ab_why3>`.
 
 .. toctree::
    :maxdepth: 2
    :caption: Contents
 
    Alt-Ergo's native language <Native/index>
-   SMT-LIB                    <http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf>
-   WhyML (partial support)    <http://why3.lri.fr/doc/syntaxref.html>
+   SMT-LIB                    <SMT-LIB2/index>

docs/sphinx_docs/Plugins/ab_why3.md

@@ -6,7 +6,7 @@ Atelier-B framework in Why3 format. It should be used with a prelude
 defining the B Set theory (currently provided in
 `src/plugins/AB-Why3/preludes/b-set-theory-prelude-2020-02-28.ae`).
 
-
+See also the [Why3 syntax reference](http://why3.lri.fr/doc/syntaxref.html).
 
 # What this plugin is not ?
 

docs/sphinx_docs/Usage/index.md

@@ -83,12 +83,6 @@ Preludes can be passed to Alt-Ergo as follows:
    path). You can also provide a relative or an absolute path as shown
    by "some-path/q.ae".
 
-   For instance, the following command-line enables floating-point
-   arithmetic reasoning in Alt-Ergo and indicates that the FPA prelude
-   should be loaded:
-
-        $ alt-ergo --use-fpa --prelude fpa-theory-2017-01-04-16h00.ae <file.ae>
-
 ### Plugins and Preludes directories
 
 As stated above, the `--where` option of `alt-ergo` can be used to get the absolute

src/bin/text/index.mld

@@ -5,9 +5,11 @@
 The alt-ergo package installs the {e alt-ergo} binary, whose documentation
 is available through the {e --help} option.
 
+See also the {{:https://ocamlpro.github.io/alt-ergo/}language documentation}.
+
 {3 Alt_Ergo_common }
 
-This package uses the Alt-Ergo_common internal lib (see {{:index_common.html}[Alt_ergo_common]}) for parsing command line, input file, and main solving loop.
+This package uses the Alt-Ergo_common internal lib (see {{!page-index_common}[Alt_ergo_common]}) for parsing command line, input file, and main solving loop.
 
 See also the {{:Alt_ergo_common/index.html}list of modules}.