Source file Why3Provers.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
let cfg = lazy
begin
let = Wp_parameters.Why3ExtraConfig.get () in
try Why3.Whyconf.init_config ~extra_config None
with exn ->
Wp_parameters.abort "%a" Why3.Exn_printer.exn_printer exn
end
let why3_version = Why3.Config.version
let config () = Lazy.force cfg
let set_procs = Why3.Controller_itp.set_session_max_tasks
let configure =
let todo = ref true in
begin fun () ->
if !todo then
begin
let commands = "why3"::Wp_parameters.Why3Flags.get () in
let args = Array.of_list commands in
begin try
Why3.Getopt.commands := commands;
Why3.Getopt.parse_all
(Why3.Debug.Args.[desc_debug;desc_debug_all;desc_debug_list])
(fun opt -> raise (Arg.Bad ("unknown option: " ^ opt)))
args
with Arg.Bad s | Arg.Help s -> Wp_parameters.abort "%s" s
end;
ignore (Why3.Debug.Args.option_list ());
Why3.Debug.Args.set_flags_selected ();
todo := false
end
end
type t = Why3.Whyconf.prover
let ident_why3 = Why3.Whyconf.prover_parseable_format
let ident_wp s =
let name = Why3.Whyconf.prover_parseable_format s in
let prv = String.split_on_char ',' name in
String.concat ":" prv
let title ?(version=true) p =
if version then Pretty_utils.to_string Why3.Whyconf.print_prover p
else p.Why3.Whyconf.prover_name
let compare = Why3.Whyconf.Prover.compare
let name p = p.Why3.Whyconf.prover_name
let version p = p.Why3.Whyconf.prover_version
let altern p = p.Why3.Whyconf.prover_altern
let is_mainstream p = p.Why3.Whyconf.prover_version <> "" && p.Why3.Whyconf.prover_altern = ""
let is_auto (p : t) =
match p.prover_name with
| "Coq" | "Isabelle" -> false
| "Alt-Ergo" | "Z3" | "CVC4" | "CVC5" | "Colibri2" -> true
| _ ->
let config = config () in
try
let prover_config = Why3.Whyconf.get_prover_config config p in
not prover_config.interactive
with Not_found -> true
let has_counter_examples p =
List.mem "counterexamples" @@
String.split_on_char '+' p.Why3.Whyconf.prover_altern
let provers () =
Why3.Whyconf.Mprover.keys (Why3.Whyconf.get_provers (config ()))
let provers_set () : Why3.Whyconf.Sprover.t =
Why3.Whyconf.Mprover.domain (Why3.Whyconf.get_provers (config ()))
let is_available p =
Why3.Whyconf.Mprover.mem p (Why3.Whyconf.get_provers (config ()))
let with_counter_examples p =
if has_counter_examples p then Some p else
let name = p.prover_name in
let version = p.prover_version in
List.find_opt
(fun (q : t) ->
q.prover_name = name &&
q.prover_version = version &&
has_counter_examples q)
@@ provers ()
type sem = V of int | S of string
let sem s = try V (int_of_string s) with Failure _ -> S s
let cmp x y =
match x,y with
| V a,V b -> b - a
| V _,S _ -> (-1)
| S _,V _ -> (+1)
| S a,S b -> String.compare a b
let scmp u v = cmp (sem u) (sem v)
let vcmp u v =
List.compare scmp (String.split_on_char '.' u) (String.split_on_char '.' v)
let by_version (p:t) (q:t) = vcmp p.prover_version q.prover_version
let filter ~name ?version (p:t) =
p.prover_altern = "" &&
String.lowercase_ascii p.prover_name = name &&
match version with None -> true | Some v -> p.prover_version = v
let select ~name ?version () =
match
List.sort by_version @@ List.filter (filter ~name ?version) @@ provers ()
with p::_ -> Some p | [] -> None
let lookup ?(fallback=false) prover_name =
match String.split_on_char ':' @@ String.lowercase_ascii prover_name with
| [name] -> select ~name ()
| [name;version] ->
begin
match select ~name ~version () with
| Some _ as res -> res
| None ->
if fallback then
match select ~name () with
| None -> None
| Some p as res ->
Wp_parameters.warning ~once:true ~current:false
"Prover %s not found, fallback to %s" prover_name (ident_wp p) ;
res
else None
end
| _ -> None
type model = Why3.Model_parser.concrete_syntax_term
let pp_model = Why3.Model_parser.print_concrete_term