author | wenzelm |
Fri, 04 Jan 2019 23:22:53 +0100 | |
changeset 69593 | 3dda49e08b9d |
parent 63692 | 1bc4bc2c9fd1 |
child 69597 | ff784d5a5bfb |
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 |
||
55212 | 14 |
val atp_dest_dir : string Config.T |
15 |
val atp_problem_prefix : string Config.T |
|
62718 | 16 |
val atp_completish : int Config.T |
55212 | 17 |
val atp_full_names : bool Config.T |
18 |
||
19 |
val is_ho_atp : Proof.context -> string -> bool |
|
20 |
||
55205 | 21 |
val run_atp : mode -> string -> prover |
22 |
end; |
|
23 |
||
24 |
structure Sledgehammer_Prover_ATP : SLEDGEHAMMER_PROVER_ATP = |
|
25 |
struct |
|
26 |
||
27 |
open ATP_Util |
|
28 |
open ATP_Problem |
|
29 |
open ATP_Proof |
|
30 |
open ATP_Problem_Generate |
|
31 |
open ATP_Proof_Reconstruct |
|
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57266
diff
changeset
|
32 |
open ATP_Waldmeister |
57707
0242e9578828
imported patch satallax_proof_support_Sledgehammer
fleury
parents:
57671
diff
changeset
|
33 |
open ATP_Satallax |
55205 | 34 |
open ATP_Systems |
35 |
open Sledgehammer_Util |
|
55287 | 36 |
open Sledgehammer_Proof_Methods |
55205 | 37 |
open Sledgehammer_Isar |
38 |
open Sledgehammer_Prover |
|
39 |
||
55212 | 40 |
(* Empty string means create files in Isabelle's temporary files directory. *) |
69593 | 41 |
val atp_dest_dir = Attrib.setup_config_string \<^binding>\<open>sledgehammer_atp_dest_dir\<close> (K "") |
55212 | 42 |
val atp_problem_prefix = |
69593 | 43 |
Attrib.setup_config_string \<^binding>\<open>sledgehammer_atp_problem_prefix\<close> (K "prob") |
44 |
val atp_completish = Attrib.setup_config_int \<^binding>\<open>sledgehammer_atp_completish\<close> (K 0) |
|
55212 | 45 |
(* In addition to being easier to read, readable names are often much shorter, especially if types |
46 |
are mangled in names. This makes a difference for some provers (e.g., E). For these reason, short |
|
47 |
names are enabled by default. *) |
|
69593 | 48 |
val atp_full_names = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_atp_full_names\<close> (K false) |
55212 | 49 |
|
50 |
fun is_atp_of_format is_format ctxt name = |
|
51 |
let val thy = Proof_Context.theory_of ctxt in |
|
52 |
(case try (get_atp thy) name of |
|
53 |
SOME config => |
|
54 |
exists (fn (_, ((_, format, _, _, _), _)) => is_format format) (#best_slices (config ()) ctxt) |
|
55 |
| NONE => false) |
|
56 |
end |
|
57 |
||
58 |
val is_ho_atp = is_atp_of_format is_format_higher_order |
|
59 |
||
55205 | 60 |
fun choose_type_enc strictness best_type_enc format = |
61 |
the_default best_type_enc |
|
62 |
#> type_enc_of_string strictness |
|
63 |
#> adjust_type_enc format |
|
64 |
||
65 |
fun has_bound_or_var_of_type pred = |
|
66 |
exists_subterm (fn Var (_, T as Type _) => pred T |
|
67 |
| Abs (_, T as Type _, _) => pred T |
|
68 |
| _ => false) |
|
69 |
||
70 |
(* Unwanted equalities are those between a (bound or schematic) variable that does not properly |
|
71 |
occur in the second operand. *) |
|
72 |
val is_exhaustive_finite = |
|
73 |
let |
|
74 |
fun is_bad_equal (Var z) t = |
|
75 |
not (exists_subterm (fn Var z' => z = z' | _ => false) t) |
|
76 |
| is_bad_equal (Bound j) t = not (loose_bvar1 (t, j)) |
|
77 |
| is_bad_equal _ _ = false |
|
78 |
fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1 |
|
79 |
fun do_formula pos t = |
|
55208 | 80 |
(case (pos, t) of |
55205 | 81 |
(_, @{const Trueprop} $ t1) => do_formula pos t1 |
69593 | 82 |
| (true, Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, _, t')) => do_formula pos t' |
83 |
| (true, Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t')) => do_formula pos t' |
|
84 |
| (false, Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, t')) => do_formula pos t' |
|
56245 | 85 |
| (_, @{const Pure.imp} $ t1 $ t2) => |
69593 | 86 |
do_formula (not pos) t1 andalso (t2 = \<^prop>\<open>False\<close> orelse do_formula pos t2) |
55205 | 87 |
| (_, @{const HOL.implies} $ t1 $ t2) => |
55208 | 88 |
do_formula (not pos) t1 andalso (t2 = @{const False} orelse do_formula pos t2) |
55205 | 89 |
| (_, @{const Not} $ t1) => do_formula (not pos) t1 |
90 |
| (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2] |
|
91 |
| (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2] |
|
69593 | 92 |
| (true, Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) => do_equals t1 t2 |
93 |
| (true, Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2) => do_equals t1 t2 |
|
55208 | 94 |
| _ => false) |
55205 | 95 |
in do_formula true end |
96 |
||
97 |
(* Facts containing variables of finite types such as "unit" or "bool" or of the form |
|
98 |
"ALL x. x = A | x = B | x = C" are likely to lead to untypable proofs for unsound type |
|
99 |
encodings. *) |
|
100 |
fun is_dangerous_prop ctxt = |
|
101 |
transform_elim_prop |
|
102 |
#> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf is_exhaustive_finite) |
|
103 |
||
104 |
fun get_slices slice slices = |
|
105 |
(0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single) |
|
106 |
||
107 |
fun get_facts_of_filter _ [(_, facts)] = facts |
|
108 |
| get_facts_of_filter fact_filter factss = |
|
109 |
(case AList.lookup (op =) factss fact_filter of |
|
110 |
SOME facts => facts |
|
111 |
| NONE => snd (hd factss)) |
|
112 |
||
113 |
(* For low values of "max_facts", this fudge value ensures that most slices are invoked with a |
|
114 |
nontrivial amount of facts. *) |
|
115 |
val max_fact_factor_fudge = 5 |
|
116 |
||
117 |
val mono_max_privileged_facts = 10 |
|
118 |
||
119 |
fun suffix_of_mode Auto_Try = "_try" |
|
120 |
| suffix_of_mode Try = "_try" |
|
121 |
| suffix_of_mode Normal = "" |
|
122 |
| suffix_of_mode MaSh = "" |
|
123 |
| suffix_of_mode Minimize = "_min" |
|
124 |
||
125 |
(* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on Linux appears to be |
|
126 |
the only ATP that does not honor its time limit. *) |
|
127 |
val atp_timeout_slack = seconds 1.0 |
|
128 |
||
57738 | 129 |
(* Important messages are important but not so important that users want to see them each time. *) |
55205 | 130 |
val atp_important_message_keep_quotient = 25 |
131 |
||
132 |
fun run_atp mode name |
|
57732 | 133 |
({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, fact_filter, |
134 |
max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, |
|
135 |
slice, minimize, timeout, preplay_timeout, ...} : params) |
|
62735 | 136 |
({comment, state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) = |
55205 | 137 |
let |
138 |
val thy = Proof.theory_of state |
|
139 |
val ctxt = Proof.context_of state |
|
140 |
||
141 |
val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters, |
|
142 |
best_max_new_mono_instances, ...} = get_atp thy name () |
|
143 |
||
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
|
144 |
val full_proofs = isar_proofs |> the_default (mode = Minimize) |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57266
diff
changeset
|
145 |
val local_name = perhaps (try (unprefix remote_prefix)) name |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57266
diff
changeset
|
146 |
val waldmeister_new = (local_name = waldmeister_newN) |
59577 | 147 |
val spassy = (local_name = pirateN orelse local_name = spassN) |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57266
diff
changeset
|
148 |
|
62718 | 149 |
val completish = Config.get ctxt atp_completish |
150 |
val atp_mode = if completish > 0 then Sledgehammer_Completish completish else Sledgehammer |
|
55205 | 151 |
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt |
152 |
val (dest_dir, problem_prefix) = |
|
153 |
if overlord then overlord_file_location_of_prover name |
|
55212 | 154 |
else (Config.get ctxt atp_dest_dir, Config.get ctxt atp_problem_prefix) |
55205 | 155 |
val problem_file_name = |
156 |
Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^ |
|
58085 | 157 |
suffix_of_mode mode ^ "_" ^ string_of_int subgoal) |
55205 | 158 |
val prob_path = |
159 |
if dest_dir = "" then |
|
160 |
File.tmp_path problem_file_name |
|
161 |
else if File.exists (Path.explode dest_dir) then |
|
162 |
Path.append (Path.explode dest_dir) problem_file_name |
|
163 |
else |
|
63692 | 164 |
error ("No such directory: " ^ quote dest_dir) |
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
|
165 |
val exec = exec full_proofs |
55205 | 166 |
val command0 = |
55208 | 167 |
(case find_first (fn var => getenv var <> "") (fst exec) of |
55205 | 168 |
SOME var => |
169 |
let |
|
170 |
val pref = getenv var ^ "/" |
|
60978 | 171 |
val paths = |
172 |
map (Path.explode o prefix pref) |
|
173 |
(if ML_System.platform_is_windows then |
|
174 |
map (suffix ".exe") (snd exec) @ snd exec |
|
175 |
else snd exec); |
|
55205 | 176 |
in |
55208 | 177 |
(case find_first File.exists paths of |
55205 | 178 |
SOME path => path |
63692 | 179 |
| NONE => error ("Bad executable: " ^ Path.print (hd paths))) |
55205 | 180 |
end |
63692 | 181 |
| NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^ " is not set")) |
55205 | 182 |
|
183 |
fun split_time s = |
|
184 |
let |
|
185 |
val split = String.tokens (fn c => str c = "\n") |
|
55249 | 186 |
val (output, t) = s |> split |> (try split_last #> the_default ([], "0")) |>> cat_lines |
187 |
val num = Scan.many1 Symbol.is_ascii_digit >> (fst o read_int) |
|
55205 | 188 |
val digit = Scan.one Symbol.is_ascii_digit |
55249 | 189 |
val num3 = digit ::: digit ::: (digit >> single) >> (fst o read_int) |
55205 | 190 |
val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b) |
55249 | 191 |
val as_time = raw_explode #> Scan.read Symbol.stopper time #> the_default 0 |
55205 | 192 |
in (output, as_time t |> Time.fromMilliseconds) end |
193 |
||
194 |
fun run () = |
|
195 |
let |
|
55208 | 196 |
(* If slicing is disabled, we expand the last slice to fill the entire time available. *) |
55205 | 197 |
val all_slices = best_slices ctxt |
198 |
val actual_slices = get_slices slice all_slices |
|
55276 | 199 |
|
200 |
fun max_facts_of_slices (slices : (real * (slice_spec * string)) list) = |
|
201 |
fold (Integer.max o fst o #1 o fst o snd) slices 0 |
|
202 |
||
55205 | 203 |
val num_actual_slices = length actual_slices |
204 |
val max_fact_factor = |
|
55248 | 205 |
Real.fromInt (case max_facts of NONE => max_facts_of_slices all_slices | SOME max => max) |
206 |
/ Real.fromInt (max_facts_of_slices (map snd actual_slices)) |
|
55212 | 207 |
|
55205 | 208 |
fun monomorphize_facts facts = |
209 |
let |
|
210 |
val ctxt = |
|
211 |
ctxt |
|
212 |
|> repair_monomorph_context max_mono_iters best_max_mono_iters max_new_mono_instances |
|
213 |
best_max_new_mono_instances |
|
214 |
(* pseudo-theorem involving the same constants as the subgoal *) |
|
215 |
val subgoal_th = |
|
216 |
Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy |
|
217 |
val rths = |
|
218 |
facts |> chop mono_max_privileged_facts |
|
219 |
|>> map (pair 1 o snd) |
|
220 |
||> map (pair 2 o snd) |
|
221 |
|> op @ |
|
222 |
|> cons (0, subgoal_th) |
|
223 |
in |
|
224 |
Monomorph.monomorph atp_schematic_consts_of ctxt rths |
|
225 |
|> tl |> curry ListPair.zip (map fst facts) |
|
55208 | 226 |
|> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths) |
55205 | 227 |
end |
228 |
||
55208 | 229 |
fun run_slice time_left (cache_key, cache_value) (slice, (time_frac, |
230 |
(key as ((best_max_facts, best_fact_filter), format, best_type_enc, best_lam_trans, |
|
55249 | 231 |
best_uncurried_aliases), |
55208 | 232 |
extra))) = |
55205 | 233 |
let |
55208 | 234 |
val effective_fact_filter = fact_filter |> the_default best_fact_filter |
55205 | 235 |
val facts = get_facts_of_filter effective_fact_filter factss |
236 |
val num_facts = |
|
237 |
Real.ceil (max_fact_factor * Real.fromInt best_max_facts) + max_fact_factor_fudge |
|
238 |
|> Integer.min (length facts) |
|
61860
2ce3d12015b3
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents:
61329
diff
changeset
|
239 |
val generate_info = (case format of DFG _ => true | _ => false) |
55205 | 240 |
val strictness = if strict then Strict else Non_Strict |
241 |
val type_enc = type_enc |> choose_type_enc strictness best_type_enc format |
|
242 |
val sound = is_type_enc_sound type_enc |
|
243 |
val real_ms = Real.fromInt o Time.toMilliseconds |
|
244 |
val slice_timeout = |
|
245 |
(real_ms time_left |
|
246 |
|> (if slice < num_actual_slices - 1 then |
|
247 |
curry Real.min (time_frac * real_ms timeout) |
|
248 |
else |
|
249 |
I)) |
|
250 |
* 0.001 |
|
251 |
|> seconds |
|
252 |
val generous_slice_timeout = |
|
62826 | 253 |
if mode = MaSh then one_day else slice_timeout + atp_timeout_slack |
55205 | 254 |
val _ = |
255 |
if debug then |
|
256 |
quote name ^ " slice #" ^ string_of_int (slice + 1) ^ |
|
257 |
" with " ^ string_of_int num_facts ^ " fact" ^ |
|
258 |
plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..." |
|
58843 | 259 |
|> writeln |
55205 | 260 |
else |
261 |
() |
|
262 |
val readable_names = not (Config.get ctxt atp_full_names) |
|
55208 | 263 |
val lam_trans = lam_trans |> the_default best_lam_trans |
264 |
val uncurried_aliases = uncurried_aliases |> the_default best_uncurried_aliases |
|
58142 | 265 |
val value as (atp_problem, _, _, _, _) = |
55205 | 266 |
if cache_key = SOME key then |
267 |
cache_value |
|
268 |
else |
|
269 |
facts |
|
59582 | 270 |
|> not sound ? filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd) |
55205 | 271 |
|> take num_facts |
272 |
|> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |
|
59582 | 273 |
|> map (apsnd Thm.prop_of) |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57266
diff
changeset
|
274 |
|> (if waldmeister_new then |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57266
diff
changeset
|
275 |
generate_waldmeister_problem ctxt hyp_ts concl_t |
61329
426c9c858099
added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs
blanchet
parents:
60978
diff
changeset
|
276 |
#> (fn (a, b, c, d, e) => (a, b, c, d, SOME e)) |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57266
diff
changeset
|
277 |
else |
61860
2ce3d12015b3
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents:
61329
diff
changeset
|
278 |
generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode |
2ce3d12015b3
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
blanchet
parents:
61329
diff
changeset
|
279 |
lam_trans uncurried_aliases readable_names true hyp_ts concl_t |
61329
426c9c858099
added "!=" (disequality) as a TPTP binary operator, since it pops up in LEO-II proofs
blanchet
parents:
60978
diff
changeset
|
280 |
#> (fn (a, b, c, d) => (a, b, c, d, NONE))) |
55205 | 281 |
|
282 |
fun sel_weights () = atp_problem_selection_weights atp_problem |
|
283 |
fun ord_info () = atp_problem_term_order_info atp_problem |
|
284 |
||
285 |
val ord = effective_term_order ctxt name |
|
286 |
val args = |
|
62549
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62519
diff
changeset
|
287 |
arguments ctxt full_proofs extra slice_timeout (File.bash_path prob_path) |
55205 | 288 |
(ord, ord_info, sel_weights) |
289 |
val command = |
|
62549
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62519
diff
changeset
|
290 |
"(exec 2>&1; " ^ File.bash_path command0 ^ " " ^ args ^ " " ^ ")" |
55205 | 291 |
|> enclose "TIMEFORMAT='%3R'; { time " " ; }" |
57263 | 292 |
|
55205 | 293 |
val _ = |
294 |
atp_problem |
|
295 |
|> lines_of_atp_problem format ord ord_info |
|
296 |
|> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) |
|
297 |
|> File.write_list prob_path |
|
57263 | 298 |
|
55205 | 299 |
val ((output, run_time), (atp_proof, outcome)) = |
62519 | 300 |
Timeout.apply generous_slice_timeout Isabelle_System.bash_output command |
55205 | 301 |
|>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I) |
302 |
|> fst |> split_time |
|
303 |
|> (fn accum as (output, _) => |
|
57776
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57750
diff
changeset
|
304 |
(accum, |
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57750
diff
changeset
|
305 |
extract_tstplike_proof_and_outcome verbose proof_delims known_failures output |
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57750
diff
changeset
|
306 |
|>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name) |
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57750
diff
changeset
|
307 |
atp_problem |
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57750
diff
changeset
|
308 |
handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofUnparsable))) |
62519 | 309 |
handle Timeout.TIMEOUT _ => (("", slice_timeout), ([], SOME TimedOut)) |
57263 | 310 |
|
55205 | 311 |
val outcome = |
312 |
(case outcome of |
|
313 |
NONE => |
|
57776
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57750
diff
changeset
|
314 |
(case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof of |
55208 | 315 |
SOME facts => |
57776
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57750
diff
changeset
|
316 |
let |
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57750
diff
changeset
|
317 |
val failure = UnsoundProof (is_type_enc_sound type_enc, sort string_ord facts) |
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57750
diff
changeset
|
318 |
in |
55208 | 319 |
if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure |
320 |
end |
|
62735 | 321 |
| NONE => (found_proof (); NONE)) |
55205 | 322 |
| _ => outcome) |
323 |
in |
|
57255
488046fdda59
add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents:
57245
diff
changeset
|
324 |
((SOME key, value), (output, run_time, facts, atp_proof, outcome), |
488046fdda59
add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents:
57245
diff
changeset
|
325 |
SOME (format, type_enc)) |
55205 | 326 |
end |
327 |
||
328 |
val timer = Timer.startRealTimer () |
|
329 |
||
57255
488046fdda59
add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents:
57245
diff
changeset
|
330 |
fun maybe_run_slice slice (result as (cache, (_, run_time0, _, _, SOME _), _)) = |
62826 | 331 |
let val time_left = timeout - Timer.checkRealTimer timer in |
332 |
if time_left <= Time.zeroTime then |
|
55205 | 333 |
result |
334 |
else |
|
335 |
run_slice time_left cache slice |
|
57255
488046fdda59
add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents:
57245
diff
changeset
|
336 |
|> (fn (cache, (output, run_time, used_from, atp_proof, outcome), |
488046fdda59
add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents:
57245
diff
changeset
|
337 |
format_type_enc) => |
62826 | 338 |
(cache, (output, run_time0 + run_time, used_from, atp_proof, outcome), |
57255
488046fdda59
add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents:
57245
diff
changeset
|
339 |
format_type_enc)) |
55205 | 340 |
end |
341 |
| maybe_run_slice _ result = result |
|
342 |
in |
|
58142 | 343 |
((NONE, ([], Symtab.empty, [], Symtab.empty,NONE)), |
57255
488046fdda59
add support for Isar reconstruction for thf1 ATP provers like Leo-II.
fleury
parents:
57245
diff
changeset
|
344 |
("", Time.zeroTime, [], [], SOME InternalError), NONE) |
55205 | 345 |
|> fold maybe_run_slice actual_slices |
346 |
end |
|
347 |
||
348 |
(* If the problem file has not been exported, remove it; otherwise, export |
|
349 |
the proof file too. *) |
|
55208 | 350 |
fun clean_up () = if 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
|
351 |
fun export (_, (output, _, _, _, _), _) = |
55205 | 352 |
if dest_dir = "" then () |
353 |
else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output |
|
55208 | 354 |
|
58142 | 355 |
val ((_, (_, pool, lifted, sym_tab,wm_info)), (output, run_time, used_from, atp_proof, outcome), |
57263 | 356 |
SOME (format, type_enc)) = |
55205 | 357 |
with_cleanup clean_up run () |> tap export |
55208 | 358 |
|
55205 | 359 |
val important_message = |
59172 | 360 |
if mode = Normal andalso Random.random_range 0 (atp_important_message_keep_quotient - 1) = 0 |
361 |
then extract_important_message output |
|
362 |
else "" |
|
55205 | 363 |
|
57738 | 364 |
val (used_facts, preferred_methss, message) = |
55205 | 365 |
(case outcome of |
366 |
NONE => |
|
367 |
let |
|
60924
610794dff23c
tuned signature, in accordance to sortBy in Scala;
wenzelm
parents:
59582
diff
changeset
|
368 |
val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof) |
55205 | 369 |
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
|
370 |
val preferred_methss = |
57778
cf4215911f85
default on 'metis' for ATPs if preplaying is disabled
blanchet
parents:
57776
diff
changeset
|
371 |
(Metis_Method (NONE, NONE), |
cf4215911f85
default on 'metis' for ATPs if preplaying is disabled
blanchet
parents:
57776
diff
changeset
|
372 |
bunches_of_proof_methods try0 (smt_proofs <> SOME false) needs_full_types |
cf4215911f85
default on 'metis' for ATPs if preplaying is disabled
blanchet
parents:
57776
diff
changeset
|
373 |
(if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)) |
55205 | 374 |
in |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
375 |
(used_facts, preferred_methss, |
55205 | 376 |
fn preplay => |
377 |
let |
|
58843 | 378 |
val _ = if verbose then writeln "Generating proof text..." else () |
57263 | 379 |
|
55205 | 380 |
fun isar_params () = |
381 |
let |
|
382 |
val metis_type_enc = |
|
55257 | 383 |
if is_typed_helper_used_in_atp_proof atp_proof then SOME full_typesN else NONE |
384 |
val metis_lam_trans = |
|
385 |
if atp_proof_prefers_lifting atp_proof then SOME liftingN else NONE |
|
55205 | 386 |
val atp_proof = |
387 |
atp_proof |
|
58142 | 388 |
|> (if waldmeister_new then termify_waldmeister_proof ctxt pool |
389 |
else termify_atp_proof ctxt name format type_enc pool lifted sym_tab) |
|
59577 | 390 |
|> spassy ? introduce_spassy_skolems |
58246
c723f55747fb
Fixed bug which broke isar proof construction for all ATPs except Waldmeister_new
steckerm
parents:
58142
diff
changeset
|
391 |
|> (if waldmeister_new then introduce_waldmeister_skolems (the wm_info) else I) |
57263 | 392 |
|> factify_atp_proof (map fst used_from) hyp_ts concl_t |
55205 | 393 |
in |
57245 | 394 |
(verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0, |
57721 | 395 |
minimize, atp_proof, goal) |
55205 | 396 |
end |
57263 | 397 |
|
57750 | 398 |
val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count) |
55205 | 399 |
val num_chained = length (#facts (Proof.goal state)) |
400 |
in |
|
57738 | 401 |
proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained |
402 |
one_line_params ^ |
|
403 |
(if important_message <> "" then |
|
404 |
"\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message |
|
405 |
else |
|
406 |
"") |
|
407 |
end) |
|
55205 | 408 |
end |
409 |
| SOME failure => |
|
57738 | 410 |
([], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)) |
55205 | 411 |
in |
57734
18bb3e1ff6f6
rationalized preplaying by eliminating (now superfluous) laziness
blanchet
parents:
57732
diff
changeset
|
412 |
{outcome = outcome, used_facts = used_facts, used_from = used_from, |
57738 | 413 |
preferred_methss = preferred_methss, run_time = run_time, message = message} |
55205 | 414 |
end |
415 |
||
62391 | 416 |
end; |