Skip to content
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.

Sign up for GitHub

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

Jump to bottom

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

Merged
merged 4 commits into from
Jul 27, 2023
Merged

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

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
2697c99
[doc] Document the floating-point primitives
bclement-ocp Jul 27, 2023
5d035ec
Add example of integer_round
bclement-ocp Jul 27, 2023
c0d679c
s/standard/usual floor and ceil
bclement-ocp Jul 27, 2023
b49ad6c
Remove mention of sqrt_real_default and sqrt_real_excess
bclement-ocp Jul 27, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions docs/sphinx_docs/About/changes.md
View file
Open in desktop
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
```
106 changes: 85 additions & 21 deletions docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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) |
|--------------|-----------|----------------------|
Expand All @@ -54,7 +52,7 @@
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.
Expand All @@ -72,7 +70,7 @@
* `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 *)
Expand All @@ -90,7 +88,7 @@
goal g: (B->A) and (C->B) -> (A <-> C)
```

### Numeric operators
## Numeric operators

| Operation | Notation | Type(s) |
|-------------------------|-----------|------------------------------------------------------------------------------------------------|
Expand All @@ -103,7 +101,7 @@
| 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 |
|------------------------- |-------------------------------|------------------------------------------|------------------------------------------------------------------------------------------------------------------|
Expand All @@ -129,7 +127,73 @@
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.
Comment on lines +144 to +145
Copy link
Collaborator

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?

Copy link
Collaborator Author

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.


```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 standard `floor` and `ceil` functions.
They compute the greatest integer less than a real and the least integer
greater than a real, respectively.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

By standard, you mean the SMT-LIB standard or the mathematical one? I guess they agree but who knows :)

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There are no floor or ceil functions in the SMT-LIB standard. Changed to usual instead.


`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. Alt-Ergo
only computes rational under- and over-approximations.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does it mean sqrt_real computes the under-approximation or the over-approximation?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But I agree we shouldn't write the square root without mentioning it's an approximation.

Copy link
Collaborator Author

@bclement-ocp bclement-ocp Jul 27, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)


### 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`.

Expand All @@ -144,7 +208,7 @@
| Extraction of contiguous bits | `x^{p,q}` <br> where 0<=p<=q<len(x) | `bitv[q-p+1]` |


#### Examples
### Examples

```
(** Usage of bitv types *)
Expand Down Expand Up @@ -178,7 +242,7 @@
(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.

Expand All @@ -190,7 +254,7 @@
axiom a2: forall x:int. f(x)=0

goal g1:
(* Valid *)

Check warning on line 257 in docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md

View workflow job for this annotation

GitHub Actions / Sphinx documentation 

Pygments lexer name 'alt-ergo' is not known
g(f(0.01)) = f(0.01)

goal g2:
Expand All @@ -199,16 +263,16 @@

goal g3:
(* I don't know *)
g(f(0.01)) = g(0)

Check warning on line 266 in docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md

View workflow job for this annotation

GitHub Actions / Sphinx documentation 

Pygments lexer name 'alt-ergo' is not known
```

### 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'
Expand All @@ -217,11 +281,11 @@
(* Access - this expression is of type (value_type) *)
<farray_access_expr> ::= <array_id> '[' <index> ']'

(* Update - this expression is of type ((index_type) (value_type) farray) *)

Check warning on line 284 in docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md

View workflow job for this annotation

GitHub Actions / Sphinx documentation 

Pygments lexer name 'alt-ergo' is not known
<farray_update_expr> ::= <array_id> '[' <index> '<-' <new_value> ( ',' <index> '<-' <new_value> )* ']'
```

#### Examples
### Examples
```
(* arr1 is a general polymorphic farray *)
logic arr1: ('a, 'b) farray
Expand All @@ -237,7 +301,7 @@

```
(* Accessing and updating farrays *)
goal g1:

Check warning on line 304 in docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md

View workflow job for this annotation

GitHub Actions / Sphinx documentation 

Pygments lexer name 'alt-ergo' is not known
forall i,j,k:int.
forall v,w:'a.
forall b:'a farray.
Expand Down
73 changes: 69 additions & 4 deletions docs/sphinx_docs/Input_file_formats/Native/05_theories.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,12 +37,77 @@
* `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

Check warning on line 66 in docs/sphinx_docs/Input_file_formats/Native/05_theories.md

View workflow job for this annotation

GitHub Actions / Sphinx documentation 

Pygments lexer name 'alt-ergo' is not known
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).

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).
Alt-Ergo also exposes convenience functions specialized for standard
floating-point types:

```alt-ergo

Check warning on line 95 in docs/sphinx_docs/Input_file_formats/Native/05_theories.md

View workflow job for this annotation

GitHub Actions / Sphinx documentation 

Pygments lexer name 'alt-ergo' is not known
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)
```

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

Check warning on line 108 in docs/sphinx_docs/Input_file_formats/Native/05_theories.md

View workflow job for this annotation

GitHub Actions / Sphinx documentation 

Pygments lexer name 'alt-ergo' is not known
logic integer_round : fpa_rounding_mode, real -> int
```
Copy link
Collaborator

Choose a reason for hiding this comment

The 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.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure.


## User-defined extensions of theories

Expand Down
22 changes: 22 additions & 0 deletions docs/sphinx_docs/Input_file_formats/SMT-LIB2/index.md
View file
Open in desktop
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
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wad doing the same doc...

Copy link
Collaborator Author

Choose a reason for hiding this comment

The 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.

Copy link
Collaborator

Choose a reason for hiding this comment

The 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.
5 changes: 2 additions & 3 deletions docs/sphinx_docs/Input_file_formats/index.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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>
2 changes: 1 addition & 1 deletion docs/sphinx_docs/Plugins/ab_why3.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ?

Expand Down
6 changes: 0 additions & 6 deletions docs/sphinx_docs/Usage/index.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion src/bin/text/index.mld
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Collaborator

Choose a reason for hiding this comment

The 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.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The 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)

Copy link
Collaborator

Choose a reason for hiding this comment

The 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}.

Expand Down
Loading