author | blanchet |
Mon, 23 Jan 2012 17:40:32 +0100 | |
changeset 46320 | 0b8b73b49848 |
parent 46301 | e2e52c7d25c9 |
child 46340 | cac402c486b0 |
permissions | -rw-r--r-- |
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_run.ML |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
2 |
Author: Fabian Immler, TU Muenchen |
32996
d2e48879e65a
removed disjunctive group cancellation -- provers run independently;
wenzelm
parents:
32995
diff
changeset
|
3 |
Author: Makarius |
35969 | 4 |
Author: Jasmin Blanchette, TU Muenchen |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
5 |
|
38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38020
diff
changeset
|
6 |
Sledgehammer's heart. |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
7 |
*) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
8 |
|
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
9 |
signature SLEDGEHAMMER_RUN = |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
10 |
sig |
46320 | 11 |
type minimize_command = ATP_Proof_Reconstruct.minimize_command |
38988 | 12 |
type relevance_override = Sledgehammer_Filter.relevance_override |
43021 | 13 |
type mode = Sledgehammer_Provers.mode |
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
14 |
type params = Sledgehammer_Provers.params |
41263
4cac389c005f
renamed function to run prover with minimizer and changed signature to clarify its semantics and make it a drop in replacement for "get_prover"
blanchet
parents:
41262
diff
changeset
|
15 |
type prover = Sledgehammer_Provers.prover |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
16 |
|
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
17 |
val someN : string |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
18 |
val noneN : string |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
19 |
val timeoutN : string |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
20 |
val unknownN : string |
44892 | 21 |
val auto_minimize_min_facts : int Config.T |
22 |
val auto_minimize_max_time : real Config.T |
|
43021 | 23 |
val get_minimizing_prover : Proof.context -> mode -> string -> prover |
38044 | 24 |
val run_sledgehammer : |
45520 | 25 |
params -> mode -> int -> relevance_override |
26 |
-> ((string * string list) list -> string -> minimize_command) |
|
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
27 |
-> Proof.state -> bool * (string * Proof.state) |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
28 |
end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
29 |
|
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
30 |
structure Sledgehammer_Run : SLEDGEHAMMER_RUN = |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
31 |
struct |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
32 |
|
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset
|
33 |
open ATP_Util |
46320 | 34 |
open ATP_Problem_Generate |
35 |
open ATP_Proof_Reconstruct |
|
38023 | 36 |
open Sledgehammer_Util |
38988 | 37 |
open Sledgehammer_Filter |
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41066
diff
changeset
|
38 |
open Sledgehammer_Provers |
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
39 |
open Sledgehammer_Minimize |
40072
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
40 |
|
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
41 |
val someN = "some" |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
42 |
val noneN = "none" |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
43 |
val timeoutN = "timeout" |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
44 |
val unknownN = "unknown" |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
45 |
|
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
46 |
val ordered_outcome_codes = [someN, unknownN, timeoutN, noneN] |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
47 |
|
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
48 |
fun max_outcome_code codes = |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
49 |
NONE |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
50 |
|> fold (fn candidate => |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
51 |
fn accum as SOME _ => accum |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
52 |
| NONE => if member (op =) codes candidate then SOME candidate |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
53 |
else NONE) |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
54 |
ordered_outcome_codes |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
55 |
|> the_default unknownN |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
56 |
|
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41180
diff
changeset
|
57 |
fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i |
41089 | 58 |
n goal = |
43005
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset
|
59 |
(name, |
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset
|
60 |
(if verbose then |
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset
|
61 |
" with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts |
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset
|
62 |
else |
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset
|
63 |
"") ^ |
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset
|
64 |
" on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ |
45379
0147a4348ca1
try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents:
45370
diff
changeset
|
65 |
(if blocking then "." |
0147a4348ca1
try "smt" as a fallback for ATPs if "metis" fails/times out
blanchet
parents:
45370
diff
changeset
|
66 |
else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) |
41089 | 67 |
|
44892 | 68 |
val auto_minimize_min_facts = |
69 |
Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts} |
|
42968
74415622d293
more work on parsing LEO-II proofs and extracting uses of extensionality
blanchet
parents:
42966
diff
changeset
|
70 |
(fn generic => Config.get_generic generic binary_min_facts) |
44892 | 71 |
val auto_minimize_max_time = |
72 |
Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time} |
|
73 |
(K 5.0) |
|
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset
|
74 |
|
45520 | 75 |
fun adjust_reconstructor_params override_params |
46301 | 76 |
({debug, verbose, overlord, blocking, provers, type_enc, strict, |
45520 | 77 |
lam_trans, relevance_thresholds, max_relevant, max_mono_iters, |
45707
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset
|
78 |
max_new_mono_instances, isar_proof, isar_shrink_factor, slice, |
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset
|
79 |
minimize, timeout, preplay_timeout, expect} : params) = |
45520 | 80 |
let |
81 |
fun lookup_override name default_value = |
|
82 |
case AList.lookup (op =) override_params name of |
|
83 |
SOME [s] => SOME s |
|
84 |
| _ => default_value |
|
85 |
(* Only those options that reconstructors are interested in are considered |
|
86 |
here. *) |
|
87 |
val type_enc = lookup_override "type_enc" type_enc |
|
88 |
val lam_trans = lookup_override "lam_trans" lam_trans |
|
89 |
in |
|
90 |
{debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, |
|
46301 | 91 |
provers = provers, type_enc = type_enc, strict = strict, |
45520 | 92 |
lam_trans = lam_trans, max_relevant = max_relevant, |
93 |
relevance_thresholds = relevance_thresholds, |
|
94 |
max_mono_iters = max_mono_iters, |
|
95 |
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, |
|
45707
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset
|
96 |
isar_shrink_factor = isar_shrink_factor, slice = slice, |
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset
|
97 |
minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, |
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset
|
98 |
expect = expect} |
45520 | 99 |
end |
100 |
||
45707
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset
|
101 |
fun minimize ctxt mode name |
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset
|
102 |
(params as {debug, verbose, isar_proof, minimize, ...}) |
43164 | 103 |
({state, subgoal, subgoal_count, facts, ...} : prover_problem) |
45370
bab52dafa63a
use "Time.time" rather than milliseconds internally
blanchet
parents:
45369
diff
changeset
|
104 |
(result as {outcome, used_facts, run_time, preplay, message, |
bab52dafa63a
use "Time.time" rather than milliseconds internally
blanchet
parents:
45369
diff
changeset
|
105 |
message_tail} : prover_result) = |
43292
ff3d49e77359
don't launch the automatic minimizer for zero facts
blanchet
parents:
43290
diff
changeset
|
106 |
if is_some outcome orelse null used_facts then |
43164 | 107 |
result |
108 |
else |
|
109 |
let |
|
110 |
val num_facts = length used_facts |
|
45707
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset
|
111 |
val ((perhaps_minimize, (minimize_name, params)), preplay) = |
43164 | 112 |
if mode = Normal then |
44892 | 113 |
if num_facts >= Config.get ctxt auto_minimize_min_facts then |
45520 | 114 |
((true, (name, params)), preplay) |
43164 | 115 |
else |
43165
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset
|
116 |
let |
45370
bab52dafa63a
use "Time.time" rather than milliseconds internally
blanchet
parents:
45369
diff
changeset
|
117 |
fun can_min_fast_enough time = |
bab52dafa63a
use "Time.time" rather than milliseconds internally
blanchet
parents:
45369
diff
changeset
|
118 |
0.001 |
bab52dafa63a
use "Time.time" rather than milliseconds internally
blanchet
parents:
45369
diff
changeset
|
119 |
* Real.fromInt ((num_facts + 1) * Time.toMilliseconds time) |
44892 | 120 |
<= Config.get ctxt auto_minimize_max_time |
45707
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset
|
121 |
fun prover_fast_enough () = can_min_fast_enough run_time |
43165
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset
|
122 |
in |
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset
|
123 |
if isar_proof then |
45707
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset
|
124 |
((prover_fast_enough (), (name, params)), preplay) |
43165
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset
|
125 |
else |
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset
|
126 |
let val preplay = preplay () in |
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset
|
127 |
(case preplay of |
45520 | 128 |
Played (reconstr, timeout) => |
45370
bab52dafa63a
use "Time.time" rather than milliseconds internally
blanchet
parents:
45369
diff
changeset
|
129 |
if can_min_fast_enough timeout then |
45561
57227eedce81
don't propagate user-set "type_enc" or "lam_trans" to Metis calls
blanchet
parents:
45520
diff
changeset
|
130 |
(true, extract_reconstructor params reconstr |
45520 | 131 |
||> (fn override_params => |
132 |
adjust_reconstructor_params |
|
133 |
override_params params)) |
|
43165
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset
|
134 |
else |
45707
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset
|
135 |
(prover_fast_enough (), (name, params)) |
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset
|
136 |
| _ => (prover_fast_enough (), (name, params)), |
43165
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset
|
137 |
K preplay) |
8cf188ff76a3
refined auto minimization code: don't use Metis if Isar proofs are desired, and fall back on prover if Metis is too slow
blanchet
parents:
43164
diff
changeset
|
138 |
end |
43164 | 139 |
end |
140 |
else |
|
45520 | 141 |
((false, (name, params)), preplay) |
45707
6bf7eec9b153
added "minimize" option for more control over automatic minimization
blanchet
parents:
45706
diff
changeset
|
142 |
val minimize = minimize |> the_default perhaps_minimize |
43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43233
diff
changeset
|
143 |
val (used_facts, (preplay, message, _)) = |
43164 | 144 |
if minimize then |
145 |
minimize_facts minimize_name params (not verbose) subgoal |
|
146 |
subgoal_count state |
|
147 |
(filter_used_facts used_facts |
|
148 |
(map (apsnd single o untranslated_fact) facts)) |
|
149 |
|>> Option.map (map fst) |
|
150 |
else |
|
43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43233
diff
changeset
|
151 |
(SOME used_facts, (preplay, message, "")) |
43164 | 152 |
in |
153 |
case used_facts of |
|
154 |
SOME used_facts => |
|
155 |
(if debug andalso not (null used_facts) then |
|
156 |
facts ~~ (0 upto length facts - 1) |
|
157 |
|> map (fn (fact, j) => fact |> untranslated_fact |> apsnd (K j)) |
|
158 |
|> filter_used_facts used_facts |
|
159 |
|> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |
|
160 |
|> commas |
|
161 |
|> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ |
|
162 |
" proof (of " ^ string_of_int (length facts) ^ "): ") "." |
|
163 |
|> Output.urgent_message |
|
41263
4cac389c005f
renamed function to run prover with minimizer and changed signature to clarify its semantics and make it a drop in replacement for "get_prover"
blanchet
parents:
41262
diff
changeset
|
164 |
else |
43164 | 165 |
(); |
45370
bab52dafa63a
use "Time.time" rather than milliseconds internally
blanchet
parents:
45369
diff
changeset
|
166 |
{outcome = NONE, used_facts = used_facts, run_time = run_time, |
bab52dafa63a
use "Time.time" rather than milliseconds internally
blanchet
parents:
45369
diff
changeset
|
167 |
preplay = preplay, message = message, message_tail = message_tail}) |
43164 | 168 |
| NONE => result |
169 |
end |
|
170 |
||
171 |
fun get_minimizing_prover ctxt mode name params minimize_command problem = |
|
172 |
get_prover ctxt mode name params minimize_command problem |
|
173 |
|> minimize ctxt mode name params problem |
|
41262
095ecb0c687f
factored out running a prover with (optionally) an implicit minimizer phrase
blanchet
parents:
41260
diff
changeset
|
174 |
|
44586 | 175 |
fun is_induction_fact (Untranslated_Fact ((_, Induction), _)) = true |
176 |
| is_induction_fact _ = false |
|
177 |
||
45706 | 178 |
fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice, |
43059 | 179 |
timeout, expect, ...}) |
43021 | 180 |
mode minimize_command only |
41741 | 181 |
{state, goal, subgoal, subgoal_count, facts, smt_filter} name = |
41089 | 182 |
let |
183 |
val ctxt = Proof.context_of state |
|
42850
c8709be8a40f
distinguish between a soft timeout (30 s by defalt) and a hard timeout (60 s), to let minimization-based provers (such as CVC3, Yices, and occasionally the other provers) do their job
blanchet
parents:
42646
diff
changeset
|
184 |
val hard_timeout = Time.+ (timeout, timeout) |
41089 | 185 |
val birth_time = Time.now () |
42850
c8709be8a40f
distinguish between a soft timeout (30 s by defalt) and a hard timeout (60 s), to let minimization-based provers (such as CVC3, Yices, and occasionally the other provers) do their job
blanchet
parents:
42646
diff
changeset
|
186 |
val death_time = Time.+ (birth_time, hard_timeout) |
41089 | 187 |
val max_relevant = |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
188 |
max_relevant |
45706 | 189 |
|> the_default (default_max_relevant_for_prover ctxt slice name) |
41089 | 190 |
val num_facts = length facts |> not only ? Integer.min max_relevant |
43006 | 191 |
fun desc () = |
41089 | 192 |
prover_description ctxt params name num_facts subgoal subgoal_count goal |
193 |
val problem = |
|
44585 | 194 |
let |
44586 | 195 |
val filter_induction = filter_out is_induction_fact |
44585 | 196 |
in {state = state, goal = goal, subgoal = subgoal, |
197 |
subgoal_count = subgoal_count, facts = |
|
44586 | 198 |
((Sledgehammer_Provers.is_ho_atp ctxt name |> not) ? filter_induction) |
199 |
facts |
|
44585 | 200 |
|> take num_facts, |
201 |
smt_filter = smt_filter} |
|
202 |
end |
|
41255
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
203 |
fun really_go () = |
41263
4cac389c005f
renamed function to run prover with minimizer and changed signature to clarify its semantics and make it a drop in replacement for "get_prover"
blanchet
parents:
41262
diff
changeset
|
204 |
problem |
43051 | 205 |
|> get_minimizing_prover ctxt mode name params minimize_command |
43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43233
diff
changeset
|
206 |
|> (fn {outcome, preplay, message, message_tail, ...} => |
43005
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset
|
207 |
(if outcome = SOME ATP_Proof.TimedOut then timeoutN |
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset
|
208 |
else if is_some outcome then noneN |
43261
a4aeb26a6362
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
blanchet
parents:
43233
diff
changeset
|
209 |
else someN, fn () => message (preplay ()) ^ message_tail)) |
41089 | 210 |
fun go () = |
211 |
let |
|
212 |
val (outcome_code, message) = |
|
213 |
if debug then |
|
214 |
really_go () |
|
215 |
else |
|
216 |
(really_go () |
|
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset
|
217 |
handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n") |
41089 | 218 |
| exn => |
219 |
if Exn.is_interrupt exn then |
|
220 |
reraise exn |
|
221 |
else |
|
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset
|
222 |
(unknownN, fn () => "Internal error:\n" ^ |
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset
|
223 |
ML_Compiler.exn_message exn ^ "\n")) |
41089 | 224 |
val _ = |
41142
43e2b051339c
weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents:
41138
diff
changeset
|
225 |
(* The "expect" argument is deliberately ignored if the prover is |
43e2b051339c
weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents:
41138
diff
changeset
|
226 |
missing so that the "Metis_Examples" can be processed on any |
43e2b051339c
weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents:
41138
diff
changeset
|
227 |
machine. *) |
43e2b051339c
weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents:
41138
diff
changeset
|
228 |
if expect = "" orelse outcome_code = expect orelse |
43e2b051339c
weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents:
41138
diff
changeset
|
229 |
not (is_prover_installed ctxt name) then |
41089 | 230 |
() |
231 |
else if blocking then |
|
232 |
error ("Unexpected outcome: " ^ quote outcome_code ^ ".") |
|
233 |
else |
|
234 |
warning ("Unexpected outcome: " ^ quote outcome_code ^ "."); |
|
43005
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset
|
235 |
in (outcome_code, message) end |
41089 | 236 |
in |
43021 | 237 |
if mode = Auto_Try then |
43006 | 238 |
let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in |
239 |
(outcome_code, |
|
240 |
state |
|
241 |
|> outcome_code = someN |
|
242 |
? Proof.goal_message (fn () => |
|
243 |
[Pretty.str "", |
|
45666 | 244 |
Pretty.mark Isabelle_Markup.hilite (Pretty.str (message ()))] |
43006 | 245 |
|> Pretty.chunks)) |
41089 | 246 |
end |
247 |
else if blocking then |
|
43006 | 248 |
let |
249 |
val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go () |
|
250 |
in |
|
43058
5f8bac7a2945
minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents:
43052
diff
changeset
|
251 |
(if outcome_code = someN orelse mode = Normal then |
5f8bac7a2945
minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents:
43052
diff
changeset
|
252 |
quote name ^ ": " ^ message () |
5f8bac7a2945
minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents:
43052
diff
changeset
|
253 |
else |
5f8bac7a2945
minimize automatically even if Metis failed, if the external prover was really fast
blanchet
parents:
43052
diff
changeset
|
254 |
"") |
43005
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset
|
255 |
|> Async_Manager.break_into_chunks |
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset
|
256 |
|> List.app Output.urgent_message; |
43006 | 257 |
(outcome_code, state) |
41089 | 258 |
end |
259 |
else |
|
43006 | 260 |
(Async_Manager.launch das_tool birth_time death_time (desc ()) |
43052
8d6a4978cc65
automatically minimize with Metis when this can be done within a few seconds
blanchet
parents:
43051
diff
changeset
|
261 |
((fn (outcome_code, message) => |
43059 | 262 |
(verbose orelse outcome_code = someN, |
263 |
message ())) o go); |
|
43006 | 264 |
(unknownN, state)) |
41089 | 265 |
end |
266 |
||
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
267 |
fun class_of_smt_solver ctxt name = |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
268 |
ctxt |> select_smt_solver name |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
269 |
|> SMT_Config.solver_class_of |> SMT_Utils.string_of_class |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
270 |
|
43043
1406f6fc5dc3
normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
blanchet
parents:
43037
diff
changeset
|
271 |
(* Makes backtraces more transparent and might well be more efficient as |
1406f6fc5dc3
normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
blanchet
parents:
43037
diff
changeset
|
272 |
well. *) |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
273 |
fun smart_par_list_map _ [] = [] |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
274 |
| smart_par_list_map f [x] = [f x] |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
275 |
| smart_par_list_map f xs = Par_List.map f xs |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
276 |
|
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset
|
277 |
fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset
|
278 |
| dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact" |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset
|
279 |
|
43021 | 280 |
val auto_try_max_relevant_divisor = 2 (* FUDGE *) |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
281 |
|
42946 | 282 |
fun run_sledgehammer (params as {debug, verbose, blocking, provers, |
45706 | 283 |
relevance_thresholds, max_relevant, slice, |
42946 | 284 |
timeout, ...}) |
43021 | 285 |
mode i (relevance_override as {only, ...}) minimize_command state = |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
286 |
if null provers then |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
287 |
error "No prover is set." |
39318 | 288 |
else case subgoal_count state of |
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
289 |
0 => (Output.urgent_message "No subgoal!"; (false, (noneN, state))) |
39318 | 290 |
| n => |
291 |
let |
|
39364 | 292 |
val _ = Proof.assert_backward state |
43021 | 293 |
val print = if mode = Normal then Output.urgent_message else K () |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
294 |
val state = |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
295 |
state |> Proof.map_context (Config.put SMT_Config.verbose debug) |
40200 | 296 |
val ctxt = Proof.context_of state |
297 |
val {facts = chained_ths, goal, ...} = Proof.goal state |
|
43043
1406f6fc5dc3
normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
blanchet
parents:
43037
diff
changeset
|
298 |
val chained_ths = chained_ths |> normalize_chained_theorems |
43004
20e9caff1f86
fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
blanchet
parents:
42968
diff
changeset
|
299 |
val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i |
44625 | 300 |
val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers |
301 |
val facts = |
|
302 |
nearly_all_facts ctxt ho_atp relevance_override chained_ths hyp_ts |
|
303 |
concl_t |
|
44586 | 304 |
val _ = () |> not blocking ? kill_provers |
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41432
diff
changeset
|
305 |
val _ = case find_first (not o is_prover_supported ctxt) provers of |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
306 |
SOME name => error ("No such prover: " ^ name ^ ".") |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40723
diff
changeset
|
307 |
| NONE => () |
41773 | 308 |
val _ = print "Sledgehammering..." |
42944
9e620869a576
improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset
|
309 |
val (smts, (ueq_atps, full_atps)) = |
9e620869a576
improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset
|
310 |
provers |> List.partition (is_smt_prover ctxt) |
9e620869a576
improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset
|
311 |
||> List.partition (is_unit_equational_atp ctxt) |
41741 | 312 |
fun launch_provers state get_facts translate maybe_smt_filter provers = |
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset
|
313 |
let |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset
|
314 |
val facts = get_facts () |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset
|
315 |
val num_facts = length facts |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset
|
316 |
val facts = facts ~~ (0 upto num_facts - 1) |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset
|
317 |
|> map (translate num_facts) |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset
|
318 |
val problem = |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset
|
319 |
{state = state, goal = goal, subgoal = i, subgoal_count = n, |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset
|
320 |
facts = facts, |
41741 | 321 |
smt_filter = maybe_smt_filter |
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset
|
322 |
(fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i} |
43021 | 323 |
val launch = launch_prover params mode minimize_command only |
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset
|
324 |
in |
43021 | 325 |
if mode = Auto_Try orelse mode = Try then |
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
326 |
(unknownN, state) |
43021 | 327 |
|> fold (fn prover => fn accum as (outcome_code, _) => |
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
328 |
if outcome_code = someN then accum |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
329 |
else launch problem prover) |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
330 |
provers |
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset
|
331 |
else |
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset
|
332 |
provers |
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
333 |
|> (if blocking then smart_par_list_map else map) |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
334 |
(launch problem #> fst) |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
335 |
|> max_outcome_code |> rpair state |
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset
|
336 |
end |
42952
96f62b77748f
tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents:
42946
diff
changeset
|
337 |
fun get_facts label is_appropriate_prop relevance_fudge provers = |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
338 |
let |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
339 |
val max_max_relevant = |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
340 |
case max_relevant of |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
341 |
SOME n => n |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
342 |
| NONE => |
42443
724e612ba248
implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents:
42361
diff
changeset
|
343 |
0 |> fold (Integer.max |
45706 | 344 |
o default_max_relevant_for_prover ctxt slice) |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
345 |
provers |
43021 | 346 |
|> mode = Auto_Try |
347 |
? (fn n => n div auto_try_max_relevant_divisor) |
|
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
348 |
val is_built_in_const = |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
349 |
is_built_in_const_for_prover ctxt (hd provers) |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
350 |
in |
43351
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43306
diff
changeset
|
351 |
facts |
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43306
diff
changeset
|
352 |
|> (case is_appropriate_prop of |
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43306
diff
changeset
|
353 |
SOME is_app => filter (is_app o prop_of o snd) |
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43306
diff
changeset
|
354 |
| NONE => I) |
44625 | 355 |
|> relevant_facts ctxt relevance_thresholds max_max_relevant |
356 |
is_built_in_const relevance_fudge relevance_override |
|
357 |
chained_ths hyp_ts concl_t |
|
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
358 |
|> tap (fn facts => |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
359 |
if debug then |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
360 |
label ^ plural_s (length provers) ^ ": " ^ |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
361 |
(if null facts then |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
362 |
"Found no relevant facts." |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
363 |
else |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
364 |
"Including (up to) " ^ string_of_int (length facts) ^ |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
365 |
" relevant fact" ^ plural_s (length facts) ^ ":\n" ^ |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
366 |
(facts |> map (fst o fst) |> space_implode " ") ^ ".") |
41773 | 367 |
|
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
368 |
else |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
369 |
()) |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
370 |
end |
42952
96f62b77748f
tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents:
42946
diff
changeset
|
371 |
fun launch_atps label is_appropriate_prop atps accum = |
42946 | 372 |
if null atps then |
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset
|
373 |
accum |
43351
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43306
diff
changeset
|
374 |
else if is_some is_appropriate_prop andalso |
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43306
diff
changeset
|
375 |
not (the is_appropriate_prop concl_t) then |
42946 | 376 |
(if verbose orelse length atps = length provers then |
377 |
"Goal outside the scope of " ^ |
|
378 |
space_implode " " (serial_commas "and" (map quote atps)) ^ "." |
|
379 |
|> Output.urgent_message |
|
380 |
else |
|
381 |
(); |
|
382 |
accum) |
|
41256
0e7d45cc005f
put the SMT weights back where they belong, so that they're also used by Mirabelle
blanchet
parents:
41255
diff
changeset
|
383 |
else |
42944
9e620869a576
improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset
|
384 |
launch_provers state |
42952
96f62b77748f
tuning -- the "appropriate" terminology is inspired from TPTP
blanchet
parents:
42946
diff
changeset
|
385 |
(get_facts label is_appropriate_prop atp_relevance_fudge o K atps) |
42944
9e620869a576
improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset
|
386 |
(K (Untranslated_Fact o fst)) (K (K NONE)) atps |
41746
e590971528b2
run all provers in blocking mode, even if a proof was already found -- this behavior is less confusing to the user
blanchet
parents:
41743
diff
changeset
|
387 |
fun launch_smts accum = |
e590971528b2
run all provers in blocking mode, even if a proof was already found -- this behavior is less confusing to the user
blanchet
parents:
41743
diff
changeset
|
388 |
if null smts then |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
389 |
accum |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
390 |
else |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
391 |
let |
43351
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43306
diff
changeset
|
392 |
val facts = get_facts "SMT solver" NONE smt_relevance_fudge smts |
42646
4781fcd53572
replaced some Unsynchronized.refs with Config.Ts
blanchet
parents:
42642
diff
changeset
|
393 |
val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt |
41741 | 394 |
fun smt_filter facts = |
41788
adfd365c7ea4
added a timeout around SMT preprocessing (notably monomorphization)
blanchet
parents:
41773
diff
changeset
|
395 |
(if debug then curry (op o) SOME |
adfd365c7ea4
added a timeout around SMT preprocessing (notably monomorphization)
blanchet
parents:
41773
diff
changeset
|
396 |
else TimeLimit.timeLimit timeout o try) |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41335
diff
changeset
|
397 |
(SMT_Solver.smt_filter_preprocess state (facts ())) |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
398 |
in |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
399 |
smts |> map (`(class_of_smt_solver ctxt)) |
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
400 |
|> AList.group (op =) |
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
401 |
|> map (snd #> launch_provers state (K facts) weight smt_filter |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
402 |
#> fst) |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
403 |
|> max_outcome_code |> rpair state |
41242
8edeb1dbbc76
run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers
blanchet
parents:
41208
diff
changeset
|
404 |
end |
43351
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43306
diff
changeset
|
405 |
val launch_full_atps = launch_atps "ATP" NONE full_atps |
42944
9e620869a576
improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset
|
406 |
val launch_ueq_atps = |
43351
b19d95b4d736
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
blanchet
parents:
43306
diff
changeset
|
407 |
launch_atps "Unit equational provers" (SOME is_unit_equality) ueq_atps |
41262
095ecb0c687f
factored out running a prover with (optionally) an implicit minimizer phrase
blanchet
parents:
41260
diff
changeset
|
408 |
fun launch_atps_and_smt_solvers () = |
43043
1406f6fc5dc3
normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
blanchet
parents:
43037
diff
changeset
|
409 |
[launch_full_atps, launch_smts, launch_ueq_atps] |
43021 | 410 |
|> smart_par_list_map (fn f => ignore (f (unknownN, state))) |
41773 | 411 |
handle ERROR msg => (print ("Error: " ^ msg); error msg) |
43021 | 412 |
fun maybe f (accum as (outcome_code, _)) = |
413 |
accum |> (mode = Normal orelse outcome_code <> someN) ? f |
|
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
414 |
in |
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
415 |
(unknownN, state) |
42944
9e620869a576
improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset
|
416 |
|> (if blocking then |
43021 | 417 |
launch_full_atps |
418 |
#> mode <> Auto_Try ? (maybe launch_ueq_atps #> maybe launch_smts) |
|
42944
9e620869a576
improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset
|
419 |
else |
9e620869a576
improved Waldmeister support -- even run it by default on unit equational goals
blanchet
parents:
42850
diff
changeset
|
420 |
(fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p)) |
41773 | 421 |
handle TimeLimit.TimeOut => |
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
422 |
(print "Sledgehammer ran out of time."; (unknownN, state)) |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
423 |
end |
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
424 |
|> `(fn (outcome_code, _) => outcome_code = someN) |
38044 | 425 |
|
28582 | 426 |
end; |