-
Notifications
You must be signed in to change notification settings - Fork 33
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[doc] Document the floating-point and bitvector primitives #762
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 | ||
``` |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -37,12 +37,83 @@ | |
* `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 | ||
``` | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. You could add an example of input file using the round function? Or a link to an examples in the appropriate directory of the repository. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Sure. |
||
|
||
Here is an example: | ||
|
||
```alt-ergo | ||
goal g: integer_round(ToZero, 2.1) = 2 | ||
``` | ||
|
||
## User-defined extensions of theories | ||
|
||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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. | ||
|
||
Comment on lines
+2
to
+12
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I wad doing the same doc... There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. The BV primitives are only available using the Dolmen frontend, I had to mention it. I can remove that paragraph. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Let's keep your paragraph ;) |
||
## 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. |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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}. | ||
|
||
Comment on lines
+8
to
+9
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Why do you add a link here? There is very same link on the sidebar. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This is the odoc for the alt-ergo package (this page: https://ocamlpro.github.io/alt-ergo/odoc/dev/alt-ergo/index.html ), I don't see a link to the language doc in the sidebar? (Sorry, this probably should have been in a separate PR, I just did it as I was in the doc folder) There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Oh sorry, I thought it was in the sphinx documentation. You don't need to do a separate PR for such a small modification. |
||
{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}. | ||
|
||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe a table given the translation between these AE primitives and the SMT-LIB ones would be clearer?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't think a table would be very helpful, people usually use either AE or SMT-LIB. This is in the documentation for the native input language anyways, so I'll remove these notes and add corresponding paragraphs in the SMT-LIB format doc.