[doc] Document the floating-point and bitvector primitives #762
Conversation
| # 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. | ||
|
|
There was a problem hiding this comment.
I wad doing the same doc...
There was a problem hiding this comment.
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.
Let's keep your paragraph ;)
| *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. |
There was a problem hiding this comment.
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.
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.
| `int_floor` and `int_ceil` implement the standard `floor` and `ceil` functions. | ||
| They compute the greatest integer less than a real and the least integer | ||
| greater than a real, respectively. |
There was a problem hiding this comment.
By standard, you mean the SMT-LIB standard or the mathematical one? I guess they agree but who knows :)
There was a problem hiding this comment.
There are no floor or ceil functions in the SMT-LIB standard. Changed to usual instead.
| The `sqrt_real` function denotes the square root of a real number. Alt-Ergo | ||
| only computes rational under- and over-approximations. |
There was a problem hiding this comment.
Does it mean sqrt_real computes the under-approximation or the over-approximation?
There was a problem hiding this comment.
sqrt_real computes the square root. Internally, Alt-Ergo tracks both an under- and an over- approximation of the square root as rationals. I agree that this sentence is confusing, I will remove it.
There was a problem hiding this comment.
But I agree we shouldn't write the square root without mentioning it's an approximation.
There was a problem hiding this comment.
It is not an approximation.
Edited to clarify: if e is not a constant rational square (i.e. equal to r * r for some rational r), Alt-Ergo treats sqrt_real(e) as uninterpreted, with the constraint that sqrt_real_default(e) ≤ sqrt_real(e) ≤ sqrt_real_excess(e) where sqrt_real_default and sqrt_real_excess are the under- and over-approximation. sqrt_real_default and sqrt_real_excess always compute to rational numbers for all (constant) rational inputs, but sqrt_real doesn't.
(Also in all cases we do have the constraint sqrt_real(x) * sqrt_real(x) = x of course)
| See also the {{:https://ocamlpro.github.io/alt-ergo/}language documentation}. | ||
|
|
There was a problem hiding this comment.
Why do you add a link here? There is very same link on the sidebar.
There was a problem hiding this comment.
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.
Oh sorry, I thought it was in the sphinx documentation. You don't need to do a separate PR for such a small modification.
|
|
||
| ```alt-ergo | ||
| logic integer_round : fpa_rounding_mode, real -> int | ||
| ``` |
There was a problem hiding this comment.
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.
bclement-ocp
changed the title
Nominating for 2.5.0 @Halbaroth I guess :)