[cmdline][verification] Add support for selecting prover alternatives.

src/main.ml

@@ -135,7 +135,8 @@ let log_theory_answer =
           Fmt.(option ~none:nop (any " " ++ string))
           additional_info)))
 
-let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover files =
+let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern
+  files =
   let debug = log_level_is_debug () in
   let memlimit = Option.map memlimit ~f:memlimit_of_string in
   let timelimit = Option.map timelimit ~f:timelimit_of_string in
@@ -143,7 +144,7 @@ let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover files =
     List.map files
       ~f:
         (Verification.verify ~debug ?format ~loadpath ?memlimit ?timelimit
-           ?dataset prover)
+           ?dataset prover ?prover_altern)
   in
   List.iter theory_answers ~f:log_theory_answer;
   theory_answers
@@ -285,39 +286,55 @@ let verify_cmd =
     let doc = "File format." in
     Arg.(value & opt (some string) None & info [ "format" ] ~doc)
   in
-  let term =
-    let files =
-      let doc = "File to verify." in
-      let file_or_stdin = Arg.conv' Verification.File.(of_string, pretty) in
-      Arg.(non_empty & pos_all file_or_stdin [] & info [] ~doc ~docv:"FILE")
-    in
-    let prover =
-      let all_provers = Prover.list_available () in
-      let doc =
-        Fmt.str
-          "Prover to use. Support is provided for the following $(docv)s: %a."
-          (Fmt.list ~sep:Fmt.comma Fmt.string)
-          (List.map ~f:Prover.to_string all_provers)
-      in
-      let provers =
-        Arg.enum (List.map ~f:(fun p -> (Prover.to_string p, p)) all_provers)
-      in
-      Arg.(
-        required
-        & opt (some provers) None
-        & info [ "p"; "prover" ] ~doc ~docv:"PROVER")
+  let prover =
+    let all_provers = Prover.list_available () in
+    let doc =
+      Fmt.str
+        "Prover to use. Support is provided for the following $(docv)s: %a."
+        (Fmt.list ~sep:Fmt.comma Fmt.string)
+        (List.map ~f:Prover.to_string all_provers)
     in
-    let dataset =
-      let doc = "Dataset $(docv) (CSV format only)." in
-      Arg.(value & opt (some file) None & info [ "dataset" ] ~doc ~docv:"FILE")
+    let provers =
+      Arg.enum (List.map ~f:(fun p -> (Prover.to_string p, p)) all_provers)
     in
+    Arg.(
+      required
+      & opt (some provers) None
+      & info [ "p"; "prover" ] ~doc ~docv:"PROVER")
+  in
+  let prover_altern =
+    let doc = "Alternative prover configuration." in
+    Arg.(value & opt (some string) None & info [ "prover-altern" ] ~doc)
+  in
+  let dataset =
+    let doc = "Dataset $(docv) (CSV format only)." in
+    Arg.(value & opt (some file) None & info [ "dataset" ] ~doc ~docv:"FILE")
+  in
+  let files =
+    let doc = "File to verify." in
+    let file_or_stdin = Arg.conv' Verification.File.(of_string, pretty) in
+    Arg.(non_empty & pos_all file_or_stdin [] & info [] ~doc ~docv:"FILE")
+  in
+  let term =
     Term.(
-      const (fun format loadpath memlimit timelimit prover dataset files _ ->
+      const
+        (fun
+          format
+          loadpath
+          memlimit
+          timelimit
+          prover
+          prover_altern
+          dataset
+          files
+          _
+        ->
         exec_cmd cmdname (fun () ->
           ignore
-            (verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover files)))
-      $ format $ loadpath $ memlimit $ timelimit $ prover $ dataset $ files
-      $ setup_logs)
+            (verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover
+               ?prover_altern files)))
+      $ format $ loadpath $ memlimit $ timelimit $ prover $ prover_altern
+      $ dataset $ files $ setup_logs)
   in
   Cmd.v info term
 

src/verification.ml

@@ -378,7 +378,7 @@ let call_prover ?dataset ~limit config env prover config_prover driver task =
   { id; result; additional_info }
 
 let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
-  prover file =
+  prover ?prover_altern file =
   if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
   let env, config = create_env ~debug loadpath in
   let main = Whyconf.get_main config in
@@ -406,12 +406,31 @@ let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
       let tasks = Task.split_theory theory None None in
       let config_prover =
         let altern =
-          if Prover.has_vnnlib_support prover && Option.is_some dataset
-          then "VNNLIB"
-          else ""
+          let default =
+            if Prover.has_vnnlib_support prover && Option.is_some dataset
+            then "VNNLIB"
+            else "" (* Select the default one, w/o an alternative. *)
+          in
+          Option.value prover_altern ~default
         in
         let prover = Prover.to_string prover in
-        Whyconf.(filter_one_prover config (mk_filter_prover ~altern prover))
+        try
+          Whyconf.(filter_one_prover config (mk_filter_prover ~altern prover))
+        with
+        | Whyconf.ProverNotFound _ ->
+          invalid_arg
+            (Fmt.str "No prover corresponds to %s%a" prover
+               (if String.equal altern ""
+               then Fmt.nop
+               else Fmt.(any " " ++ parens string))
+               altern)
+        | Whyconf.ProverAmbiguity _ ->
+          invalid_arg
+            (Fmt.str "More than one prover correspond to %s%a" prover
+               (if String.equal altern ""
+               then Fmt.nop
+               else Fmt.(any " " ++ parens string))
+               altern)
       in
       let driver =
         match

src/verification.mli

@@ -90,20 +90,23 @@ val verify :
   ?timelimit:int ->
   ?dataset:string ->
   Prover.t ->
+  ?prover_altern:string ->
   File.t ->
   theory_answer
-(** [verify debug format loadpath memlimit timeout dataset prover file] launches
-    a verification of the given [file] with the provided [prover] and [dataset].
+(** [verify debug format loadpath memlimit timelimit dataset prover prover_altern file]
+    launches a verification of the given [file] with the provided [prover] and
+    [dataset].
 
     @param debug when set, enables debug information.
     @param format is the [file] format.
     @param loadpath is the additional loadpath.
     @param memlimit
       is the memory limit (in megabytes) granted to the verification.
-    @param timeout is the timeout (in seconds) granted to the verification.
+    @param timelimit is the timeout (in seconds) granted to the verification.
     @param dataset
       is the filepath of a dataset (eg, in CSV format) possibly appearing in
       [file].
+    @param prover_altern is the alternative [prover] configuration.
     @return
       for each theory, an [answer] for each goal of the theory, respecting the
       order of appearance. *)