Merge pull request #758 from Halbaroth/backporting-2.5.0

Backporting 2.5.0

alt-ergo-lib.opam

@@ -17,9 +17,9 @@ depends: [
   "ocaml" {>= "4.08.0"}
   "dune" {>= "3.0"}
   "dune-build-info"
-  "dolmen" {>= "0.8.1"}
-  "dolmen_type" {>= "0.8.1"}
-  "dolmen_loop" {>= "0.8.1"}
+  "dolmen" {>= "0.9"}
+  "dolmen_type" {>= "0.9"}
+  "dolmen_loop" {>= "0.9"}
   "ocplib-simplex" {>= "0.5"}
   "zarith" {>= "1.4"}
   "seq"
@@ -54,18 +54,3 @@ license: [
   "LicenseRef-OCamlpro-Non-Commercial"
   "Apache-2.0"
 ]
-
-pin-depends: [
-  [
-  "dolmen.dev"
-  "git+https://github.com/Gbury/dolmen.git#master"
-  ]
-  [
-  "dolmen_loop.dev"
-  "git+https://github.com/Gbury/dolmen.git#master"
-  ]
-  [
-  "dolmen_type.dev"
-  "git+https://github.com/Gbury/dolmen.git#master"
-  ]
-]

alt-ergo-lib.opam.template

@@ -6,18 +6,3 @@ license: [
   "LicenseRef-OCamlpro-Non-Commercial"
   "Apache-2.0"
 ]
-
-pin-depends: [
-  [
-  "dolmen.dev"
-  "git+https://github.com/Gbury/dolmen.git#master"
-  ]
-  [
-  "dolmen_loop.dev"
-  "git+https://github.com/Gbury/dolmen.git#master"
-  ]
-  [
-  "dolmen_type.dev"
-  "git+https://github.com/Gbury/dolmen.git#master"
-  ]
-]

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/00_summary.md

@@ -23,13 +23,13 @@
 Reserved keywords are the following.
 * To add new uninterpreted symbols (variables or functions) to the signature: [`logic`](01_declaration_of_symbols.md#logic-uninterpreted-symbols) and the [`ac` modifier](01_declaration_of_symbols.md#ac-modifier-associative-and-commutative-symbols) for associative and commutative symbols.
 * Interpreted functions: [`function`](01_declaration_of_symbols.md#function-user-defined-functions) and [`predicate`](01_declaration_of_symbols.md#predicate-propositional-valued-functions).
-* Built-in types: [`int`](02_types/02_01_builtin.md#numbers-int-real-and-floats), [`real`](02_types/02_01_builtin.md#numbers-int-real-and-floats), [`bool`](02_types/02_01_builtin.md#bool-and-prop), [`prop`](02_types/02_01_builtin.md#bool-and-prop), [`unit`](02_types/02_01_builtin.md#unit), [`bitv`](02_types/02_01_builtin.md#bitvectors-bitv), [`farray`](02_types/02_01_builtin.md#functional-polymorphic-arrays-farray).
+* Built-in types: [`int`](02_types/02_01_builtin.md#numeric-types), [`real`](02_types/02_01_builtin.md#numeric-types), [`bool`](02_types/02_01_builtin.md#boolean-types), [`prop`](02_types/02_01_builtin.md#boolean-types), [`unit`](02_types/02_01_builtin.md#unit-type), [`bitv`](02_types/02_01_builtin.md#bitvectors), [`farray`](02_types/02_01_builtin.md#polymorphic-functional-arrays).
 * Constant and operators for propositions are available: `and`, `or`, `xor`, `not`, `true`, `false`. The construct `distinct` is available for all types. Quantifiers `forall` and `exists` can be used.
 * To create new types: [`type`](02_types/index). They keyword `of` is useful when dealing with structured datatypes, which include [records](02_types/02_02_user_defined.md#records), [enums](02_types/02_02_user_defined.md#enums-and-algebraic-datatypes) and [algebraic datatypes](02_types/02_02_user_defined.md#enums-and-algebraic-datatypes).
 * To declare new axioms: [`axiom`](03_declaration_of_axioms.md#axiom), and the special case [`rewriting`](03_declaration_of_axioms.md#rewriting).
 * To define goals that must be proven valid: [`goal`](04_setting_goals.md#goal). [`cut`](04_setting_goals.md#intermediate-goals-cut-and-check) and [`check`](04_setting_goals.md#intermediate-goals-cut-and-check) can create intermediate goals that won't interact with other goals through [triggers](03_declaration_of_axioms.md#triggers).
-* New theories may be defined using [theory](05_theories.md#theory-extends-end) (and the keywords `extends` and `end`). Inside theories, [`axiom`](05_theories.md#axiom) can be used with [additional triggers](05_theories.md#semantic-triggers). The construct [`case_split`](05_theories.md#case-split) is also available.
-* Other useful constructs are [`let` [...] `in`](06_control_flow.md#let-in), [`match` [...] `with` [...] `end`](06_control_flow.md#match-with) and [`if` [...] `then` [...] `else` [...]](06_control_flow.md#if-then-else).
+* New theories may be defined using [theory](05_theories.md#user-defined-extensions-of-theories) (and the keywords `extends` and `end`). Inside theories, [`axiom`](03_declaration_of_axioms.md#axiom) can be used with [additional triggers](05_theories.md#semantic-triggers). The construct [`case_split`](05_theories.md#case_split) is also available.
+* Other useful constructs are [`let` [...] `in`](06_control_flow.md#let--in), [`match` [...] `with` [...] `end`](06_control_flow.md#match--with) and [`if` [...] `then` [...] `else` [...]](06_control_flow.md#if--then--else).
 
 The list of all reserved keywords, in alphabetical order, is:
 ```

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)              |
 |--------------|-----------|----------------------|
@@ -53,7 +51,8 @@ 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.
@@ -71,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 *)
@@ -89,7 +88,7 @@ axiom a2: B -> C
 goal g: (B->A) and (C->B) -> (A <-> C)
 ```
 
-### Numeric operators
+## Numeric operators
 
 | Operation               | Notation  | Type(s)                                                                                        |
 |-------------------------|-----------|------------------------------------------------------------------------------------------------|
@@ -102,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                                                                                                            |
 |------------------------- |-------------------------------|------------------------------------------|------------------------------------------------------------------------------------------------------------------|
@@ -128,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`.
 
@@ -143,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 *)
@@ -177,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.
 
@@ -201,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'
@@ -220,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/03_declaration_of_axioms.md

@@ -11,13 +11,13 @@ The heuristic for choosing new instances is based on *triggers*. By default, tri
 In order to declare an axiom, the user can use the following construct.
 Note that axioms must always be named.
 
-#### Syntax
+### Syntax
 ```
 <axiom_declaration> ::= 'axiom' <id> ':' <axiom_body>
 ```
 Here, `<axiom_body>` is an expression which may contain quantifiers, and where user-specified triggers may be added to universal quantifiers.
 
-#### Example
+### Example
 
 ```
 (* Axioms can be used without quantifiers *)
@@ -56,7 +56,7 @@ Interval triggers further restrict instantiation of axioms, and check that varia
 
 Multiple patterns can be used in syntactic triggers. They are separated by `|` which means 'or' and by `,` which means 'and'. `|` has an higher precedence than `,`.
 
-#### Syntax
+### Syntax
 ```
 <quantified_formula>    ::= <quantifier> <var_id_list_sep_comma> ':' <var_type> <syntactic_triggers>? <interval_triggers>? '.' <expr>
 <quantifier>            ::= 'exists' | 'forall'
@@ -75,9 +75,9 @@ Interval triggers also exists. [TODO: add more explanations]
 <rel>                   ::= '<' | '<='
 ```
 
-[Semantic triggers](05_theories.html#semantic-triggers) are only available in theories
+[Semantic triggers](05_theories.md#semantic-triggers) are only available in theories
 
-#### Examples
+### Examples
 ```
 (* P(x) used as the only trigger *)
 logic P,Q,R: int -> prop
@@ -110,13 +110,13 @@ To add a new axiom directly in the form of a rewriting technique, the keyword `r
 
 [TODO: complete]
 
-#### Syntax
+### Syntax
 ```
 <rewriting_declaraction> ::= 'rewriting' <id> ':' <predicate_list_sep_pv>
 <predicate_list_sep_pv>  ::= <predicate> (';' <predicate_list_sep_pv>? )? 
 (* pre-written objects of type predicate can be used, as well as expressions that can be interpreted as predicates *) 
 <predicate>              ::= <predicate_expr> | <predicate_id>
 ```
 
-#### Example
+### Example
 [TODO: find relevant examples]

docs/sphinx_docs/Input_file_formats/Native/04_setting_goals.md

@@ -9,13 +9,13 @@ Alt-Ergo will answer `Valid` if it can prove that the formula of the goal is tru
 To declare goals, the user can use the following construct.
 Note that goals must always be named.
 
-#### Syntax
+### Syntax
 ```
 <goal_declaration> ::= 'goal' <id> ':' <goal_body>
 ```
 Here, `<goal_body>` is an expression which may contain quantifiers.
 
-#### Examples
+### Examples
 ```
 logic h, g, f: int, int -> int
 logic a, b:int
@@ -44,7 +44,7 @@ In other word, `cut` and `check` allow to test if intermediate goals can be prov
 
 [WIP: complete]
 
-#### Syntax
+### Syntax
 ```
 <check_declaration> ::= 'check' <expr>
 <cut_declaration>   ::= 'cut' <expr>