From 2bba1aa48b45bd0415229d99cc4040f3b1494095 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] 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 d09cc1d02f..71a937fdd6 100644 --- a/src/bin/common/parse_command.ml +++ b/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 \ diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index 8895a8809e..f238ae6413 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 Native let infer_input_format = ref true let parse_only = ref false diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t index 187dc2748c..ff932c9595 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 (