Make Dolmen the default frontend

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

docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md

@@ -141,8 +141,8 @@
 
 `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 @@
 
 `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
 
@@ -254,7 +254,7 @@
 
 goal g1: 
    (* Valid *)
    g(f(0.01)) = f(0.01)
 
 goal g2: 
    (* Valid *)
@@ -263,7 +263,7 @@
 goal g3: 
    (* I don't know *)
    g(f(0.01)) = g(0)
 ```
 
 ## Polymorphic functional arrays
 
@@ -281,7 +281,7 @@
 <farray_access_expr> ::= <array_id> '[' <index> ']'
 
 (* Update - this expression is of type ((index_type) (value_type) farray) *)
 <farray_update_expr> ::= <array_id> '[' <index> '<-' <new_value> ( ',' <index> '<-' <new_value> )* ']'
 ```
 
 ### Examples
@@ -300,7 +300,7 @@
 
 ```
 (* Accessing and updating farrays *)
 goal g1:
     forall i,j,k:int.
     forall v,w:'a.
     forall b:'a farray.

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

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
   ```

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 \

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 []

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
   (