author | blanchet |
Mon, 01 Feb 2016 19:57:58 +0100 | |
changeset 62258 | 338bdbf14e31 |
parent 61330 | 20af2ad9261e |
child 62505 | 9e2a65912111 |
permissions | -rw-r--r-- |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer.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 |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
9 |
signature SLEDGEHAMMER = |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
10 |
sig |
60612
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
11 |
type stature = ATP_Problem_Generate.stature |
51008 | 12 |
type fact = Sledgehammer_Fact.fact |
48292 | 13 |
type fact_override = Sledgehammer_Fact.fact_override |
57755 | 14 |
type proof_method = Sledgehammer_Proof_Methods.proof_method |
15 |
type play_outcome = Sledgehammer_Proof_Methods.play_outcome |
|
55201 | 16 |
type mode = Sledgehammer_Prover.mode |
17 |
type params = Sledgehammer_Prover.params |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
18 |
|
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
19 |
val someN : string |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
20 |
val noneN : string |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
21 |
val timeoutN : string |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
22 |
val unknownN : string |
55212 | 23 |
|
60612
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
24 |
val play_one_line_proof : bool -> Time.time -> (string * stature) list -> Proof.state -> int -> |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
25 |
proof_method * proof_method list list -> (string * stature) list * (proof_method * play_outcome) |
51010 | 26 |
val string_of_factss : (string * fact list) list -> string |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54799
diff
changeset
|
27 |
val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override -> |
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message -- print outcome more directly;
wenzelm
parents:
58843
diff
changeset
|
28 |
Proof.state -> bool * (string * string list) |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
29 |
end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
30 |
|
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
31 |
structure Sledgehammer : SLEDGEHAMMER = |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
32 |
struct |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
33 |
|
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43064
diff
changeset
|
34 |
open ATP_Util |
55212 | 35 |
open ATP_Proof |
46320 | 36 |
open ATP_Problem_Generate |
38023 | 37 |
open Sledgehammer_Util |
48250
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
47904
diff
changeset
|
38 |
open Sledgehammer_Fact |
55287 | 39 |
open Sledgehammer_Proof_Methods |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57557
diff
changeset
|
40 |
open Sledgehammer_Isar_Proof |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57557
diff
changeset
|
41 |
open Sledgehammer_Isar_Preplay |
57740 | 42 |
open Sledgehammer_Isar_Minimize |
55201 | 43 |
open Sledgehammer_Prover |
55212 | 44 |
open Sledgehammer_Prover_ATP |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55201
diff
changeset
|
45 |
open Sledgehammer_Prover_Minimize |
48381 | 46 |
open Sledgehammer_MaSh |
40072
27f2a45b0aab
more robust handling of "remote_" vs. non-"remote_" provers
blanchet
parents:
40071
diff
changeset
|
47 |
|
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
48 |
val someN = "some" |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
49 |
val noneN = "none" |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
50 |
val timeoutN = "timeout" |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
51 |
val unknownN = "unknown" |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
52 |
|
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
53 |
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
|
54 |
|
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
55 |
fun max_outcome_code codes = |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
56 |
NONE |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
57 |
|> fold (fn candidate => |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57557
diff
changeset
|
58 |
fn accum as SOME _ => accum |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57557
diff
changeset
|
59 |
| NONE => if member (op =) codes candidate then SOME candidate else NONE) |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57557
diff
changeset
|
60 |
ordered_outcome_codes |
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
61 |
|> the_default unknownN |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43006
diff
changeset
|
62 |
|
57774
d2ad1320c770
honor 'dont_minimize' option when preplaying one-liner proof
blanchet
parents:
57755
diff
changeset
|
63 |
fun is_metis_method (Metis_Method _) = true |
d2ad1320c770
honor 'dont_minimize' option when preplaying one-liner proof
blanchet
parents:
57755
diff
changeset
|
64 |
| is_metis_method _ = false |
d2ad1320c770
honor 'dont_minimize' option when preplaying one-liner proof
blanchet
parents:
57755
diff
changeset
|
65 |
|
60612
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
66 |
fun play_one_line_proof minimize timeout used_facts0 state i (preferred_meth, methss) = |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
67 |
let val used_facts = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts0 in |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
68 |
if timeout = Time.zeroTime then |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
69 |
(used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
70 |
else |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
71 |
let |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
72 |
val ctxt = Proof.context_of state |
60548
e6adb8868478
use right context for preplay, to avoid errors in fact lookup
blanchet
parents:
59582
diff
changeset
|
73 |
|
60612
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
74 |
val fact_names = map fst used_facts |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
75 |
val {facts = chained, goal, ...} = Proof.goal state |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
76 |
val goal_t = Logic.get_goal (Thm.prop_of goal) i |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57557
diff
changeset
|
77 |
|
60612
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
78 |
fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
79 |
| try_methss ress [] = |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
80 |
(used_facts, |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
81 |
(case AList.lookup (op =) ress preferred_meth of |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
82 |
SOME play => (preferred_meth, play) |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
83 |
| NONE => hd (sort (play_outcome_ord o apply2 snd) (rev ress)))) |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
84 |
| try_methss ress (meths :: methss) = |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
85 |
let |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
86 |
fun mk_step fact_names meths = |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
87 |
Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "") |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
88 |
in |
62258
338bdbf14e31
preplaying of 'smt' and 'metis' more in sync with actual method
blanchet
parents:
61330
diff
changeset
|
89 |
(case preplay_isar_step ctxt chained timeout [] (mk_step fact_names meths) of |
60612
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
90 |
(res as (meth, Played time)) :: _ => |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
91 |
(* if a fact is needed by an ATP, it will be needed by "metis" *) |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
92 |
if not minimize orelse is_metis_method meth then |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
93 |
(used_facts, res) |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
94 |
else |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
95 |
let |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
96 |
val (time', used_names') = |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
97 |
minimized_isar_step ctxt time (mk_step fact_names [meth]) |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
98 |
||> (facts_of_isar_step #> snd) |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
99 |
val used_facts' = filter (member (op =) used_names' o fst) used_facts |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
100 |
in |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
101 |
(used_facts', (meth, Played time')) |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
102 |
end |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
103 |
| ress' => try_methss (ress' @ ress) methss) |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
104 |
end |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
105 |
in |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
106 |
try_methss [] methss |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
107 |
end |
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
60549
diff
changeset
|
108 |
end |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57557
diff
changeset
|
109 |
|
61311
150aa3015c47
removed legacy asynchronous mode in Sledgehammer
blanchet
parents:
61223
diff
changeset
|
110 |
fun launch_prover (params as {debug, verbose, spy, max_facts, minimize, timeout, preplay_timeout, |
150aa3015c47
removed legacy asynchronous mode in Sledgehammer
blanchet
parents:
61223
diff
changeset
|
111 |
expect, ...}) mode writeln_result only learn |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54799
diff
changeset
|
112 |
{comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name = |
41089 | 113 |
let |
114 |
val ctxt = Proof.context_of state |
|
53800 | 115 |
|
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54799
diff
changeset
|
116 |
val hard_timeout = time_mult 3.0 timeout |
54062 | 117 |
val _ = spying spy (fn () => (state, subgoal, name, "Launched")); |
54126
6675cdc0d1ae
if slicing is disabled, pick the maximum number of facts, not the number of facts in the last slice
blanchet
parents:
54090
diff
changeset
|
118 |
val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name) |
48293 | 119 |
val num_facts = length facts |> not only ? Integer.min max_facts |
53800 | 120 |
|
41089 | 121 |
val problem = |
54141
f57f8e7a879f
generate a comment storing the goal nickname in "learn_prover"
blanchet
parents:
54126
diff
changeset
|
122 |
{comment = comment, state = state, goal = goal, subgoal = subgoal, |
47904
67663c968d70
distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers
blanchet
parents:
47531
diff
changeset
|
123 |
subgoal_count = subgoal_count, |
53800 | 124 |
factss = factss |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57557
diff
changeset
|
125 |
|> map (apsnd ((not (is_ho_atp ctxt name) |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57557
diff
changeset
|
126 |
? filter_out (fn ((_, (_, Induction)), _) => true | _ => false)) |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57557
diff
changeset
|
127 |
#> take num_facts))} |
53800 | 128 |
|
51009
e8ff34a1fa9a
thread through fact triple component from which used facts come, for accurate index output
blanchet
parents:
51008
diff
changeset
|
129 |
fun print_used_facts used_facts used_from = |
e8ff34a1fa9a
thread through fact triple component from which used facts come, for accurate index output
blanchet
parents:
51008
diff
changeset
|
130 |
tag_list 1 used_from |
51005
ce4290c33d73
eliminated needless speed optimization -- and simplified code quite a bit
blanchet
parents:
51004
diff
changeset
|
131 |
|> map (fn (j, fact) => fact |> apsnd (K j)) |
48798 | 132 |
|> filter_used_facts false used_facts |
48394
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48384
diff
changeset
|
133 |
|> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48384
diff
changeset
|
134 |
|> commas |
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48384
diff
changeset
|
135 |
|> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ |
82fc8c956cdc
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents:
48384
diff
changeset
|
136 |
" proof (of " ^ string_of_int (length facts) ^ "): ") "." |
58843 | 137 |
|> writeln |
53800 | 138 |
|
54062 | 139 |
fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) = |
140 |
let |
|
141 |
val num_used_facts = length used_facts |
|
54063 | 142 |
|
143 |
fun find_indices facts = |
|
144 |
tag_list 1 facts |
|
54062 | 145 |
|> map (fn (j, fact) => fact |> apsnd (K j)) |
146 |
|> filter_used_facts false used_facts |
|
54773 | 147 |
|> distinct (eq_fst (op =)) |
54062 | 148 |
|> map (prefix "@" o string_of_int o snd) |
54063 | 149 |
|
150 |
fun filter_info (fact_filter, facts) = |
|
151 |
let |
|
152 |
val indices = find_indices facts |
|
54773 | 153 |
(* "Int.max" is there for robustness -- it shouldn't be necessary *) |
154 |
val unknowns = replicate (Int.max (0, num_used_facts - length indices)) "?" |
|
155 |
in |
|
156 |
(commas (indices @ unknowns), fact_filter) |
|
157 |
end |
|
54063 | 158 |
|
159 |
val filter_infos = |
|
160 |
map filter_info (("actual", used_from) :: factss) |
|
161 |
|> AList.group (op =) |
|
162 |
|> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices) |
|
54062 | 163 |
in |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57557
diff
changeset
|
164 |
"Success: Found proof with " ^ string_of_int num_used_facts ^ " of " ^ |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57557
diff
changeset
|
165 |
string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ |
54063 | 166 |
(if num_used_facts = 0 then "" else ": " ^ commas filter_infos) |
53800 | 167 |
end |
168 |
| spying_str_of_res {outcome = SOME failure, ...} = |
|
54062 | 169 |
"Failure: " ^ string_of_atp_failure failure |
53800 | 170 |
|
41255
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41245
diff
changeset
|
171 |
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
|
172 |
problem |
57735
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57734
diff
changeset
|
173 |
|> get_minimizing_prover ctxt mode learn name params |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57557
diff
changeset
|
174 |
|> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} => |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57557
diff
changeset
|
175 |
print_used_facts used_facts used_from |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57557
diff
changeset
|
176 |
| _ => ()) |
57056 | 177 |
|> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res))) |
57739 | 178 |
|> (fn {outcome, used_facts, preferred_methss, message, ...} => |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57557
diff
changeset
|
179 |
(if outcome = SOME ATP_Proof.TimedOut then timeoutN |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57557
diff
changeset
|
180 |
else if is_some outcome then noneN |
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57557
diff
changeset
|
181 |
else someN, |
57774
d2ad1320c770
honor 'dont_minimize' option when preplaying one-liner proof
blanchet
parents:
57755
diff
changeset
|
182 |
fn () => message (fn () => play_one_line_proof minimize preplay_timeout used_facts state |
d2ad1320c770
honor 'dont_minimize' option when preplaying one-liner proof
blanchet
parents:
57755
diff
changeset
|
183 |
subgoal preferred_methss))) |
53800 | 184 |
|
41089 | 185 |
fun go () = |
186 |
let |
|
187 |
val (outcome_code, message) = |
|
188 |
if debug then |
|
189 |
really_go () |
|
190 |
else |
|
191 |
(really_go () |
|
57056 | 192 |
handle |
193 |
ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n") |
|
194 |
| exn => |
|
195 |
if Exn.is_interrupt exn then reraise exn |
|
196 |
else (unknownN, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n")) |
|
197 |
||
41089 | 198 |
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
|
199 |
(* 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
|
200 |
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
|
201 |
machine. *) |
43e2b051339c
weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
blanchet
parents:
41138
diff
changeset
|
202 |
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
|
203 |
not (is_prover_installed ctxt name) then |
41089 | 204 |
() |
61311
150aa3015c47
removed legacy asynchronous mode in Sledgehammer
blanchet
parents:
61223
diff
changeset
|
205 |
else |
41089 | 206 |
error ("Unexpected outcome: " ^ quote outcome_code ^ ".") |
43005
c96f06bffd90
merge timeout messages from several ATPs into one message to avoid clutter
blanchet
parents:
43004
diff
changeset
|
207 |
in (outcome_code, message) end |
41089 | 208 |
in |
43021 | 209 |
if mode = Auto_Try then |
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents:
54799
diff
changeset
|
210 |
let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in |
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59058
diff
changeset
|
211 |
(outcome_code, if outcome_code = someN then [message ()] else []) |
41089 | 212 |
end |
61311
150aa3015c47
removed legacy asynchronous mode in Sledgehammer
blanchet
parents:
61223
diff
changeset
|
213 |
else |
43006 | 214 |
let |
215 |
val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go () |
|
53048
0f76e620561f
more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents:
52997
diff
changeset
|
216 |
val outcome = |
57056 | 217 |
if outcome_code = someN orelse mode = Normal then quote name ^ ": " ^ message () else "" |
53048
0f76e620561f
more direct sledgehammer configuration via mode = Normal_Result and output_result;
wenzelm
parents:
52997
diff
changeset
|
218 |
val _ = |
61312
6d779a71086d
further reduced dependency on legacy async thread manager
blanchet
parents:
61311
diff
changeset
|
219 |
if outcome <> "" andalso is_some writeln_result then the writeln_result outcome |
6d779a71086d
further reduced dependency on legacy async thread manager
blanchet
parents:
61311
diff
changeset
|
220 |
else writeln outcome |
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message -- print outcome more directly;
wenzelm
parents:
58843
diff
changeset
|
221 |
in (outcome_code, []) end |
41089 | 222 |
end |
223 |
||
48293 | 224 |
val auto_try_max_facts_divisor = 2 (* FUDGE *) |
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
40059
diff
changeset
|
225 |
|
51008 | 226 |
fun string_of_facts facts = |
57384 | 227 |
"Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ": " ^ |
51008 | 228 |
(facts |> map (fst o fst) |> space_implode " ") ^ "." |
229 |
||
51010 | 230 |
fun string_of_factss factss = |
57464 | 231 |
if forall (null o snd) factss then |
232 |
"Found no relevant facts." |
|
233 |
else |
|
234 |
cat_lines (map (fn (filter, facts) => |
|
235 |
(if filter = "" then "" else quote filter ^ ": ") ^ string_of_facts facts) factss) |
|
51008 | 236 |
|
61311
150aa3015c47
removed legacy asynchronous mode in Sledgehammer
blanchet
parents:
61223
diff
changeset
|
237 |
fun run_sledgehammer (params as {verbose, spy, provers, max_facts, ...}) mode writeln_result i |
150aa3015c47
removed legacy asynchronous mode in Sledgehammer
blanchet
parents:
61223
diff
changeset
|
238 |
(fact_override as {only, ...}) state = |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
239 |
if null provers then |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39494
diff
changeset
|
240 |
error "No prover is set." |
55286 | 241 |
else |
242 |
(case subgoal_count state of |
|
61311
150aa3015c47
removed legacy asynchronous mode in Sledgehammer
blanchet
parents:
61223
diff
changeset
|
243 |
0 => (error "No subgoal!"; (false, (noneN, []))) |
55286 | 244 |
| n => |
245 |
let |
|
246 |
val _ = Proof.assert_backward state |
|
247 |
val print = |
|
61223 | 248 |
if mode = Normal andalso is_none writeln_result then writeln else K () |
55286 | 249 |
val ctxt = Proof.context_of state |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58919
diff
changeset
|
250 |
val keywords = Thy_Header.get_keywords' ctxt |
55286 | 251 |
val {facts = chained, goal, ...} = Proof.goal state |
252 |
val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt |
|
253 |
val ho_atp = exists (is_ho_atp ctxt) provers |
|
254 |
val css = clasimpset_rule_table_of ctxt |
|
255 |
val all_facts = |
|
58919 | 256 |
nearly_all_facts ctxt ho_atp fact_override keywords css chained hyp_ts concl_t |
55286 | 257 |
val _ = |
258 |
(case find_first (not o is_prover_supported ctxt) provers of |
|
259 |
SOME name => error ("No such prover: " ^ name ^ ".") |
|
260 |
| NONE => ()) |
|
261 |
val _ = print "Sledgehammering..." |
|
57037 | 262 |
val _ = spying spy (fn () => (state, i, "***", "Starting " ^ str_of_mode mode ^ " mode")) |
54090
a28992e35032
run relevance filter only once for ATPs and SMT solvers, since it should now yield the same results anyway
blanchet
parents:
54063
diff
changeset
|
263 |
|
55286 | 264 |
val spying_str_of_factss = |
265 |
commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts)) |
|
53800 | 266 |
|
55286 | 267 |
fun get_factss provers = |
268 |
let |
|
269 |
val max_max_facts = |
|
270 |
(case max_facts of |
|
271 |
SOME n => n |
|
272 |
| NONE => |
|
273 |
0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers |
|
274 |
|> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)) |
|
275 |
val _ = spying spy (fn () => (state, i, "All", |
|
57557 | 276 |
"Filtering " ^ string_of_int (length all_facts) ^ " facts (MaSh algorithm: " ^ |
277 |
str_of_mash_algorithm (the_mash_algorithm ()) ^ ")")); |
|
55286 | 278 |
in |
279 |
all_facts |
|
280 |
|> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t |
|
281 |
|> tap (fn factss => if verbose then print (string_of_factss factss) else ()) |
|
282 |
|> spy ? tap (fn factss => spying spy (fn () => |
|
283 |
(state, i, "All", "Selected facts: " ^ spying_str_of_factss factss))) |
|
284 |
end |
|
53800 | 285 |
|
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message -- print outcome more directly;
wenzelm
parents:
58843
diff
changeset
|
286 |
fun launch_provers () = |
55286 | 287 |
let |
288 |
val factss = get_factss provers |
|
289 |
val problem = |
|
290 |
{comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, |
|
291 |
factss = factss} |
|
59582 | 292 |
val learn = mash_learn_proof ctxt params (Thm.prop_of goal) all_facts |
61223 | 293 |
val launch = launch_prover params mode writeln_result only learn |
55286 | 294 |
in |
295 |
if mode = Auto_Try then |
|
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message -- print outcome more directly;
wenzelm
parents:
58843
diff
changeset
|
296 |
(unknownN, []) |
55286 | 297 |
|> fold (fn prover => fn accum as (outcome_code, _) => |
57056 | 298 |
if outcome_code = someN then accum else launch problem prover) |
299 |
provers |
|
55286 | 300 |
else |
57387
2b6fe2a48352
reintroduced MaSh hints, this time as persistent creatures
blanchet
parents:
57384
diff
changeset
|
301 |
(learn chained; |
2b6fe2a48352
reintroduced MaSh hints, this time as persistent creatures
blanchet
parents:
57384
diff
changeset
|
302 |
provers |
61311
150aa3015c47
removed legacy asynchronous mode in Sledgehammer
blanchet
parents:
61223
diff
changeset
|
303 |
|> Par_List.map (launch problem #> fst) |
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message -- print outcome more directly;
wenzelm
parents:
58843
diff
changeset
|
304 |
|> max_outcome_code |> rpair []) |
55286 | 305 |
end |
306 |
in |
|
61311
150aa3015c47
removed legacy asynchronous mode in Sledgehammer
blanchet
parents:
61223
diff
changeset
|
307 |
launch_provers () |
150aa3015c47
removed legacy asynchronous mode in Sledgehammer
blanchet
parents:
61223
diff
changeset
|
308 |
handle TimeLimit.TimeOut => |
150aa3015c47
removed legacy asynchronous mode in Sledgehammer
blanchet
parents:
61223
diff
changeset
|
309 |
(print "Sledgehammer ran out of time."; (unknownN, [])) |
55286 | 310 |
end |
311 |
|> `(fn (outcome_code, _) => outcome_code = someN)) |
|
38044 | 312 |
|
28582 | 313 |
end; |