From 6342c4822b2bc435995bfcec6b82e3762d84c331 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 6 Oct 2020 15:05:24 +0200
Subject: [PATCH] [wp/gui] filter mainstream provers
---
src/plugins/wp/GuiConfig.ml | 27 ++++++++++++++++++++-------
src/plugins/wp/Why3Provers.ml | 1 +
src/plugins/wp/Why3Provers.mli | 1 +
3 files changed, 22 insertions(+), 7 deletions(-)
diff --git a/src/plugins/wp/GuiConfig.ml b/src/plugins/wp/GuiConfig.ml
index 3a286db188b..4e28f2e8957 100644
--- a/src/plugins/wp/GuiConfig.ml
+++ b/src/plugins/wp/GuiConfig.ml
@@ -34,13 +34,17 @@ class provers =
initializer
begin
(** select automatically the provers set on the command line *)
- let cmdline = Wp_parameters.Provers.get () in
+ let cmdline =
+ match Wp_parameters.Provers.get () with
+ | [] -> [ "alt-ergo" ]
+ | prvs -> prvs
+ in
let selection = List.fold_left
(fun acc e ->
match Why3Provers.find_opt e with
| None -> acc
| Some p -> S.add p acc)
- S.empty cmdline
+ S.empty cmdline
in
self#set selection ;
end
@@ -62,13 +66,14 @@ class dp_chooser
let array = new Wpane.warray () in
object(self)
+ val mutable mainstream = true
val mutable selected = M.empty
method private enable dp e =
selected <- M.add dp e selected
method private lookup dp =
- M.find dp selected
+ try M.find dp selected with Not_found -> false
method private entry dp =
let text = Why3Provers.title dp in
@@ -91,9 +96,15 @@ class dp_chooser
array#update () ;
end
- method private detect () =
+ method private provers =
+ let filter p =
+ self#lookup p || not mainstream || Why3Provers.is_mainstream p
+ in S.filter filter (Why3Provers.provers_set ())
+
+ method private filter () =
begin
- self#configure (Why3Provers.provers_set ());
+ mainstream <- not mainstream ;
+ self#configure self#provers ;
end
method private apply () =
@@ -105,7 +116,8 @@ class dp_chooser
selected)
method run () =
- let dps = Why3Provers.provers_set () in
+ selected <- M.empty ;
+ let dps = self#provers in
let sel = provers#get in
selected <- M.merge
(fun _ avail enab ->
@@ -119,7 +131,8 @@ class dp_chooser
initializer
begin
- dialog#button ~action:(`ACTION self#detect) ~label:"Detect Provers" () ;
+ dialog#button ~action:(`ACTION self#filter) ~label:"Filter"
+ ~tooltip:"Switch to main stream / alternative solvers" () ;
dialog#button ~action:(`CANCEL) ~label:"Cancel" () ;
dialog#button ~action:(`APPLY) ~label:"Apply" () ;
array#set_entry self#entry ;
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 46a1f714ab5..215d8912e50 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -94,6 +94,7 @@ let print_wp s =
let title p = Pretty_utils.sfprintf "%a" Why3.Whyconf.print_prover p
let name p = p.Why3.Whyconf.prover_name
let compare = Why3.Whyconf.Prover.compare
+let is_mainstream p = p.Why3.Whyconf.prover_altern = ""
let provers () =
Why3.Whyconf.Mprover.keys (Why3.Whyconf.get_provers (config ()))
diff --git a/src/plugins/wp/Why3Provers.mli b/src/plugins/wp/Why3Provers.mli
index 4875dbcc97b..1098dc55906 100644
--- a/src/plugins/wp/Why3Provers.mli
+++ b/src/plugins/wp/Why3Provers.mli
@@ -41,6 +41,7 @@ val compare : t -> t -> int
val provers : unit -> t list
val provers_set : unit -> Why3.Whyconf.Sprover.t
val is_available : t -> bool
+val is_mainstream : t -> bool
val has_shortcut : t -> string -> bool
(**************************************************************************)
--
GitLab