From dfa96e7218b49b19a5b7c93458965f1996952925 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Wed, 26 Jul 2023 15:36:39 +0200 Subject: [PATCH 01/11] Fix links in odoc mld files --- src/bin/common/dune | 1 + src/bin/common/index_common.mld | 10 ++++++---- src/bin/text/index.mld | 12 +++++++----- src/parsers/index.mld | 7 +------ src/plugins/AB-Why3/{index_abwhy3.mld => index.mld} | 0 5 files changed, 15 insertions(+), 15 deletions(-) rename src/plugins/AB-Why3/{index_abwhy3.mld => index.mld} (100%) diff --git a/src/bin/common/dune b/src/bin/common/dune index 795a9a45c..9c56361e4 100644 --- a/src/bin/common/dune +++ b/src/bin/common/dune @@ -4,6 +4,7 @@ ) (library + (package alt-ergo) (name alt_ergo_common) (libraries alt-ergo-lib diff --git a/src/bin/common/index_common.mld b/src/bin/common/index_common.mld index 9663dbc72..69b725175 100644 --- a/src/bin/common/index_common.mld +++ b/src/bin/common/index_common.mld @@ -1,8 +1,10 @@ {1 Alt_ergo_common} +See also the {{:Alt_ergo_common/index.html}list of modules}. + {2 Main Solving } -The solving loop is done in the {!module:Alt_ergo_common.solving_loop} module. This module uses the registered input method (parser and typechecker) to compute the input file (see {!section:input}). It relies on initialised options (see {!section:cmdline}). +The solving loop is done in the {!Alt_ergo_common.Solving_loop} module. This module uses the registered input method (parser and typechecker) to compute the input file (see {!section:input}). It relies on initialised options (see {!section:cmdline}). {2:cmdline Command line parsing} @@ -10,14 +12,14 @@ The command line parsing is done with {{:https://erratique.ch/software/cmdliner} {2:input Input Frontend } -The {!module:Alt_ergo_common.input_frontend} module register an input method capable of parsing and typechecking the input files +The {!module:Alt_ergo_common.Input_frontend} module register an input method capable of parsing and typechecking the input files The legacy frontend is used to parse and typecheck file with the native Alt-Ergo syntaxe and also the smtlib2 and psmt2 syntaxe. {2:signals Signals and profiling } -The {!module:Alt_ergo_common.signals_profiling} module initialise handlers for system signals and profiling informations and timers. +The {!module:Alt_ergo_common.Signals_profiling} module initialise handlers for system signals and profiling informations and timers. {2:dynlink Stdlib wrapper} -{!modules:Alt_ergo_common.MyDynlink} +See {!Alt_ergo_common.MyDynlink} diff --git a/src/bin/text/index.mld b/src/bin/text/index.mld index bd452abf3..390dff19c 100644 --- a/src/bin/text/index.mld +++ b/src/bin/text/index.mld @@ -9,14 +9,16 @@ is available through the {e --help} option. 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. +See also the {{:Alt_ergo_common/index.html}list of modules}. + {3 Plugins} {4 Why3 parser} -for the Why3 parser plugin documentation see -{{:index_abwhy3.html} - [ABWhy3]} +For the Why3 parser plugin documentation see +{{:../alt-ergo-plugin-ab-why3/index.html} + [ABWhy3]}. {4 Fourier Motzkin simplex} -for the Fourier Motzkin simplex plugin documentation see +For the Fourier Motzkin simplex plugin documentation see {{:index_fmsimplex.html} - [FMsimplex]} + [FMsimplex]}. diff --git a/src/parsers/index.mld b/src/parsers/index.mld index b96e518a6..ae57fc2e1 100644 --- a/src/parsers/index.mld +++ b/src/parsers/index.mld @@ -25,10 +25,5 @@ Users can add new parsers to Alt-Ergo with the option [--add-parser]. This parser should have the same interface as {!module-type:AltErgoParsers.Parsers.PARSER_INTERFACE} and should be registered using {!val:AltErgoParsers.Parsers.register_parser} {4 Why3 parser plugin} -see {{:../alt-ergo/index_abwhy3.html}[ABWhy3]} - -{2 Utilities} -{!modules: -AltErgoParsers.MyZip -} +See {{:../alt-ergo-plugin-ab-why3/index.html}[the ABWhy3 plugin]}. diff --git a/src/plugins/AB-Why3/index_abwhy3.mld b/src/plugins/AB-Why3/index.mld similarity index 100% rename from src/plugins/AB-Why3/index_abwhy3.mld rename to src/plugins/AB-Why3/index.mld From bd3124483b558dfad02aa6d634ccbed56900307d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Wed, 26 Jul 2023 15:49:25 +0200 Subject: [PATCH 02/11] Fix dead links and compilation warnings in sphinx doc --- .../Input_file_formats/Native/00_summary.md | 6 +++--- .../Native/02_types/02_01_builtin.md | 1 + .../Native/03_declaration_of_axioms.md | 14 +++++++------- .../Input_file_formats/Native/04_setting_goals.md | 6 +++--- .../Input_file_formats/Native/05_theories.md | 2 +- .../Input_file_formats/Native/06_control_flow.md | 12 ++++++------ 6 files changed, 21 insertions(+), 20 deletions(-) diff --git a/docs/sphinx_docs/Input_file_formats/Native/00_summary.md b/docs/sphinx_docs/Input_file_formats/Native/00_summary.md index 66486bf9c..993d23239 100644 --- a/docs/sphinx_docs/Input_file_formats/Native/00_summary.md +++ b/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: ``` diff --git a/docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md b/docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md index 9f809d208..bd95d8d64 100644 --- a/docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md +++ b/docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md @@ -53,6 +53,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 Prior to Alt-Ergo 2.3.0, Alt-Ergo's native language handled differently boolean variables `bool` and propositional variables `prop`. diff --git a/docs/sphinx_docs/Input_file_formats/Native/03_declaration_of_axioms.md b/docs/sphinx_docs/Input_file_formats/Native/03_declaration_of_axioms.md index 2cea18941..de0c8ea39 100644 --- a/docs/sphinx_docs/Input_file_formats/Native/03_declaration_of_axioms.md +++ b/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' ':' ``` Here, `` 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 ``` ::= ':' ? ? '.' ::= 'exists' | 'forall' @@ -75,9 +75,9 @@ Interval triggers also exists. [TODO: add more explanations] ::= '<' | '<=' ``` -[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,7 +110,7 @@ To add a new axiom directly in the form of a rewriting technique, the keyword `r [TODO: complete] -#### Syntax +### Syntax ``` ::= 'rewriting' ':' ::= (';' ? )? @@ -118,5 +118,5 @@ To add a new axiom directly in the form of a rewriting technique, the keyword `r ::= | ``` -#### Example +### Example [TODO: find relevant examples] diff --git a/docs/sphinx_docs/Input_file_formats/Native/04_setting_goals.md b/docs/sphinx_docs/Input_file_formats/Native/04_setting_goals.md index 68a43f7fa..bc178c3e0 100644 --- a/docs/sphinx_docs/Input_file_formats/Native/04_setting_goals.md +++ b/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' ':' ``` Here, `` 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' ::= 'cut' diff --git a/docs/sphinx_docs/Input_file_formats/Native/05_theories.md b/docs/sphinx_docs/Input_file_formats/Native/05_theories.md index fe7220023..4354becad 100644 --- a/docs/sphinx_docs/Input_file_formats/Native/05_theories.md +++ b/docs/sphinx_docs/Input_file_formats/Native/05_theories.md @@ -54,7 +54,7 @@ More information on this strategy and the language extension can be found in [th ### Semantic triggers -In addition to syntactic triggers (or triggers) and interval triggers (or filters) defined in [section Axioms](03_declaration_of_axioms.md), additional triggers are available inside theories. +In addition to syntactic triggers (or triggers) and interval triggers (or filters) defined in [axioms](03_declaration_of_axioms.md), additional triggers are available inside theories. Those additional triggers are called semantic triggers. They correspond to the following constructs. diff --git a/docs/sphinx_docs/Input_file_formats/Native/06_control_flow.md b/docs/sphinx_docs/Input_file_formats/Native/06_control_flow.md index 578a124e9..d544a2010 100644 --- a/docs/sphinx_docs/Input_file_formats/Native/06_control_flow.md +++ b/docs/sphinx_docs/Input_file_formats/Native/06_control_flow.md @@ -7,13 +7,13 @@ Like in OCaml, let expressions are available. They allow for named local expressions, which are written `let name = expression in [...]`. Name defined like this only have local scope. -#### Syntax +### Syntax ``` ::= 'let' 'in' ::= '=' ( ',' '=' )* ``` -#### Example +### Example ``` function average(a:real, b:real):real = let sum = a+b in @@ -27,7 +27,7 @@ Pattern matching, a [Really Cool Feature](https://ocaml.org/learn/tutorials/data Warning: the only patterns that can be matched are constructors of algebraic datatypes. Moreover, constructors can't be nested in a pattern. -#### Syntax +### Syntax ``` ::= 'match' 'with' 'end' ::= '|'? '->' ( '|' '->' )* @@ -35,7 +35,7 @@ Moreover, constructors can't be nested in a pattern. ::= ( "," )* ``` -#### Example +### Example ``` type 'a tree = NIL | Node of { left:'a tree; val:'a; right:'a tree } @@ -53,7 +53,7 @@ function height(t: 'a tree):int = The simple construct `if then else` for conditional expressions is available in Alt-Ergo's native language. -#### Syntax +### Syntax ``` ::= 'if' 'then' 'else' (* Note that must have type bool - or prop *) @@ -63,7 +63,7 @@ The simple construct `if then else` for conditional expressions is available in ::= ``` -#### Example +### Example ``` function max(a:int, b:int):int = if a>b then a else b From 42f7f7b1999eebc8e6efffd7aee5822fb97f1ba5 Mon Sep 17 00:00:00 2001 From: Pierrot Date: Thu, 27 Jul 2023 11:52:08 +0200 Subject: [PATCH 03/11] Update dependencies (#760) * Update the opam file for Dolmen 0.9 * Update the documentation * remove the pin for Dolmen --- alt-ergo-lib.opam | 21 +++------------------ alt-ergo-lib.opam.template | 15 --------------- docs/sphinx_docs/Install/index.md | 17 ++++++++++++----- dune-project | 6 +++--- 4 files changed, 18 insertions(+), 41 deletions(-) diff --git a/alt-ergo-lib.opam b/alt-ergo-lib.opam index 1bffd419d..1c1da3884 100644 --- a/alt-ergo-lib.opam +++ b/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" - ] -] diff --git a/alt-ergo-lib.opam.template b/alt-ergo-lib.opam.template index ac6375ca6..cde1fa1b8 100644 --- a/alt-ergo-lib.opam.template +++ b/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" - ] -] diff --git a/docs/sphinx_docs/Install/index.md b/docs/sphinx_docs/Install/index.md index a065d4f6b..a43926dc7 100644 --- a/docs/sphinx_docs/Install/index.md +++ b/docs/sphinx_docs/Install/index.md @@ -25,18 +25,25 @@ External dependencies graph generated with `dune-deps` (use `make archi` for sou ![](deps.png) -To compile the sources, you will need the following libraries : +To compile the sources of the library `alt-ergo-lib` and the binary `alt-ergo`, you will need the +following libraries : ``` ocaml >= 4.08.0 dune >= 3.0 - zarith >= 1.4 - camlzip - menhir + dune-build-info + dolmen >= 0.9 + dolmen_loop >= 0.9 ocplib-simplex >= 0.5 + zarith >= 1.4 seq + fmt + ppx_blob + camlzip >= 1.07 + menhir + dune-site cmdliner + psmt2-frontend >= 0.4 stdlib-shims - psmt2-frontend ``` You can install dependencies using: diff --git a/dune-project b/dune-project index 251d40b4e..ad75c3605 100644 --- a/dune-project +++ b/dune-project @@ -77,9 +77,9 @@ See more details on http://alt-ergo.ocamlpro.com/" (ocaml (>= 4.08.0)) dune 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 From bf6c6dbcad6b2a7e52cf433727bd755583d6adcb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <129742207+bclement-ocp@users.noreply.github.com> Date: Thu, 27 Jul 2023 12:04:49 +0000 Subject: [PATCH 04/11] [doc] Document the floating-point and bitvector primitives (#762) --- docs/sphinx_docs/About/changes.md | 4 + .../Native/02_types/02_01_builtin.md | 105 ++++++++++++++---- .../Input_file_formats/Native/05_theories.md | 79 ++++++++++++- .../Input_file_formats/SMT-LIB2/index.md | 22 ++++ docs/sphinx_docs/Input_file_formats/index.rst | 5 +- docs/sphinx_docs/Plugins/ab_why3.md | 2 +- docs/sphinx_docs/Usage/index.md | 6 - src/bin/text/index.mld | 4 +- 8 files changed, 191 insertions(+), 36 deletions(-) create mode 100644 docs/sphinx_docs/Input_file_formats/SMT-LIB2/index.md diff --git a/docs/sphinx_docs/About/changes.md b/docs/sphinx_docs/About/changes.md index 2bf6f717c..345b27241 100644 --- a/docs/sphinx_docs/About/changes.md +++ b/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 ``` diff --git a/docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md b/docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md index bd95d8d64..164af1616 100644 --- a/docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md +++ b/docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md @@ -1,36 +1,34 @@ -# 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). @@ -38,9 +36,9 @@ Creation and manipulation of values having those types are covered in [built-in 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`,
`real, int -> real`,
`int, real -> real`,
`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}`
where 0<=p<=q ::= 'farray' @@ -221,7 +284,7 @@ Remember that `farray` are parametrized by two types: the type of their indexes ::= '[' '<-' ( ',' '<-' )* ']' ``` -#### Examples +### Examples ``` (* arr1 is a general polymorphic farray *) logic arr1: ('a, 'b) farray diff --git a/docs/sphinx_docs/Input_file_formats/Native/05_theories.md b/docs/sphinx_docs/Input_file_formats/Native/05_theories.md index 4354becad..8815262e4 100644 --- a/docs/sphinx_docs/Input_file_formats/Native/05_theories.md +++ b/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 diff --git a/docs/sphinx_docs/Input_file_formats/SMT-LIB2/index.md b/docs/sphinx_docs/Input_file_formats/SMT-LIB2/index.md new file mode 100644 index 000000000..b15c7c164 --- /dev/null +++ b/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. diff --git a/docs/sphinx_docs/Input_file_formats/index.rst b/docs/sphinx_docs/Input_file_formats/index.rst index 1ef7276c3..5d88d04ed 100644 --- a/docs/sphinx_docs/Input_file_formats/index.rst +++ b/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 - SMT-LIB - WhyML (partial support) + SMT-LIB diff --git a/docs/sphinx_docs/Plugins/ab_why3.md b/docs/sphinx_docs/Plugins/ab_why3.md index 42fb4497b..64d75552e 100644 --- a/docs/sphinx_docs/Plugins/ab_why3.md +++ b/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 ? diff --git a/docs/sphinx_docs/Usage/index.md b/docs/sphinx_docs/Usage/index.md index 33ac75f65..07749314e 100644 --- a/docs/sphinx_docs/Usage/index.md +++ b/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 - ### Plugins and Preludes directories As stated above, the `--where` option of `alt-ergo` can be used to get the absolute diff --git a/src/bin/text/index.mld b/src/bin/text/index.mld index 390dff19c..5aeb29ed9 100644 --- a/src/bin/text/index.mld +++ b/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}. From 97930cb7463a0e78bf2d13de63bfcaf5d7bdbf46 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <129742207+bclement-ocp@users.noreply.github.com> Date: Thu, 27 Jul 2023 12:08:37 +0000 Subject: [PATCH 05/11] [frontend] Use the dolmen frontend by default with --produce-models (#764) Since --produce-models is intended to be used with `(get-model)` in the SMT-LIB format, it only makes sense to use a frontend that actually supports `(get-model)` when the option is provided. (Reported by @Halbaroth) --- src/bin/common/parse_command.ml | 45 +++++++++++++++++++++++---------- 1 file changed, 32 insertions(+), 13 deletions(-) diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index dca512b3b..41a543b80 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -296,7 +296,7 @@ let mk_context_opt replay replay_all_used_context replay_used_context set_replay_used_context replay_used_context; `Ok() -let mk_execution_opt frontend input_format parse_only () +let mk_execution_opt input_format parse_only () preludes no_locs_in_answers colors_in_output no_headers_in_output no_formatting_in_output no_forced_flush_in_output pretty_output type_only type_smt2 @@ -319,7 +319,6 @@ let mk_execution_opt frontend input_format parse_only () set_output_with_forced_flush output_with_forced_flush; set_input_format input_format; set_parse_only parse_only; - set_frontend frontend; set_type_only type_only; set_type_smt2 type_smt2; set_preludes preludes; @@ -368,7 +367,7 @@ let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation let mk_output_opt interpretation use_underscore unsat_core output_format model_type - () () + () () () = set_infer_output_format (Option.is_none output_format); let output_format = match output_format with @@ -617,12 +616,6 @@ let parse_execution_opt = let docs = s_execution in - let frontend = - let doc = "Select the parsing and typing frontend." in - let docv = "FTD" in - Arg.(value & opt string (get_frontend ()) & - info ["frontend"] ~docv ~docs ~doc) in - let input_format = let doc = Format.sprintf "Set the default input format to $(docv) and must be %s. \ @@ -741,7 +734,7 @@ let parse_execution_opt = Term.(ret (const mk_execution_opt $ - frontend $ input_format $ parse_only $ parsers $ preludes $ + input_format $ parse_only $ parsers $ preludes $ no_locs_in_answers $ colors_in_output $ no_headers_in_output $ no_formatting_in_output $ no_forced_flush_in_output $ pretty_output $ type_only $ type_smt2 @@ -855,7 +848,7 @@ let parse_output_opt = (* Use the --interpretation and --produce-models (which is equivalent to --interpretation last) to determine the interpretation value. *) - let interpretation, dump_models = + let interpretation, dump_models, frontend = let interpretation = let doc = Format.sprintf "Best effort support for counter-example generation. \ @@ -888,6 +881,26 @@ let parse_output_opt = Arg.(value & flag & info ["produce-models"] ~doc ~docs:s_models) in + let frontend = + let doc = "Select the parsing and typing frontend." in + let docv = "FTD" in + Arg.(value & opt (some string) None & + info ["frontend"] ~docv ~docs:s_execution ~doc) + in + + (* Use the dolmen frontend by default with --produce-models *) + let mk_frontend frontend produce_models = + match frontend with + | None -> + if produce_models then + "dolmen" + else + get_frontend () + | Some frontend -> frontend + in + + let frontend = Term.(const mk_frontend $ frontend $ produce_models) in + let dump_models = let doc = "Display a model each time the result is unknown (implies \ @@ -905,7 +918,8 @@ let parse_output_opt = const mk_interpretation $ interpretation $ produce_models $ dump_models ), - dump_models + dump_models, + frontend in (* Use the --sat-solver to determine the sat solver. @@ -1054,10 +1068,15 @@ let parse_output_opt = Term.(const set_dump_models $ dump_models) in + let set_frontend = + Term.(const set_frontend $ frontend) + in + Term.(ret (const mk_output_opt $ interpretation $ use_underscore $ unsat_core $ output_format $ model_type $ - set_dump_models $ set_sat_options + set_dump_models $ set_sat_options $ + set_frontend )) let parse_profiling_opt = From ca84eab15244f6c4b1e48009c99b84f8518ba68a Mon Sep 17 00:00:00 2001 From: Pierrot Date: Thu, 27 Jul 2023 16:01:08 +0200 Subject: [PATCH 06/11] Clean up documentation (#765) * Keep the default width of the rtd-theme * Improve conf.py * Clarify input file formats * Fix spelling * Review changes * Doublon * Revert removing _static directory --- docs/sphinx_docs/Input_file_formats/index.rst | 15 +++++++++++---- docs/sphinx_docs/_static/.gitkeep | 0 docs/sphinx_docs/_static/css/dac_theme_modif.css | 8 -------- docs/sphinx_docs/conf.py | 9 +++------ 4 files changed, 14 insertions(+), 18 deletions(-) create mode 100644 docs/sphinx_docs/_static/.gitkeep delete mode 100644 docs/sphinx_docs/_static/css/dac_theme_modif.css diff --git a/docs/sphinx_docs/Input_file_formats/index.rst b/docs/sphinx_docs/Input_file_formats/index.rst index 5d88d04ed..5a4c44ca8 100644 --- a/docs/sphinx_docs/Input_file_formats/index.rst +++ b/docs/sphinx_docs/Input_file_formats/index.rst @@ -3,11 +3,18 @@ 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 through the :doc:`AB-Why3 plugin <../Plugins/ab_why3>`. +Alt-ergo supports different input languages: + +- The original input language is its native language, based on the language of the Why3 platform and + detailed below. +- Alt-ergo supports the SMT-LIB language v2.6. Since 2.5.0, improved support + is provided by the `Dolmen `_ frontend, available with + the `--frontend dolmen` option. +- 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 - SMT-LIB + + Alt-Ergo's native language + SMT-LIB 2 diff --git a/docs/sphinx_docs/_static/.gitkeep b/docs/sphinx_docs/_static/.gitkeep new file mode 100644 index 000000000..e69de29bb diff --git a/docs/sphinx_docs/_static/css/dac_theme_modif.css b/docs/sphinx_docs/_static/css/dac_theme_modif.css deleted file mode 100644 index ba4584a84..000000000 --- a/docs/sphinx_docs/_static/css/dac_theme_modif.css +++ /dev/null @@ -1,8 +0,0 @@ -/* Theme modification for the documentation included in Try-Alt-Ergo (Doc-Alt-Ergo). - * The original theme is sphinx_rtd_theme - */ - -/* Used for larger body */ -.wy-nav-content { - max-width: 1200px !important; -} diff --git a/docs/sphinx_docs/conf.py b/docs/sphinx_docs/conf.py index 3ee83db4a..cf504c2a3 100644 --- a/docs/sphinx_docs/conf.py +++ b/docs/sphinx_docs/conf.py @@ -17,9 +17,9 @@ # -- Project information ----------------------------------------------------- -project = 'Doc-Alt-Ergo' -copyright = '2020 - 2023, Alt-Ergo devs' -author = 'Alt-Ergo devs' +project = 'Alt-Ergo Documentation' +copyright = '2020 - 2023, Alt-Ergo developers' +author = 'Alt-Ergo developers' # -- Entry point ------------------------------------------------------------- @@ -56,9 +56,6 @@ html_show_sourcelink = False -def setup(app): - app.add_css_file('css/dac_theme_modif.css') - # Add any paths that contain custom static files (such as style sheets) here, # relative to this directory. They are copied after the builtin static files, # so a file named "default.css" will overwrite the builtin "default.css". From b1c804002b82221853ae1a631819a9e5ca5d2278 Mon Sep 17 00:00:00 2001 From: Pierrot Date: Thu, 27 Jul 2023 17:00:49 +0200 Subject: [PATCH 07/11] Frontend documentation (#766) * Update the frontend documentation * Removing the `fully` adjective * Review changes --- docs/sphinx_docs/Usage/index.md | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/docs/sphinx_docs/Usage/index.md b/docs/sphinx_docs/Usage/index.md index 07749314e..8858d0a7a 100644 --- a/docs/sphinx_docs/Usage/index.md +++ b/docs/sphinx_docs/Usage/index.md @@ -21,7 +21,18 @@ Alt-Ergo supports file extensions: - `.psmt2`, `.smt2` for (our polymorphic extension of) the SMT-LIB 2 standard -See the [Input section] for more information about the format of the input files +See the [Input section] for more information about the format of the input files. + +### Frontend option + +The `--frontend` option let's you select the frontend used to parse and type the input file. Since version 2.5.0, +Alt-Ergo integrates two frontends: +- The `legacy` frontend is the historical frontend of Alt-Ergo supporting the native language + and (partially) supporting the SMT-LIB language. The legacy frontend is currently the default. +- The `dolmen` frontend is a new frontend using the [Dolmen library](https://github.com/Gbury/dolmen). + The native and SMT-LIB languages are both supported by this frontend. + You can select it with the `--frontend dolmen` option, which is planned to become the + default in a future release. ### Generating models Since 2.5.0, Alt-Ergo also generates models in the case it concludes on the satisfiability of From 0d3a703613baf90fdee6ff13c97e1981ab98ddd3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <129742207+bclement-ocp@users.noreply.github.com> Date: Thu, 27 Jul 2023 19:37:54 +0000 Subject: [PATCH 08/11] [doc] Fix documentation typo (#768) --- docs/sphinx_docs/Usage/index.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/sphinx_docs/Usage/index.md b/docs/sphinx_docs/Usage/index.md index 8858d0a7a..e0bafefc5 100644 --- a/docs/sphinx_docs/Usage/index.md +++ b/docs/sphinx_docs/Usage/index.md @@ -25,7 +25,7 @@ See the [Input section] for more information about the format of the input files ### Frontend option -The `--frontend` option let's you select the frontend used to parse and type the input file. Since version 2.5.0, +The `--frontend` option lets you select the frontend used to parse and type the input file. Since version 2.5.0, Alt-Ergo integrates two frontends: - The `legacy` frontend is the historical frontend of Alt-Ergo supporting the native language and (partially) supporting the SMT-LIB language. The legacy frontend is currently the default. From 4e2dded167358ddcd2598992b8d1cf8ed9ea9909 Mon Sep 17 00:00:00 2001 From: Pierrot Date: Fri, 28 Jul 2023 10:24:55 +0200 Subject: [PATCH 09/11] Update model documentation (#759) * Update model documentation * Review changes * Review changes bis * Review changes ter * Clarify the dolmen option --- docs/sphinx_docs/Usage/index.md | 129 +++++++++++++++++++++++++++----- 1 file changed, 112 insertions(+), 17 deletions(-) diff --git a/docs/sphinx_docs/Usage/index.md b/docs/sphinx_docs/Usage/index.md index e0bafefc5..4ee753576 100644 --- a/docs/sphinx_docs/Usage/index.md +++ b/docs/sphinx_docs/Usage/index.md @@ -35,22 +35,117 @@ Alt-Ergo integrates two frontends: default in a future release. ### Generating models -Since 2.5.0, Alt-Ergo also generates models in the case it concludes on the satisfiability of -the formula. -There is two ways to activate model generation: - -- with the `--model` option; - -- `with the --interpretation=VALUE`, where VALUE can be equal to: - * "none", and alt-ergo will not generate models (by default); - * "first", and alt-ergo will output the first model it finds; - * "every", alt alt-ergo will compute a model before each decision - * "last", and alt-ergo will output the last model it computes before returning 'unknown'. - Note that this mode only works with the option `--sat-solver tableaux`. - -NB: the `--model` option is equivalent to `--interpretation every --sat-solver tableaux`. - -The default model format is the SMT format. +Alt-Ergo can generates best-effort models in the case it cannot conclude the unsatisfiability of +the context. The model format is a SMT-LIB compatible format, even if you use the native input language. + +#### Activation + +Model generation is disabled by default. There are two recommended ways to enable it: +- with the native language and the `--dump-models` option, Alt-Ergo tries to produce + a model after each `check_sat` that returns `I don't known` or + a counter-example after each `goal` it cannot prove `valid`. Note that both + `goal` and `check_sat` statements are independent in the native language. + +- with the SMT-LIB language and the `--produce-models` option, Alt-Ergo tries to + produce a model after each `(check-sat)` that returns `unknown`. Models are output + on demand using the statement `(get-model)`. + + Alternatively, you can enable model generation using the statement + `(set-option :produce-models true)`. This currently requires using the options + `--sat-solver tableaux` and `--frontend dolmen`. + +#### Examples + + Using the native language in the input file `INPUT.ae`: + + ``` + logic a, b, c : int + axiom A : a <> c + + check_sat c1: a = b + c + check_sat c2: a <> b + ``` + and the command `alt-ergo --dump-models INPUT.ae`, Alt-Ergo produces the + output models: + + ``` + ; Model for c1 + ( + (define-fun a () Int 2) + (define-fun b () Int 2) + (define-fun c () Int 0) + ) + I don't known + + ; Model for c2 + ( + (define-fun a () Int 2) + (define-fun b () Int 0) + (define-fun c () Int 0) + ) + I don't known + ``` + *Note*: In this example the model for the statement `check_sat c2` is not a + model for the statement `check_sat c1` since `check_sat` are independent in + the native language. The same goes for `goals`. + + Using the SMT-LIB language in the input file `INPUT.smt2`: + + ``` + (set-logic ALL) + (declare-fun a () Int) + (declare-fun b () Int) + (declare-fun c () Int) + + (assert (= a (+ b c))) + (check-sat) + (get-model) + + (assert (distinct a b)) + (check-sat) + + ``` + and the command `alt-ergo --produce-models INPUT.smt2` produces the output + ``` + unknown + ( + (define-fun a () Int 0) + (define-fun b () Int 0) + (define-fun c () Int 0) + ) + + unknown + ``` + *Note*: There is no model printed after the second `(check-sat)` since we + don't demand it with the statement `(get-model)`. + + Alternatively, using the statement `(set-option :produce-models true)` + ``` + (set-logic ALL) + (set-option :produce-models true) + (declare-fun a () Int) + (declare-fun b () Int) + (declare-fun c () Int) + + (assert (= a (+ b c))) + (check-sat) + (get-model) + + ``` + and the command `alt-ergo --frontend dolmen --sat-solver tableaux INPUT.smt2` produces + the output model + ``` + unknown + ( + (define-fun a () Int 0) + (define-fun b () Int 0) + (define-fun c () Int 0) + ) + ``` + *Note*: you need to select the Dolmen frontend and the SAT solver Tableaux as the + model generation is not supported yet by the other SAT solvers. The options + `--dump-models` and `--produce-models` select the right frontend and SAT solver + for you. ### Output The results of an Alt-ergo's execution have the following form : @@ -143,7 +238,7 @@ The worker also take a Json file that correspond to the options to set in Alt-Er "steps_bound": 1000 } ``` -#### Outpus +#### Outputs At the end of solving it returns a Json file corresponding to results, debug informations, etc: From ec67eacb7aa30c74b5d938aabac0cfc7e6ab2433 Mon Sep 17 00:00:00 2001 From: Pierrot Date: Fri, 28 Jul 2023 12:11:25 +0200 Subject: [PATCH 10/11] Add block for the notes (#769) --- docs/sphinx_docs/Input_file_formats/index.rst | 4 +-- docs/sphinx_docs/Usage/index.md | 36 +++++++++++++------ 2 files changed, 27 insertions(+), 13 deletions(-) diff --git a/docs/sphinx_docs/Input_file_formats/index.rst b/docs/sphinx_docs/Input_file_formats/index.rst index 5a4c44ca8..c368ebdc3 100644 --- a/docs/sphinx_docs/Input_file_formats/index.rst +++ b/docs/sphinx_docs/Input_file_formats/index.rst @@ -7,9 +7,9 @@ Alt-ergo supports different input languages: - The original input language is its native language, based on the language of the Why3 platform and detailed below. -- Alt-ergo supports the SMT-LIB language v2.6. Since 2.5.0, improved support +- Alt-ergo supports the SMT-LIB language v2.6. Since version 2.5.0, improved support is provided by the `Dolmen `_ frontend, available with - the `--frontend dolmen` option. + the ``--frontend dolmen`` option. - It also (partially) supports the input language of Why3 through the :doc:`AB-Why3 plugin <../Plugins/ab_why3>`. .. toctree:: diff --git a/docs/sphinx_docs/Usage/index.md b/docs/sphinx_docs/Usage/index.md index 4ee753576..de82ac051 100644 --- a/docs/sphinx_docs/Usage/index.md +++ b/docs/sphinx_docs/Usage/index.md @@ -56,7 +56,7 @@ Model generation is disabled by default. There are two recommended ways to enabl #### Examples - Using the native language in the input file `INPUT.ae`: + - Using the native language in the input file `INPUT.ae`: ``` logic a, b, c : int @@ -85,11 +85,16 @@ Model generation is disabled by default. There are two recommended ways to enabl ) I don't known ``` - *Note*: In this example the model for the statement `check_sat c2` is not a + + ```{admonition} Note + + In this example the model for the statement `check_sat c2` is not a model for the statement `check_sat c1` since `check_sat` are independent in the native language. The same goes for `goals`. - Using the SMT-LIB language in the input file `INPUT.smt2`: + ``` + + - Using the SMT-LIB language in the input file `INPUT.smt2`: ``` (set-logic ALL) @@ -116,10 +121,15 @@ Model generation is disabled by default. There are two recommended ways to enabl unknown ``` - *Note*: There is no model printed after the second `(check-sat)` since we + + ```{admonition} Note + + There is no model printed after the second `(check-sat)` since we don't demand it with the statement `(get-model)`. + ``` + - Alternatively, using the statement `(set-option :produce-models true)` + - Alternatively, using the statement `(set-option :produce-models true)` ``` (set-logic ALL) (set-option :produce-models true) @@ -142,10 +152,13 @@ Model generation is disabled by default. There are two recommended ways to enabl (define-fun c () Int 0) ) ``` - *Note*: you need to select the Dolmen frontend and the SAT solver Tableaux as the + + ```{admonition} Note + You need to select the Dolmen frontend and the SAT solver Tableaux as the model generation is not supported yet by the other SAT solvers. The options `--dump-models` and `--produce-models` select the right frontend and SAT solver for you. + ``` ### Output The results of an Alt-ergo's execution have the following form : @@ -154,11 +167,12 @@ File "/", line , characters : (