author | blanchet |
Thu, 16 Dec 2010 15:12:17 +0100 | |
changeset 41208 | 1b28c43a7074 |
parent 41138 | eb80538166b6 |
child 41242 | 8edeb1dbbc76 |
permissions | -rw-r--r-- |
38988 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_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 |
|
40977 | 5 |
Minimization of fact list for Metis using external 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 |
|
38988 | 8 |
signature SLEDGEHAMMER_MINIMIZE = |
32525 | 9 |
sig |
38988 | 10 |
type locality = Sledgehammer_Filter.locality |
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset
|
11 |
type params = Sledgehammer_Provers.params |
35867 | 12 |
|
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
13 |
val filter_used_facts : |
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
14 |
(string * locality) list -> ((string * locality) * thm list) list |
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
15 |
-> ((string * locality) * thm list) list |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
16 |
val minimize_facts : |
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
17 |
params -> bool -> int -> int -> Proof.state |
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
18 |
-> ((string * locality) * thm list) list |
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38745
diff
changeset
|
19 |
-> ((string * locality) * thm list) list option * string |
38996 | 20 |
val run_minimize : |
21 |
params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit |
|
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
22 |
end; |
32525 | 23 |
|
38988 | 24 |
structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE = |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
25 |
struct |
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
26 |
|
39496
a52a4e4399c1
got caught once again by SML's pattern maching (ctor vs. var)
blanchet
parents:
39491
diff
changeset
|
27 |
open ATP_Proof |
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36063
diff
changeset
|
28 |
open Sledgehammer_Util |
38988 | 29 |
open Sledgehammer_Filter |
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset
|
30 |
open Sledgehammer_Provers |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
31 |
|
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
32 |
(* wrapper for calling external prover *) |
31236 | 33 |
|
40553
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40342
diff
changeset
|
34 |
fun string_for_failure ATP_Proof.Unprovable = "Unprovable." |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40342
diff
changeset
|
35 |
| string_for_failure ATP_Proof.TimedOut = "Timed out." |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40342
diff
changeset
|
36 |
| string_for_failure ATP_Proof.Interrupted = "Interrupted." |
1264c9172338
pick up SMT solver crashes and report them to the user/Mirabelle if desired
blanchet
parents:
40342
diff
changeset
|
37 |
| string_for_failure _ = "Error." |
31236 | 38 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
39 |
fun n_facts names = |
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset
|
40 |
let val n = length names in |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
41 |
string_of_int n ^ " fact" ^ plural_s n ^ |
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
|
42 |
(if n > 0 then |
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset
|
43 |
": " ^ (names |> map fst |
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset
|
44 |
|> sort_distinct string_ord |> space_implode " ") |
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
|
45 |
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
|
46 |
"") |
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
|
47 |
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
|
48 |
|
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
49 |
fun print silent f = if silent then () else Output.urgent_message (f ()) |
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
50 |
|
41138
eb80538166b6
implemented partially-typed "tags" type encoding
blanchet
parents:
41134
diff
changeset
|
51 |
fun test_facts ({debug, overlord, provers, type_sys, isar_proof, |
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
52 |
isar_shrink_factor, ...} : params) silent (prover : prover) |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
53 |
explicit_apply timeout i n state facts = |
31236 | 54 |
let |
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
55 |
val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ "...") |
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
56 |
val params = |
41208
1b28c43a7074
make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive
blanchet
parents:
41138
diff
changeset
|
57 |
{debug = debug, verbose = false, overlord = overlord, blocking = true, |
41138
eb80538166b6
implemented partially-typed "tags" type encoding
blanchet
parents:
41134
diff
changeset
|
58 |
provers = provers, type_sys = type_sys, explicit_apply = explicit_apply, |
eb80538166b6
implemented partially-typed "tags" type encoding
blanchet
parents:
41134
diff
changeset
|
59 |
relevance_thresholds = (1.01, 1.01), max_relevant = NONE, |
eb80538166b6
implemented partially-typed "tags" type encoding
blanchet
parents:
41134
diff
changeset
|
60 |
isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, |
eb80538166b6
implemented partially-typed "tags" type encoding
blanchet
parents:
41134
diff
changeset
|
61 |
timeout = timeout, expect = ""} |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
62 |
val facts = |
41090 | 63 |
facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) |
40069 | 64 |
val {goal, ...} = Proof.goal state |
40065 | 65 |
val problem = |
66 |
{state = state, goal = goal, subgoal = i, subgoal_count = n, |
|
40983 | 67 |
facts = facts} |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
68 |
val result as {outcome, used_facts, ...} = prover params (K "") problem |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
69 |
in |
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
70 |
print silent |
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
71 |
(fn () => case outcome of |
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
72 |
SOME failure => string_for_failure failure |
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
73 |
| NONE => |
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
74 |
if length used_facts = length facts then "Found proof." |
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
75 |
else "Found proof with " ^ n_facts used_facts ^ "."); |
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
|
76 |
result |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
77 |
end |
31236 | 78 |
|
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
79 |
(* minimalization of facts *) |
31236 | 80 |
|
40977 | 81 |
(* The sublinear algorithm works well in almost all situations, except when the |
82 |
external prover cannot return the list of used facts and hence returns all |
|
83 |
facts as used. In that case, the binary algorithm is much more |
|
84 |
appropriate. We can usually detect that situation just by looking at the |
|
85 |
number of used facts reported by the prover. *) |
|
86 |
val binary_threshold = 50 |
|
87 |
||
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
88 |
fun filter_used_facts used = filter (member (op =) used o fst) |
38015 | 89 |
|
90 |
fun sublinear_minimize _ [] p = p |
|
91 |
| sublinear_minimize test (x :: xs) (seen, result) = |
|
92 |
case test (xs @ seen) of |
|
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
93 |
result as {outcome = NONE, used_facts, ...} : prover_result => |
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
94 |
sublinear_minimize test (filter_used_facts used_facts xs) |
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
95 |
(filter_used_facts used_facts seen, result) |
38015 | 96 |
| _ => sublinear_minimize test xs (x :: seen, result) |
97 |
||
40977 | 98 |
fun binary_minimize test xs = |
99 |
let |
|
100 |
fun p xs = #outcome (test xs : prover_result) = NONE |
|
101 |
fun split [] p = p |
|
102 |
| split [h] (l, r) = (h :: l, r) |
|
103 |
| split (h1 :: h2 :: t) (l, r) = split t (h1 :: l, h2 :: r) |
|
104 |
fun min _ [] = raise Empty |
|
105 |
| min _ [s0] = [s0] |
|
106 |
| min sup xs = |
|
107 |
let val (l0, r0) = split xs ([], []) in |
|
108 |
if p (sup @ l0) then |
|
109 |
min sup l0 |
|
110 |
else if p (sup @ r0) then |
|
111 |
min sup r0 |
|
112 |
else |
|
113 |
let |
|
114 |
val l = min (sup @ r0) l0 |
|
115 |
val r = min (sup @ l) r0 |
|
116 |
in l @ r end |
|
117 |
end |
|
118 |
val xs = |
|
119 |
case min [] xs of |
|
120 |
[x] => if p [] then [] else [x] |
|
121 |
| xs => xs |
|
122 |
in (xs, test xs) end |
|
123 |
||
124 |
(* Give the external prover some slack. The ATP gets further slack because the |
|
125 |
Sledgehammer preprocessing time is included in the estimate below but isn't |
|
126 |
part of the timeout. *) |
|
38590
bd443b426d56
get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize"
blanchet
parents:
38589
diff
changeset
|
127 |
val fudge_msecs = 1000 |
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
|
128 |
|
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
129 |
fun minimize_facts {provers = [], ...} _ _ _ _ _ = error "No prover is set." |
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
130 |
| minimize_facts (params as {provers = prover_name :: _, timeout, ...}) silent |
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
131 |
i n state facts = |
31236 | 132 |
let |
36378 | 133 |
val thy = Proof.theory_of state |
40941
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40553
diff
changeset
|
134 |
val ctxt = Proof.context_of state |
a3e6f8634a11
replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us
blanchet
parents:
40553
diff
changeset
|
135 |
val prover = get_prover ctxt false prover_name |
38590
bd443b426d56
get rid of "minimize_timeout", now that there's an automatic adaptive timeout mechanism in "minimize"
blanchet
parents:
38589
diff
changeset
|
136 |
val msecs = Time.toMilliseconds timeout |
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
137 |
val _ = print silent (fn () => "Sledgehammer minimize: " ^ |
40977 | 138 |
quote prover_name ^ ".") |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
139 |
val {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
|
140 |
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
|
141 |
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
|
142 |
not (forall (Meson.is_fol_term thy) |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
143 |
(concl_t :: hyp_ts @ maps (map prop_of o snd) facts)) |
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
144 |
fun do_test timeout = |
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
145 |
test_facts params silent prover explicit_apply timeout i n 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
|
146 |
val timer = Timer.startRealTimer () |
31236 | 147 |
in |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
148 |
(case do_test timeout facts of |
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
149 |
result as {outcome = NONE, used_facts, ...} => |
38015 | 150 |
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
|
151 |
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
|
152 |
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
|
153 |
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
|
154 |
|> Time.fromMilliseconds |
40977 | 155 |
val facts = filter_used_facts used_facts facts |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
156 |
val (min_thms, {message, ...}) = |
40977 | 157 |
if length facts >= binary_threshold then |
158 |
binary_minimize (do_test new_timeout) facts |
|
159 |
else |
|
160 |
sublinear_minimize (do_test new_timeout) facts ([], result) |
|
38094 | 161 |
val n = length min_thms |
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
162 |
val _ = print silent (fn () => cat_lines |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
163 |
["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^ |
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38745
diff
changeset
|
164 |
(case length (filter (curry (op =) Chained o snd o fst) min_thms) of |
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset
|
165 |
0 => "" |
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset
|
166 |
| n => " (including " ^ Int.toString n ^ " chained)") ^ ".") |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
167 |
in (SOME min_thms, message) end |
38015 | 168 |
| {outcome = SOME TimedOut, ...} => |
169 |
(NONE, "Timeout: You can increase the time limit using the \"timeout\" \ |
|
170 |
\option (e.g., \"timeout = " ^ |
|
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40205
diff
changeset
|
171 |
string_of_int (10 + msecs div 1000) ^ "\").") |
38015 | 172 |
| {outcome = SOME UnknownError, ...} => |
173 |
(* Failure sometimes mean timeout, unfortunately. *) |
|
174 |
(NONE, "Failure: No proof was found with the current time limit. You \ |
|
175 |
\can increase the time limit using the \"timeout\" \ |
|
176 |
\option (e.g., \"timeout = " ^ |
|
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40205
diff
changeset
|
177 |
string_of_int (10 + msecs div 1000) ^ "\").") |
40977 | 178 |
| {message, ...} => (NONE, "Prover error: " ^ message)) |
37994
b04307085a09
make TPTP generator accept full first-order formulas
blanchet
parents:
37926
diff
changeset
|
179 |
handle ERROR msg => (NONE, "Error: " ^ msg) |
31236 | 180 |
end |
181 |
||
38282
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38100
diff
changeset
|
182 |
fun run_minimize params i refs state = |
38045 | 183 |
let |
184 |
val ctxt = Proof.context_of state |
|
38696
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38617
diff
changeset
|
185 |
val reserved = reserved_isar_keyword_table () |
38045 | 186 |
val chained_ths = #facts (Proof.goal state) |
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
blanchet
parents:
40200
diff
changeset
|
187 |
val facts = |
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
188 |
refs |
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
189 |
|> maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths) |
38045 | 190 |
in |
191 |
case subgoal_count state of |
|
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
40114
diff
changeset
|
192 |
0 => Output.urgent_message "No subgoal!" |
38045 | 193 |
| n => |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39496
diff
changeset
|
194 |
(kill_provers (); |
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
195 |
Output.urgent_message (#2 (minimize_facts params false i n state facts))) |
38045 | 196 |
end |
197 |
||
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
198 |
end; |