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)`.
OCamlPro · Sep 21, 2023 · 2619445 · 2619445
1 parent f764ed4
commit 2619445
Show file tree

Hide file tree

Showing 3 changed files with 33 additions and 63 deletions.
diff --git 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
@@ -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
@@ -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"; _ } ->