From 269b807dd9212f7304cea44f1fa3d321ce51d1fb Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 2 Feb 2024 14:40:28 +0100
Subject: [PATCH] [wp] fix prover selection - use Alt-Ergo instead of alt-ergo
- resolve ambiguity when several solvers match the provided name
---
src/plugins/wp/Why3Provers.ml | 40 ++++++++++---------
src/plugins/wp/gui/GuiConfig.ml | 2 +-
src/plugins/wp/register.ml | 2 +-
.../wp/tests/wp/stmtcompiler_test_rela.ml | 2 +-
4 files changed, 25 insertions(+), 21 deletions(-)
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 38a9e971297..d0c6c907463 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -62,16 +62,24 @@ let configure =
type t = Why3.Whyconf.prover
+(* In an ambiguous map of provers, tries to find the basic alternative, if none
+ is found, just give an arbitrary one. *)
+let resolve_ambiguity provers =
+ let open Why3.Whyconf in
+ let provers = fst @@ List.split @@ Mprover.bindings provers in
+ try List.find (fun p -> p.prover_altern = "") provers
+ with Not_found -> List.hd provers
+
let find_opt s =
+ let open Why3.Whyconf in
try
let config = Lazy.force cfg in
- let filter = Why3.Whyconf.parse_filter_prover s in
- Some ((Why3.Whyconf.filter_one_prover config filter).Why3.Whyconf.prover)
+ let filter = parse_filter_prover s in
+ Some ((filter_one_prover config filter).prover)
with
- | Why3.Whyconf.ProverNotFound _
- | Why3.Whyconf.ParseFilterProver _
- | Why3.Whyconf.ProverAmbiguity _ ->
- None
+ | ParseFilterProver _ -> None
+ | ProverNotFound _ -> None
+ | ProverAmbiguity (_, _, provers) -> Some (resolve_ambiguity provers)
type fallback = Exact of t | Fallback of t | NotFound
@@ -79,18 +87,14 @@ let find_fallback name =
match find_opt name with
| Some prv -> Exact prv
| None ->
- (* Why3 should deal with this intermediate case *)
- match find_opt (String.lowercase_ascii name) with
- | Some prv -> Exact prv
- | None ->
- match String.split_on_char ',' name with
- | shortname :: _ :: _ ->
- begin
- match find_opt (String.lowercase_ascii shortname) with
- | Some prv -> Fallback prv
- | None -> NotFound
- end
- | _ -> NotFound
+ match String.split_on_char ',' name with
+ | shortname :: _ :: _ ->
+ begin
+ match find_opt (String.lowercase_ascii shortname) with
+ | Some prv -> Fallback prv
+ | None -> NotFound
+ end
+ | _ -> NotFound
let ident_why3 = Why3.Whyconf.prover_parseable_format
let ident_wp s =
diff --git a/src/plugins/wp/gui/GuiConfig.ml b/src/plugins/wp/gui/GuiConfig.ml
index a6ba232e23f..f40609610d9 100644
--- a/src/plugins/wp/gui/GuiConfig.ml
+++ b/src/plugins/wp/gui/GuiConfig.ml
@@ -36,7 +36,7 @@ class provers =
(* select automatically the provers set on the command line *)
let cmdline =
match Wp_parameters.Provers.get () with
- | [] -> [ "alt-ergo" ]
+ | [] -> [ "Alt-Ergo" ]
| prvs -> prvs
in
let selection = List.fold_left
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 21f04e38923..ab5b89f86ec 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -549,7 +549,7 @@ let spawn_wp_proofs ~script goals =
let get_prover_names () =
match Wp_parameters.Provers.get () with
- | [] -> [ "alt-ergo" ] | pnames -> pnames
+ | [] -> [ "Alt-Ergo" ] | pnames -> pnames
let compute_provers ~mode ~script =
script.provers <- List.fold_right
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
index 3e167f78bf9..77eab89a96c 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
@@ -22,7 +22,7 @@ let run () =
| None -> prvs
| Some VCS.Tactical -> prvs
| Some prv -> (VCS.Batch, prv) :: prvs)
- ["alt-ergo"] []
+ ["Alt-Ergo"] []
in
let spawn goal =
--
GitLab