diff --git a/src/main.ml b/src/main.ml
index 1e6ac5235796a466756b4eab35a245e14efa927b..37916d130a260900ee239fcdee02fb48a319fac0 100644
--- a/src/main.ml
+++ b/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
diff --git a/src/verification.ml b/src/verification.ml
index 872cb3907d661751f05315140569aed8ca76f9d1..8d547728324f1ade6a9f8b9dfb305195e62bd3d4 100644
--- a/src/verification.ml
+++ b/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
diff --git a/src/verification.mli b/src/verification.mli
index 2910d6734ddd239418b7aacfa11da38c130ba24c..27d6fc6e961be2732441576402f81494532fafb0 100644
--- a/src/verification.mli
+++ b/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. *)