6 |
6 |
7 signature SLEDGEHAMMER_ISAR = |
7 signature SLEDGEHAMMER_ISAR = |
8 sig |
8 sig |
9 type params = ATP_Manager.params |
9 type params = ATP_Manager.params |
10 |
10 |
|
11 val atps: string Unsynchronized.ref |
|
12 val timeout: int Unsynchronized.ref |
|
13 val full_types: bool Unsynchronized.ref |
11 val default_params : theory -> (string * string) list -> params |
14 val default_params : theory -> (string * string) list -> params |
12 end; |
15 end; |
13 |
16 |
14 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = |
17 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = |
15 struct |
18 struct |
32 (r2 : relevance_override) = |
35 (r2 : relevance_override) = |
33 {add = #add r1 @ #add r2, del = #del r1 @ #del r2, |
36 {add = #add r1 @ #add r2, del = #del r1 @ #del r2, |
34 only = #only r1 andalso #only r2} |
37 only = #only r1 andalso #only r2} |
35 fun merge_relevance_overrides rs = |
38 fun merge_relevance_overrides rs = |
36 fold merge_relevance_override_pairwise rs (only_relevance_override []) |
39 fold merge_relevance_override_pairwise rs (only_relevance_override []) |
|
40 |
|
41 (*** parameters ***) |
|
42 |
|
43 val atps = Unsynchronized.ref (default_atps_param_value ()) |
|
44 val timeout = Unsynchronized.ref 60 |
|
45 val full_types = Unsynchronized.ref false |
|
46 |
|
47 val _ = |
|
48 ProofGeneralPgip.add_preference Preferences.category_proof |
|
49 (Preferences.string_pref atps |
|
50 "Sledgehammer: ATPs" |
|
51 "Default automatic provers (separated by whitespace)") |
|
52 |
|
53 val _ = |
|
54 ProofGeneralPgip.add_preference Preferences.category_proof |
|
55 (Preferences.int_pref timeout |
|
56 "Sledgehammer: Time limit" |
|
57 "ATPs will be interrupted after this time (in seconds)") |
|
58 |
|
59 val _ = |
|
60 ProofGeneralPgip.add_preference Preferences.category_proof |
|
61 (Preferences.bool_pref full_types |
|
62 "Sledgehammer: Full types" "ATPs will use full type information") |
37 |
63 |
38 type raw_param = string * string list |
64 type raw_param = string * string list |
39 |
65 |
40 val default_default_params = |
66 val default_default_params = |
41 [("debug", "false"), |
67 [("debug", "false"), |