From af1f3a5af08a329f84aff47a3e826a0ba953a04a Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 27 Jul 2023 14:57:51 +0200 Subject: [PATCH 1/3] Update the frontend documentation --- 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..d2e244561 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 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 selected by 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 fully supported by this frontend. + You can select it with the `--frontend dolmen` option. In the future, this + frontend will be used by default. ### Generating models Since 2.5.0, Alt-Ergo also generates models in the case it concludes on the satisfiability of From 073569041f095286c1ee01bf7d0611dc1ef97069 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 27 Jul 2023 15:03:45 +0200 Subject: [PATCH 2/3] Removing the `fully` adjective --- 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 d2e244561..bf2f698eb 100644 --- a/docs/sphinx_docs/Usage/index.md +++ b/docs/sphinx_docs/Usage/index.md @@ -30,7 +30,7 @@ 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 selected by 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 fully supported by this frontend. + The native and SMT-LIB languages are both supported by this frontend. You can select it with the `--frontend dolmen` option. In the future, this frontend will be used by default. From 9f917ecdef1f904ecdb9fcf5c5ccf4fe8eb07c57 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 27 Jul 2023 16:54:24 +0200 Subject: [PATCH 3/3] Review changes --- docs/sphinx_docs/Usage/index.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/sphinx_docs/Usage/index.md b/docs/sphinx_docs/Usage/index.md index bf2f698eb..8858d0a7a 100644 --- a/docs/sphinx_docs/Usage/index.md +++ b/docs/sphinx_docs/Usage/index.md @@ -25,14 +25,14 @@ 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 2.5.0, +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 selected by default. + 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. In the future, this - frontend will be used by default. + 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