author | blanchet |
Mon, 31 Jan 2022 16:09:23 +0100 | |
changeset 75018 | fcfd96a59625 |
parent 75017 | 30ccc472d486 |
child 75019 | 30a619de7973 |
permissions | -rw-r--r-- |
55205 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML |
2 |
Author: Fabian Immler, TU Muenchen |
|
3 |
Author: Makarius |
|
4 |
Author: Jasmin Blanchette, TU Muenchen |
|
5 |
||
6 |
ATPs as Sledgehammer provers. |
|
7 |
*) |
|
8 |
||
9 |
signature SLEDGEHAMMER_PROVER_ATP = |
|
10 |
sig |
|
11 |
type mode = Sledgehammer_Prover.mode |
|
12 |
type prover = Sledgehammer_Prover.prover |
|
13 |
||
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
14 |
val atp_problem_dest_dir : string Config.T |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
15 |
val atp_proof_dest_dir : string Config.T |
55212 | 16 |
val atp_problem_prefix : string Config.T |
62718 | 17 |
val atp_completish : int Config.T |
55212 | 18 |
val atp_full_names : bool Config.T |
19 |
||
20 |
val is_ho_atp : Proof.context -> string -> bool |
|
21 |
||
55205 | 22 |
val run_atp : mode -> string -> prover |
23 |
end; |
|
24 |
||
25 |
structure Sledgehammer_Prover_ATP : SLEDGEHAMMER_PROVER_ATP = |
|
26 |
struct |
|
27 |
||
28 |
open ATP_Util |
|
29 |
open ATP_Problem |
|
72399
f8900a5ad4a7
drop obsolete ad hoc support for Satallax isar proof reconstruction
desharna
parents:
71931
diff
changeset
|
30 |
open ATP_Problem_Generate |
55205 | 31 |
open ATP_Proof |
32 |
open ATP_Proof_Reconstruct |
|
33 |
open Sledgehammer_Util |
|
55287 | 34 |
open Sledgehammer_Proof_Methods |
55205 | 35 |
open Sledgehammer_Isar |
72400 | 36 |
open Sledgehammer_ATP_Systems |
55205 | 37 |
open Sledgehammer_Prover |
38 |
||
55212 | 39 |
(* Empty string means create files in Isabelle's temporary files directory. *) |
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
40 |
val atp_problem_dest_dir = |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
41 |
Attrib.setup_config_string \<^binding>\<open>sledgehammer_atp_problem_dest_dir\<close> (K "") |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
42 |
val atp_proof_dest_dir = |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
43 |
Attrib.setup_config_string \<^binding>\<open>sledgehammer_atp_proof_dest_dir\<close> (K "") |
55212 | 44 |
val atp_problem_prefix = |
69593 | 45 |
Attrib.setup_config_string \<^binding>\<open>sledgehammer_atp_problem_prefix\<close> (K "prob") |
46 |
val atp_completish = Attrib.setup_config_int \<^binding>\<open>sledgehammer_atp_completish\<close> (K 0) |
|
55212 | 47 |
(* In addition to being easier to read, readable names are often much shorter, especially if types |
48 |
are mangled in names. This makes a difference for some provers (e.g., E). For these reason, short |
|
49 |
names are enabled by default. *) |
|
69593 | 50 |
val atp_full_names = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_atp_full_names\<close> (K false) |
55212 | 51 |
|
52 |
fun is_atp_of_format is_format ctxt name = |
|
53 |
let val thy = Proof_Context.theory_of ctxt in |
|
54 |
(case try (get_atp thy) name of |
|
55 |
SOME config => |
|
56 |
exists (fn (_, ((_, format, _, _, _), _)) => is_format format) (#best_slices (config ()) ctxt) |
|
57 |
| NONE => false) |
|
58 |
end |
|
59 |
||
60 |
val is_ho_atp = is_atp_of_format is_format_higher_order |
|
61 |
||
55205 | 62 |
fun choose_type_enc strictness best_type_enc format = |
63 |
the_default best_type_enc |
|
64 |
#> type_enc_of_string strictness |
|
65 |
#> adjust_type_enc format |
|
66 |
||
67 |
fun has_bound_or_var_of_type pred = |
|
68 |
exists_subterm (fn Var (_, T as Type _) => pred T |
|
69 |
| Abs (_, T as Type _, _) => pred T |
|
70 |
| _ => false) |
|
71 |
||
72 |
(* Unwanted equalities are those between a (bound or schematic) variable that does not properly |
|
73 |
occur in the second operand. *) |
|
74 |
val is_exhaustive_finite = |
|
75 |
let |
|
76 |
fun is_bad_equal (Var z) t = |
|
77 |
not (exists_subterm (fn Var z' => z = z' | _ => false) t) |
|
78 |
| is_bad_equal (Bound j) t = not (loose_bvar1 (t, j)) |
|
79 |
| is_bad_equal _ _ = false |
|
80 |
fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1 |
|
81 |
fun do_formula pos t = |
|
55208 | 82 |
(case (pos, t) of |
74379 | 83 |
(_, \<^Const_>\<open>Trueprop for t1\<close>) => do_formula pos t1 |
69593 | 84 |
| (true, Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, _, t')) => do_formula pos t' |
85 |
| (true, Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t')) => do_formula pos t' |
|
86 |
| (false, Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, t')) => do_formula pos t' |
|
74379 | 87 |
| (_, \<^Const_>\<open>Pure.imp for t1 t2\<close>) => |
69593 | 88 |
do_formula (not pos) t1 andalso (t2 = \<^prop>\<open>False\<close> orelse do_formula pos t2) |
74379 | 89 |
| (_, \<^Const_>\<open>implies for t1 t2\<close>) => |
90 |
do_formula (not pos) t1 andalso (t2 = \<^Const>\<open>False\<close> orelse do_formula pos t2) |
|
91 |
| (_, \<^Const_>\<open>Not for t1\<close>) => do_formula (not pos) t1 |
|
92 |
| (true, \<^Const_>\<open>disj for t1 t2\<close>) => forall (do_formula pos) [t1, t2] |
|
93 |
| (false, \<^Const_>\<open>conj for t1 t2\<close>) => forall (do_formula pos) [t1, t2] |
|
69593 | 94 |
| (true, Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) => do_equals t1 t2 |
95 |
| (true, Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2) => do_equals t1 t2 |
|
55208 | 96 |
| _ => false) |
55205 | 97 |
in do_formula true end |
98 |
||
99 |
(* Facts containing variables of finite types such as "unit" or "bool" or of the form |
|
100 |
"ALL x. x = A | x = B | x = C" are likely to lead to untypable proofs for unsound type |
|
101 |
encodings. *) |
|
102 |
fun is_dangerous_prop ctxt = |
|
103 |
transform_elim_prop |
|
104 |
#> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf is_exhaustive_finite) |
|
105 |
||
106 |
val mono_max_privileged_facts = 10 |
|
107 |
||
108 |
fun suffix_of_mode Auto_Try = "_try" |
|
109 |
| suffix_of_mode Try = "_try" |
|
110 |
| suffix_of_mode Normal = "" |
|
111 |
| suffix_of_mode MaSh = "" |
|
112 |
| suffix_of_mode Minimize = "_min" |
|
113 |
||
57738 | 114 |
(* Important messages are important but not so important that users want to see them each time. *) |
55205 | 115 |
val atp_important_message_keep_quotient = 25 |
116 |
||
117 |
fun run_atp mode name |
|
75017
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
118 |
({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, max_facts, |
75018
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
119 |
max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, minimize, |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
120 |
slice, timeout, preplay_timeout, spy, ...} : params) |
75017
30ccc472d486
disable slicing within SMT (in preparation for factoring it out)
blanchet
parents:
75016
diff
changeset
|
121 |
({comment, state, goal, subgoal, subgoal_count, facts, found_proof, ...} : prover_problem) = |
55205 | 122 |
let |
123 |
val thy = Proof.theory_of state |
|
124 |
val ctxt = Proof.context_of state |
|
125 |
||
126 |
val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters, |
|
127 |
best_max_new_mono_instances, ...} = get_atp thy name () |
|
128 |
||
57671
dc5e1b1db9ba
avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
blanchet
parents:
57460
diff
changeset
|
129 |
val full_proofs = isar_proofs |> the_default (mode = Minimize) |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57266
diff
changeset
|
130 |
val local_name = perhaps (try (unprefix remote_prefix)) name |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57266
diff
changeset
|
131 |
|
62718 | 132 |
val completish = Config.get ctxt atp_completish |
133 |
val atp_mode = if completish > 0 then Sledgehammer_Completish completish else Sledgehammer |
|
55205 | 134 |
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt |
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
135 |
val (problem_dest_dir, proof_dest_dir, problem_prefix) = |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
136 |
if overlord then |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
137 |
overlord_file_location_of_prover name |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
138 |
|> (fn (dir, prefix) => (dir, dir, prefix)) |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
139 |
else |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
140 |
(Config.get ctxt atp_problem_dest_dir, |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
141 |
Config.get ctxt atp_proof_dest_dir, |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
142 |
Config.get ctxt atp_problem_prefix) |
55205 | 143 |
val problem_file_name = |
144 |
Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^ |
|
58085 | 145 |
suffix_of_mode mode ^ "_" ^ string_of_int subgoal) |
74893 | 146 |
|> Path.ext "p" |
55205 | 147 |
val prob_path = |
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
148 |
if problem_dest_dir = "" then |
55205 | 149 |
File.tmp_path problem_file_name |
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
150 |
else if File.exists (Path.explode problem_dest_dir) then |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
151 |
Path.explode problem_dest_dir + problem_file_name |
55205 | 152 |
else |
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
153 |
error ("No such directory: " ^ quote problem_dest_dir) |
73435
1cc848548f21
invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
wenzelm
parents:
73432
diff
changeset
|
154 |
val executable = |
55208 | 155 |
(case find_first (fn var => getenv var <> "") (fst exec) of |
55205 | 156 |
SOME var => |
157 |
let |
|
158 |
val pref = getenv var ^ "/" |
|
60978 | 159 |
val paths = |
160 |
map (Path.explode o prefix pref) |
|
161 |
(if ML_System.platform_is_windows then |
|
162 |
map (suffix ".exe") (snd exec) @ snd exec |
|
163 |
else snd exec); |
|
55205 | 164 |
in |
55208 | 165 |
(case find_first File.exists paths of |
55205 | 166 |
SOME path => path |
63692 | 167 |
| NONE => error ("Bad executable: " ^ Path.print (hd paths))) |
55205 | 168 |
end |
63692 | 169 |
| NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^ " is not set")) |
55205 | 170 |
|
171 |
fun run () = |
|
172 |
let |
|
75018
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
173 |
val (_, (((best_max_facts, _), format, best_type_enc, best_lam_trans, |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
174 |
best_uncurried_aliases), extra)) = |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
175 |
List.last (best_slices ctxt) |
55212 | 176 |
|
55205 | 177 |
fun monomorphize_facts facts = |
178 |
let |
|
179 |
val ctxt = |
|
180 |
ctxt |
|
181 |
|> repair_monomorph_context max_mono_iters best_max_mono_iters max_new_mono_instances |
|
182 |
best_max_new_mono_instances |
|
183 |
(* pseudo-theorem involving the same constants as the subgoal *) |
|
184 |
val subgoal_th = |
|
185 |
Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy |
|
186 |
val rths = |
|
187 |
facts |> chop mono_max_privileged_facts |
|
188 |
|>> map (pair 1 o snd) |
|
189 |
||> map (pair 2 o snd) |
|
190 |
|> op @ |
|
191 |
|> cons (0, subgoal_th) |
|
192 |
in |
|
193 |
Monomorph.monomorph atp_schematic_consts_of ctxt rths |
|
194 |
|> tl |> curry ListPair.zip (map fst facts) |
|
55208 | 195 |
|> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths) |
55205 | 196 |
end |
197 |
||
75018
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
198 |
val facts = snd facts |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
199 |
val num_facts = |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
200 |
(case max_facts of |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
201 |
NONE => best_max_facts |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
202 |
| SOME max_facts => max_facts) |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
203 |
|> Integer.min (length facts) |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
204 |
val strictness = if strict then Strict else Non_Strict |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
205 |
val type_enc = type_enc |> choose_type_enc strictness best_type_enc format |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
206 |
val run_timeout = if slice = Time.zeroTime then timeout else slice |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
207 |
val generous_run_timeout = if mode = MaSh then one_day else run_timeout |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
208 |
val ({elapsed, ...}, atp_problem_data as (atp_problem, _, _, _)) = Timing.timing (fn () => |
55205 | 209 |
let |
75018
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
210 |
val sound = is_type_enc_sound type_enc |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
211 |
val generate_info = (case format of DFG _ => true | _ => false) |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
212 |
val readable_names = not (Config.get ctxt atp_full_names) |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
213 |
val lam_trans = lam_trans |> the_default best_lam_trans |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
214 |
val uncurried_aliases = uncurried_aliases |> the_default best_uncurried_aliases |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
215 |
in |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
216 |
facts |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
217 |
|> not sound ? filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd) |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
218 |
|> take num_facts |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
219 |
|> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
220 |
|> map (apsnd Thm.prop_of) |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
221 |
|> generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
222 |
lam_trans uncurried_aliases readable_names true hyp_ts concl_t |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
223 |
end) () |
75000 | 224 |
|
75018
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
225 |
val () = spying spy (fn () => |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
226 |
(state, subgoal, name, "Generating ATP problem in " ^ |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
227 |
string_of_int (Time.toMilliseconds elapsed) ^ " ms")) |
55205 | 228 |
|
75018
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
229 |
fun sel_weights () = atp_problem_selection_weights atp_problem |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
230 |
fun ord_info () = atp_problem_term_order_info atp_problem |
55205 | 231 |
|
75018
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
232 |
val ord = effective_term_order ctxt name |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
233 |
val args = arguments ctxt full_proofs extra run_timeout prob_path |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
234 |
(ord, ord_info, sel_weights) |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
235 |
val command = space_implode " " (File.bash_path executable :: args) |
73435
1cc848548f21
invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
wenzelm
parents:
73432
diff
changeset
|
236 |
|
75018
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
237 |
fun run_command () = |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
238 |
if exec = isabelle_scala_function then |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
239 |
let val {output, timing} = SystemOnTPTP.run_system_encoded args |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
240 |
in (output, timing) end |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
241 |
else |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
242 |
let val res = Isabelle_System.bash_process (Bash.script command |> Bash.redirect) |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
243 |
in (Process_Result.out res, Process_Result.timing_elapsed res) end |
57263 | 244 |
|
75018
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
245 |
val _ = |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
246 |
atp_problem |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
247 |
|> lines_of_atp_problem format ord ord_info |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
248 |
|> (exec <> isabelle_scala_function) ? |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
249 |
cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
250 |
|> File.write_list prob_path |
75000 | 251 |
|
75018
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
252 |
val ((output, run_time), (atp_proof, outcome)) = |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
253 |
Timeout.apply generous_run_timeout run_command () |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
254 |
|>> overlord ? |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
255 |
(fn output => prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") output) |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
256 |
|> (fn accum as (output, _) => |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
257 |
(accum, |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
258 |
extract_tstplike_proof_and_outcome verbose proof_delims known_failures output |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
259 |
|>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name) |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
260 |
atp_problem |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
261 |
handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofUnparsable))) |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
262 |
handle Timeout.TIMEOUT _ => (("", run_timeout), ([], SOME TimedOut)) |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
263 |
| ERROR msg => (("", Time.zeroTime), ([], SOME (UnknownError msg))) |
55205 | 264 |
|
75018
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
265 |
val () = spying spy (fn () => |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
266 |
(state, subgoal, name, "Running command in " ^ |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
267 |
string_of_int (Time.toMilliseconds run_time) ^ " ms")) |
55205 | 268 |
|
75018
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
269 |
val outcome = |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
270 |
(case outcome of |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
271 |
NONE => |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
272 |
(case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof of |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
273 |
SOME facts => |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
274 |
let |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
275 |
val failure = UnsoundProof (is_type_enc_sound type_enc, sort string_ord facts) |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
276 |
in |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
277 |
if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
278 |
end |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
279 |
| NONE => (found_proof (); NONE)) |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
280 |
| _ => outcome) |
55205 | 281 |
in |
75018
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
282 |
(atp_problem_data, (output, run_time, facts, atp_proof, outcome), (format, type_enc)) |
55205 | 283 |
end |
284 |
||
285 |
(* If the problem file has not been exported, remove it; otherwise, export |
|
286 |
the proof file too. *) |
|
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
287 |
fun clean_up () = if problem_dest_dir = "" then (try File.rm prob_path; ()) else () |
57255
488046fdda59
add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents:
57245
diff
changeset
|
288 |
fun export (_, (output, _, _, _, _), _) = |
74893 | 289 |
let |
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
290 |
val proof_dest_dir_path = Path.explode proof_dest_dir |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
291 |
val make_export_file_name = |
74893 | 292 |
Path.split_ext |
293 |
#> apfst (Path.explode o suffix "_proof" o Path.implode) |
|
294 |
#> swap |
|
295 |
#> uncurry Path.ext |
|
296 |
in |
|
74981
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
297 |
if proof_dest_dir = "" then Output.system_message "don't export proof" |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
298 |
else if File.exists proof_dest_dir_path then |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
299 |
File.write (proof_dest_dir_path + make_export_file_name problem_file_name) output |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
300 |
else |
10df7a627ab6
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
desharna
parents:
74927
diff
changeset
|
301 |
error ("No such directory: " ^ quote proof_dest_dir) |
74893 | 302 |
end |
55208 | 303 |
|
75018
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
304 |
val ((_, pool, lifted, sym_tab), (output, run_time, used_from, atp_proof, outcome), |
fcfd96a59625
disable slicing within ATP module (in preparation for refactoring)
blanchet
parents:
75017
diff
changeset
|
305 |
(format, type_enc)) = |
55205 | 306 |
with_cleanup clean_up run () |> tap export |
55208 | 307 |
|
55205 | 308 |
val important_message = |
59172 | 309 |
if mode = Normal andalso Random.random_range 0 (atp_important_message_keep_quotient - 1) = 0 |
310 |
then extract_important_message output |
|
311 |
else "" |
|
55205 | 312 |
|
57738 | 313 |
val (used_facts, preferred_methss, message) = |
55205 | 314 |
(case outcome of |
315 |
NONE => |
|
316 |
let |
|
60924
610794dff23c
tuned signature, in accordance to sortBy in Scala;
wenzelm
parents:
59582
diff
changeset
|
317 |
val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof) |
55205 | 318 |
val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
319 |
val preferred_methss = |
57778
cf4215911f85
default on 'metis' for ATPs if preplaying is disabled
blanchet
parents:
57776
diff
changeset
|
320 |
(Metis_Method (NONE, NONE), |
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72511
diff
changeset
|
321 |
bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types |
73932
fd21b4a93043
added opaque_combs and renamed hide_lams to opaque_lifting
desharna
parents:
73604
diff
changeset
|
322 |
(if atp_proof_prefers_lifting atp_proof then liftingN else opaque_liftingN)) |
55205 | 323 |
in |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
324 |
(used_facts, preferred_methss, |
55205 | 325 |
fn preplay => |
326 |
let |
|
58843 | 327 |
val _ = if verbose then writeln "Generating proof text..." else () |
57263 | 328 |
|
55205 | 329 |
fun isar_params () = |
330 |
let |
|
331 |
val metis_type_enc = |
|
55257 | 332 |
if is_typed_helper_used_in_atp_proof atp_proof then SOME full_typesN else NONE |
333 |
val metis_lam_trans = |
|
334 |
if atp_proof_prefers_lifting atp_proof then SOME liftingN else NONE |
|
55205 | 335 |
val atp_proof = |
336 |
atp_proof |
|
70931 | 337 |
|> termify_atp_proof ctxt name format type_enc pool lifted sym_tab |
72401
2783779b7dd3
removed obsolete unmaintained experimental prover Pirate
blanchet
parents:
72400
diff
changeset
|
338 |
|> local_name = spassN ? introduce_spass_skolems |
57263 | 339 |
|> factify_atp_proof (map fst used_from) hyp_ts concl_t |
55205 | 340 |
in |
57245 | 341 |
(verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0, |
57721 | 342 |
minimize, atp_proof, goal) |
55205 | 343 |
end |
57263 | 344 |
|
57750 | 345 |
val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count) |
55205 | 346 |
val num_chained = length (#facts (Proof.goal state)) |
347 |
in |
|
57738 | 348 |
proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained |
349 |
one_line_params ^ |
|
350 |
(if important_message <> "" then |
|
351 |
"\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message |
|
352 |
else |
|
353 |
"") |
|
354 |
end) |
|
55205 | 355 |
end |
356 |
| SOME failure => |
|
57738 | 357 |
([], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)) |
55205 | 358 |
in |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
359 |
{outcome = outcome, used_facts = used_facts, used_from = used_from, |
57738 | 360 |
preferred_methss = preferred_methss, run_time = run_time, message = message} |
55205 | 361 |
end |
362 |
||
62391 | 363 |
end; |