From 26194459b2ba0811cc3b687ea55084961de68f00 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 21 Sep 2023 14:56:09 +0200 Subject: [PATCH] Remove SAT solver choice while model generating As SatML supports model generation, we don't need to select the appropriate SAT solver while parsing the command line or the SMT-LIB statement `(set-option :produce-models true)`. --- docs/sphinx_docs/Usage/index.md | 12 +++--- src/bin/common/parse_command.ml | 74 ++++++++++++--------------------- src/bin/common/solving_loop.ml | 10 +---- 3 files changed, 33 insertions(+), 63 deletions(-) diff --git a/docs/sphinx_docs/Usage/index.md b/docs/sphinx_docs/Usage/index.md index de82ac0517..c102f6a10d 100644 --- a/docs/sphinx_docs/Usage/index.md +++ b/docs/sphinx_docs/Usage/index.md @@ -51,8 +51,8 @@ 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 options - `--sat-solver tableaux` and `--frontend dolmen`. + `(set-option :produce-models true)`. This currently requires using the option + `--frontend dolmen`. #### Examples @@ -142,7 +142,7 @@ Model generation is disabled by default. There are two recommended ways to enabl (get-model) ``` - and the command `alt-ergo --frontend dolmen --sat-solver tableaux INPUT.smt2` produces + and the command `alt-ergo --frontend dolmen INPUT.smt2` produces the output model ``` unknown @@ -154,10 +154,8 @@ Model generation is disabled by default. There are two recommended ways to enabl ``` ```{admonition} Note - You need to select the Dolmen frontend and the SAT solver Tableaux as the - model generation is not supported yet by the other SAT solvers. The options - `--dump-models` and `--produce-models` select the right frontend and SAT solver - for you. + You need to select the Dolmen frontend. The options `--dump-models` and + `--produce-models` select the right frontend for you. ``` ### Output diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index 04a2c61b44..296f070b50 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -923,58 +923,38 @@ let parse_output_opt = frontend in - (* Use the --sat-solver to determine the sat solver. - - If an interpretation is provided, the solver is forced to be Tableaux, - because generation of models requires OptimAE for the other solvers. - - See https://github.com/OCamlPro/alt-ergo/pull/553 *) + (* Use the --sat-solver to determine the sat solver. *) let sat_solver = - let sat_solver_arg = - let sat_solver : _ Arg.conv = - let parse = function - | "CDCL" | "satML" -> - Ok Util.CDCL - | "CDCL-Tableaux" | "satML-Tableaux" - | "CDCL-tableaux" | "satML-tableaux" -> - Ok Util.CDCL_Tableaux - | "tableaux" | "Tableaux" - | "tableaux-like" | "Tableaux-like" -> - Ok Util.Tableaux - | "tableaux-cdcl" | "Tableaux-CDCL" - | "tableaux-CDCL" | "Tableaux-cdcl" -> - Ok Util.Tableaux_CDCL - | sat_solver -> - Error ("Args parsing error: unkown SAT solver " ^ sat_solver) + let sat_solver : _ Arg.conv = + let parse = function + | "CDCL" | "satML" -> + Ok Util.CDCL + | "CDCL-Tableaux" | "satML-Tableaux" + | "CDCL-tableaux" | "satML-tableaux" -> + Ok Util.CDCL_Tableaux + | "tableaux" | "Tableaux" + | "tableaux-like" | "Tableaux-like" -> + Ok Util.Tableaux + | "tableaux-cdcl" | "Tableaux-CDCL" + | "tableaux-CDCL" | "Tableaux-cdcl" -> + Ok Util.Tableaux_CDCL + | sat_solver -> + Error ("Args parsing error: unkown SAT solver " ^ sat_solver) - in - Arg.(conv' (parse, Util.pp_sat_solver)) in - let default, sum_up = "CDCL-Tableaux", "satML" in - let doc = Format.sprintf - "Choose the SAT solver to use. Default value is %s (i.e. %s\ - solver). Possible options are %s." - default sum_up - (Arg.doc_alts ["CDCL"; "satML"; "CDCL-Tableaux"; - "satML-Tableaux"; "Tableaux-CDCL"]) - in - let docv = "SAT" in - Arg.(value & opt (some ~none:default sat_solver) None & - info ["sat-solver"] ~docv ~docs:s_sat ~doc) + Arg.(conv' (parse, Util.pp_sat_solver)) in - - let mk_sat_solver sat_solver interpretation = - match interpretation, sat_solver with - | INone, None -> Ok Util.CDCL_Tableaux - | INone, Some sat_solver -> Ok sat_solver - | _, (None | Some Util.Tableaux) -> Ok Tableaux - | _, Some sat_solver -> - Fmt.error - "solver '%a' does not suppot model generation" - Util.pp_sat_solver sat_solver + let default, sum_up = "CDCL-Tableaux", "satML" in + let doc = Format.sprintf + "Choose the SAT solver to use. Default value is %s (i.e. %s\ + solver). Possible options are %s." + default sum_up + (Arg.doc_alts ["CDCL"; "satML"; "CDCL-Tableaux"; + "satML-Tableaux"; "Tableaux-CDCL"]) in - Term.term_result' @@ - Term.(const mk_sat_solver $ sat_solver_arg $ interpretation) + let docv = "SAT" in + Arg.(value & opt sat_solver Util.CDCL_Tableaux & + info ["sat-solver"] ~docv ~docs:s_sat ~doc) in let cdcl_tableaux_inst = diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 44d2ace472..22afb5053a 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -358,15 +358,7 @@ let main () = Options.Output.create_channel name |> Options.Output.set_diagnostic | ":produce-models", Symbol { name = Simple "true"; _ } -> - (* TODO: The generation of models is supported only with the SAT - solver Tableaux. Remove this line after merging the OptimAE - PR. See https://github.com/OCamlPro/alt-ergo/pull/553 *) - if Stdlib.(Options.get_sat_solver () = Tableaux) then - Options.set_interpretation ILast - else - Printer.print_smtlib_err - "Model generation requires the Tableaux solver \ - (try --produce-models)"; + Options.set_interpretation ILast | ":produce-models", Symbol { name = Simple "false"; _ } -> Options.set_interpretation INone | ":produce-unsat-cores", Symbol { name = Simple "true"; _ } ->