From 8da4e00c271dfa5918242bcf3d8cf4969369b4d5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Tue, 3 Oct 2023 15:12:43 +0200 Subject: [PATCH 1/2] Make Dolmen the default frontend The current plan is for Dolmen to be the default frontend in the next release. Making the switch as early as possible in the development branch will help us use it and test it more. --- src/bin/common/parse_command.ml | 26 ++++++++++---------------- src/lib/util/options.ml | 2 +- tests/cram.t/run.t | 27 ++++++++++----------------- 3 files changed, 21 insertions(+), 34 deletions(-) diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index 9c6c9e3d2..fc6947dd3 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -879,25 +879,19 @@ let parse_output_opt = let frontend = - let doc = "Select the parsing and typing frontend." in + let doc = + "Select the parsing and typing frontend. Support for non-default \ + frontends is deprecated and will be removed in the next release." + 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 + let deprecated = + "this option is deprecated and will be ignored in the \ + next version" + in + Arg.(value & opt string "dolmen" & + info ["frontend"] ~docv ~docs:s_execution ~doc ~deprecated) 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 \ diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index 00c821688..70fac991f 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -259,7 +259,7 @@ let output_with_colors = ref false let output_with_headers = ref true let output_with_formatting = ref true let output_with_forced_flush = ref true -let frontend = ref "legacy" +let frontend = ref "dolmen" let input_format = ref None let parse_only = ref false let preludes = ref [] diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t index 187dc2748..ff932c959 100644 --- a/tests/cram.t/run.t +++ b/tests/cram.t/run.t @@ -6,7 +6,7 @@ Now we will have some tests for the models. Note that it is okay if the format changes slightly, you should be concerned with ensuring the semantic is appropriate here. - $ alt-ergo --frontend dolmen --produce-models model555.smt2 --no-forced-flush-in-output 2>/dev/null + $ alt-ergo --produce-models model555.smt2 --no-forced-flush-in-output 2>/dev/null unknown ( @@ -17,14 +17,7 @@ appropriate here. Now we will test some semantic triggers. - $ alt-ergo --frontend legacy -o smtlib2 semantic_triggers.ae 2>/dev/null - - unknown - - unsat - - unsat - $ alt-ergo --frontend dolmen -o smtlib2 semantic_triggers.ae 2>/dev/null + $ alt-ergo -o smtlib2 semantic_triggers.ae 2>/dev/null unknown @@ -34,7 +27,7 @@ Now we will test some semantic triggers. And some SMT2 action. - $ alt-ergo --frontend dolmen -o smtlib2 --prelude prelude.ae postlude.smt2 2>/dev/null + $ alt-ergo -o smtlib2 --prelude prelude.ae postlude.smt2 2>/dev/null unknown @@ -50,37 +43,37 @@ combinations of produce-models et al. First, if model generation is not enabled, we should error out when a `(get-model)` statement is issued: - $ echo '(get-model)' | alt-ergo --frontend dolmen -i smtlib2 -o smtlib2 + $ echo '(get-model)' | alt-ergo -i smtlib2 -o smtlib2 (error "Model generation disabled (try --produce-models)") This should be the case Tableaux solver as well: - $ echo '(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2 + $ echo '(get-model)' | alt-ergo --sat-solver Tableaux -i smtlib2 -o smtlib2 (error "Model generation disabled (try --produce-models)") The messages above mention `--produce-models`, but we can also use `set-option`. - $ echo '(get-model)' | alt-ergo --frontend dolmen --produce-models -i smtlib2 -o smtlib2 + $ echo '(get-model)' | alt-ergo --produce-models -i smtlib2 -o smtlib2 (error "No model produced.") - $ echo '(set-option :produce-models true)(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2 + $ echo '(set-option :produce-models true)(get-model)' | alt-ergo --sat-solver Tableaux -i smtlib2 -o smtlib2 (error "No model produced.") And now some cases where it should work (using either `--produce-models` or `set-option`): - $ echo '(check-sat)(get-model)' | alt-ergo --frontend dolmen --produce-models -i smtlib2 -o smtlib2 2>/dev/null + $ echo '(check-sat)(get-model)' | alt-ergo --produce-models -i smtlib2 -o smtlib2 2>/dev/null unknown ( ) - $ echo '(set-option :produce-models true)(check-sat)(get-model)' | alt-ergo --frontend dolmen -i smtlib2 -o smtlib2 2>/dev/null + $ echo '(set-option :produce-models true)(check-sat)(get-model)' | alt-ergo -i smtlib2 -o smtlib2 2>/dev/null unknown ( ) - $ echo '(set-option :produce-models true)(check-sat)(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2 2>/dev/null + $ echo '(set-option :produce-models true)(check-sat)(get-model)' | alt-ergo --sat-solver Tableaux -i smtlib2 -o smtlib2 2>/dev/null unknown ( From 3f4b2db5b832a267cd2edca4a8b112e053de4195 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Wed, 4 Oct 2023 11:21:00 +0200 Subject: [PATCH 2/2] Document the change --- CHANGES.md | 2 ++ .../Native/02_types/02_01_builtin.md | 10 +++--- .../Input_file_formats/SMT-LIB2/index.md | 9 ++---- docs/sphinx_docs/Usage/index.md | 31 ++++++++++--------- 4 files changed, 26 insertions(+), 26 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 17a25cace..fb1b736ad 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 164af1616..811e78776 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 b15c7c164..630aa8380 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 efdcdacaa..646c41df8 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 ```