diff --git a/CHANGES.md b/CHANGES.md index 17a25cace9..fb1b736ad7 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,5 +1,7 @@ ## unreleased + ### Deprecated +* make Dolmen the default and deprecate the legacy frontend (PR #857) * printing underscore instead of fresh value in model (PR #805) ### Build 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 164af1616b..811e78776a 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 @@ -141,8 +141,8 @@ 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. +*Note*: `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 @@ -156,9 +156,9 @@ 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. +*Note*: `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 diff --git a/docs/sphinx_docs/Input_file_formats/SMT-LIB2/index.md b/docs/sphinx_docs/Input_file_formats/SMT-LIB2/index.md index b15c7c164b..630aa83809 100644 --- a/docs/sphinx_docs/Input_file_formats/SMT-LIB2/index.md +++ b/docs/sphinx_docs/Input_file_formats/SMT-LIB2/index.md @@ -6,16 +6,13 @@ standard](http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.p 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. +provided by the new [Dolmen](http://gbury.github.io/dolmen/) frontend. ## 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. +theory and the `QF_BV` and `BV` logics. 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 diff --git a/docs/sphinx_docs/Usage/index.md b/docs/sphinx_docs/Usage/index.md index efdcdacaaf..646c41df8f 100644 --- a/docs/sphinx_docs/Usage/index.md +++ b/docs/sphinx_docs/Usage/index.md @@ -27,12 +27,19 @@ See the [Input section] for more information about the format of the input files 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. -- 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. +- The `dolmen` frontend is the default frontend, powered by the + [Dolmen](https://github.com/Gbury/dolmen) library. The native and SMT-LIB + languages are both supported by this frontend. +- The `legacy` frontend is the historical frontend of Alt-Ergo supporting the + native language. You can select it with the `--frontend legacy` option. The + legacy frontend is deprecated, and will be removed in a future release. + +```{admonition} Note + +The `legacy` frontend has limited support for the SMT-LIB language, but many +SMT-LIB features will not work with the `legacy` frontend. Use the (default) +`dolmen` frontend for SMT-LIB inputs. +``` ### Generating models Alt-Ergo can generates best-effort models in the case it cannot conclude the unsatisfiability of @@ -51,8 +58,7 @@ Model generation is disabled by default. There are two recommended ways to enabl 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 option - `--frontend dolmen`. + `(set-option :produce-models true)`. #### Examples @@ -142,7 +148,7 @@ Model generation is disabled by default. There are two recommended ways to enabl (get-model) ``` - and the command `alt-ergo --frontend dolmen INPUT.smt2` produces + and the command `alt-ergo INPUT.smt2` produces the output model ``` unknown @@ -153,11 +159,6 @@ Model generation is disabled by default. There are two recommended ways to enabl ) ``` - ```{admonition} Note - You need to select the Dolmen frontend. The options `--dump-models` and - `--produce-models` select the right frontend for you. - ``` - - As a more didactic example, let us imagine while checking the loop invariant in the pseudocode below: ``` @@ -177,7 +178,7 @@ Model generation is disabled by default. There are two recommended ways to enabl ``` Execute the command ```sh - alt-ergo --frontend dolmen --produce-models INPUT.smt2 + alt-ergo --produce-models INPUT.smt2 ``` We got the output ```