author | blanchet |
Mon, 09 Aug 2010 12:05:48 +0200 | |
changeset 38282 | 319c59682c51 |
parent 38100 | src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML@e458a0dd3dc1 |
child 38283 | 1dac99cc8dbd |
permissions | -rw-r--r-- |
38282
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38100
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
2 |
Author: Philipp Meyer, TU Muenchen |
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
4 |
|
35867 | 5 |
Minimization of theorem list for Metis using automatic theorem provers. |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
6 |
*) |
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
7 |
|
38282
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38100
diff
changeset
|
8 |
signature SLEDGEHAMMER_FACT_MINIMIZE = |
32525 | 9 |
sig |
38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38015
diff
changeset
|
10 |
type params = Sledgehammer.params |
35867 | 11 |
|
38050 | 12 |
val minimize_theorems : |
13 |
params -> int -> int -> Proof.state -> (string * thm list) list |
|
14 |
-> (string * thm list) list option * string |
|
38282
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38100
diff
changeset
|
15 |
val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
16 |
end; |
32525 | 17 |
|
38282
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38100
diff
changeset
|
18 |
structure Sledgehammer_Fact_Minimize : SLEDGEHAMMER_FACT_MINIMIZE = |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
19 |
struct |
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
20 |
|
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
21 |
open ATP_Systems |
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset
|
22 |
open Sledgehammer_Util |
38045 | 23 |
open Sledgehammer_Fact_Filter |
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
35969
diff
changeset
|
24 |
open Sledgehammer_Proof_Reconstruct |
38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38015
diff
changeset
|
25 |
open Sledgehammer |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
26 |
|
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
27 |
(* wrapper for calling external prover *) |
31236 | 28 |
|
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
29 |
fun string_for_failure Unprovable = "Unprovable." |
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
30 |
| string_for_failure TimedOut = "Timed out." |
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
31 |
| string_for_failure _ = "Unknown error." |
31236 | 32 |
|
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
33 |
fun n_theorems name_thms_pairs = |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
34 |
let val n = length name_thms_pairs in |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
35 |
string_of_int n ^ " theorem" ^ plural_s n ^ |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
36 |
(if n > 0 then |
38093 | 37 |
": " ^ space_implode " " |
38 |
(name_thms_pairs |
|
39 |
|> map (perhaps (try (unprefix chained_prefix))) |
|
40 |
|> sort_distinct string_ord) |
|
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
41 |
else |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
42 |
"") |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
43 |
end |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
44 |
|
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
45 |
fun test_theorems ({debug, verbose, overlord, atps, full_types, |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
46 |
relevance_threshold, relevance_convergence, theory_relevant, |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
47 |
defs_relevant, isar_proof, isar_shrink_factor, |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
48 |
...} : params) |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
49 |
(prover : prover) explicit_apply timeout subgoal state |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
50 |
name_thms_pairs = |
31236 | 51 |
let |
38015 | 52 |
val _ = |
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
53 |
priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...") |
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
54 |
val params = |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
55 |
{debug = debug, verbose = verbose, overlord = overlord, atps = atps, |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
56 |
full_types = full_types, explicit_apply = explicit_apply, |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
57 |
relevance_threshold = relevance_threshold, |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
58 |
relevance_convergence = relevance_convergence, |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
59 |
theory_relevant = theory_relevant, defs_relevant = defs_relevant, |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
60 |
isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
61 |
timeout = timeout, minimize_timeout = timeout} |
38084
e2aac207d13b
"axiom_clauses" -> "axioms" (these are no longer clauses)
blanchet
parents:
38083
diff
changeset
|
62 |
val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs |
36263
56bf63d70120
use "Proof.goal" in Sledgehammer's minimizer (just like everywhere else in Sledgehammer), not "Proof.raw_goal"
blanchet
parents:
36232
diff
changeset
|
63 |
val {context = ctxt, facts, goal} = Proof.goal state |
32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32937
diff
changeset
|
64 |
val problem = |
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
35969
diff
changeset
|
65 |
{subgoal = subgoal, goal = (ctxt, (facts, goal)), |
35969 | 66 |
relevance_override = {add = [], del = [], only = false}, |
38084
e2aac207d13b
"axiom_clauses" -> "axioms" (these are no longer clauses)
blanchet
parents:
38083
diff
changeset
|
67 |
axioms = SOME axioms} |
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
68 |
val result as {outcome, used_thm_names, ...} = |
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
69 |
prover params (K "") problem |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
70 |
in |
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
71 |
priority (case outcome of |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
72 |
NONE => |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
73 |
if length used_thm_names = length name_thms_pairs then |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
74 |
"Found proof." |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
75 |
else |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
76 |
"Found proof with " ^ n_theorems used_thm_names ^ "." |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
77 |
| SOME failure => string_for_failure failure); |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
78 |
result |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
79 |
end |
31236 | 80 |
|
81 |
(* minimalization of thms *) |
|
82 |
||
38093 | 83 |
fun filter_used_facts used = |
84 |
filter (member (op =) used o perhaps (try (unprefix chained_prefix)) o fst) |
|
38015 | 85 |
|
86 |
fun sublinear_minimize _ [] p = p |
|
87 |
| sublinear_minimize test (x :: xs) (seen, result) = |
|
88 |
case test (xs @ seen) of |
|
89 |
result as {outcome = NONE, proof, used_thm_names, ...} |
|
90 |
: prover_result => |
|
91 |
sublinear_minimize test (filter_used_facts used_thm_names xs) |
|
92 |
(filter_used_facts used_thm_names seen, result) |
|
93 |
| _ => sublinear_minimize test xs (x :: seen, result) |
|
94 |
||
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
95 |
(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
96 |
preprocessing time is included in the estimate below but isn't part of the |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
97 |
timeout. *) |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
98 |
val fudge_msecs = 250 |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
99 |
|
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
100 |
fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set." |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
101 |
| minimize_theorems |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
102 |
(params as {debug, verbose, overlord, atps as atp :: _, full_types, |
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
103 |
relevance_threshold, relevance_convergence, theory_relevant, |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
104 |
defs_relevant, isar_proof, isar_shrink_factor, |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
105 |
minimize_timeout, ...}) |
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
106 |
i n state name_thms_pairs = |
31236 | 107 |
let |
36378 | 108 |
val thy = Proof.theory_of state |
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
109 |
val prover = get_prover_fun thy atp |
35969 | 110 |
val msecs = Time.toMilliseconds minimize_timeout |
31236 | 111 |
val _ = |
38282
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38100
diff
changeset
|
112 |
priority ("Sledgehammer minimize: ATP " ^ quote atp ^ |
36224 | 113 |
" with a time limit of " ^ string_of_int msecs ^ " ms.") |
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
114 |
val {context = ctxt, goal, ...} = Proof.goal state |
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
115 |
val (_, hyp_ts, concl_t) = strip_subgoal goal i |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
116 |
val explicit_apply = |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
117 |
not (forall (Meson.is_fol_term thy) |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
118 |
(concl_t :: hyp_ts @ maps (map prop_of o snd) name_thms_pairs)) |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
119 |
fun do_test timeout = |
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
120 |
test_theorems params prover explicit_apply timeout i state |
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
121 |
val timer = Timer.startRealTimer () |
31236 | 122 |
in |
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
123 |
(case do_test minimize_timeout name_thms_pairs of |
38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38050
diff
changeset
|
124 |
result as {outcome = NONE, pool, used_thm_names, |
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38050
diff
changeset
|
125 |
conjecture_shape, ...} => |
38015 | 126 |
let |
38092
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
127 |
val time = Timer.checkRealTimer timer |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
128 |
val new_timeout = |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
129 |
Int.min (msecs, Time.toMilliseconds time + fudge_msecs) |
81a003f7de0d
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents:
38084
diff
changeset
|
130 |
|> Time.fromMilliseconds |
38282
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38100
diff
changeset
|
131 |
val (min_thms, {proof, axiom_names, ...}) = |
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
132 |
sublinear_minimize (do_test new_timeout) |
38083
c4b57f68ddb3
remove the "extra_clauses" business introduced in 19a5f1c8a844;
blanchet
parents:
38050
diff
changeset
|
133 |
(filter_used_facts used_thm_names name_thms_pairs) ([], result) |
38094 | 134 |
val n = length min_thms |
38015 | 135 |
val _ = priority (cat_lines |
38094 | 136 |
["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ |
137 |
(case filter (String.isPrefix chained_prefix o fst) min_thms of |
|
138 |
[] => "" |
|
139 |
| chained => " (including " ^ Int.toString (length chained) ^ |
|
140 |
" chained)") ^ ".") |
|
38015 | 141 |
in |
142 |
(SOME min_thms, |
|
143 |
proof_text isar_proof |
|
144 |
(pool, debug, isar_shrink_factor, ctxt, conjecture_shape) |
|
38282
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38100
diff
changeset
|
145 |
(full_types, K "", proof, axiom_names, goal, i) |> fst) |
38015 | 146 |
end |
147 |
| {outcome = SOME TimedOut, ...} => |
|
148 |
(NONE, "Timeout: You can increase the time limit using the \"timeout\" \ |
|
149 |
\option (e.g., \"timeout = " ^ |
|
150 |
string_of_int (10 + msecs div 1000) ^ " s\").") |
|
151 |
| {outcome = SOME UnknownError, ...} => |
|
152 |
(* Failure sometimes mean timeout, unfortunately. *) |
|
153 |
(NONE, "Failure: No proof was found with the current time limit. You \ |
|
154 |
\can increase the time limit using the \"timeout\" \ |
|
155 |
\option (e.g., \"timeout = " ^ |
|
156 |
string_of_int (10 + msecs div 1000) ^ " s\").") |
|
157 |
| {message, ...} => (NONE, "ATP error: " ^ message)) |
|
37994
b04307085a09
make TPTP generator accept full first-order formulas
blanchet
parents:
37926
diff
changeset
|
158 |
handle ERROR msg => (NONE, "Error: " ^ msg) |
31236 | 159 |
end |
160 |
||
38282
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38100
diff
changeset
|
161 |
fun run_minimize params i refs state = |
38045 | 162 |
let |
163 |
val ctxt = Proof.context_of state |
|
164 |
val chained_ths = #facts (Proof.goal state) |
|
165 |
val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs |
|
166 |
in |
|
167 |
case subgoal_count state of |
|
168 |
0 => priority "No subgoal!" |
|
169 |
| n => |
|
170 |
(kill_atps (); |
|
171 |
priority (#2 (minimize_theorems params i n state name_thms_pairs))) |
|
172 |
end |
|
173 |
||
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
174 |
end; |