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

@@ -884,25 +884,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 Native
 let infer_input_format = ref true
 let parse_only = ref false

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
   (