author | blanchet |
Thu, 10 Feb 2011 10:09:38 +0100 | |
changeset 41744 | a18e7bbca258 |
parent 41743 | d52af5722f0f |
child 41745 | 4b3edd6a375d |
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 |
|
41335
66edbd0f7a2e
added "smt_triggers" option to experiment with triggers in Sledgehammer;
blanchet
parents:
41277
diff
changeset
|
13 |
val binary_min_facts : int Unsynchronized.ref |
41255
a80024d7b71b
added debugging option to find out how good the relevance filter was at identifying relevant facts
blanchet
parents:
41242
diff
changeset
|
14 |
val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
15 |
val minimize_facts : |
41742
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
16 |
string -> params -> bool option -> bool -> int -> int -> Proof.state |
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
17 |
-> ((string * locality) * thm list) list |
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38745
diff
changeset
|
18 |
-> ((string * locality) * thm list) list option * string |
38996 | 19 |
val run_minimize : |
20 |
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
|
21 |
end; |
32525 | 22 |
|
38988 | 23 |
structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE = |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
24 |
struct |
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
diff
changeset
|
25 |
|
39496
a52a4e4399c1
got caught once again by SML's pattern maching (ctor vs. var)
blanchet
parents:
39491
diff
changeset
|
26 |
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
|
27 |
open Sledgehammer_Util |
38988 | 28 |
open Sledgehammer_Filter |
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
40983
diff
changeset
|
29 |
open Sledgehammer_Provers |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
30 |
|
36370
a4f601daa175
centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents:
36369
diff
changeset
|
31 |
(* wrapper for calling external prover *) |
31236 | 32 |
|
41277
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
33 |
fun short_string_for_failure ATP_Proof.Unprovable = "Unprovable." |
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
34 |
| short_string_for_failure ATP_Proof.TimedOut = "Timed out." |
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
35 |
| short_string_for_failure ATP_Proof.Interrupted = "Interrupted." |
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
36 |
| short_string_for_failure _ = "Error." |
31236 | 37 |
|
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
38 |
fun n_facts names = |
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset
|
39 |
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
|
40 |
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
|
41 |
(if n > 0 then |
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset
|
42 |
": " ^ (names |> map fst |
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset
|
43 |
|> 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
|
44 |
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
|
45 |
"") |
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 |
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
|
47 |
|
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
48 |
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
|
49 |
|
41277
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
50 |
fun test_facts ({debug, verbose, overlord, provers, type_sys, isar_proof, |
41742
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
51 |
isar_shrink_factor, ...} : params) |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
52 |
explicit_apply_opt silent (prover : prover) timeout i n state facts = |
31236 | 53 |
let |
41742
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
54 |
val thy = Proof.theory_of state |
41277
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
55 |
val _ = |
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
56 |
print silent (fn () => |
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
57 |
"Testing " ^ n_facts (map fst facts) ^ |
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
58 |
(if verbose then " (timeout: " ^ string_from_time timeout ^ ")" |
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
59 |
else "") ^ "...") |
41742
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
60 |
val {goal, ...} = Proof.goal state |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
61 |
val explicit_apply = |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
62 |
case explicit_apply_opt of |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
63 |
SOME explicit_apply => explicit_apply |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
64 |
| NONE => |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
65 |
let val (_, hyp_ts, concl_t) = strip_subgoal goal i in |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
66 |
not (forall (Meson.is_fol_term thy) |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
67 |
(concl_t :: hyp_ts @ maps (map prop_of o snd) facts)) |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
68 |
end |
38100
e458a0dd3dc1
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents:
38094
diff
changeset
|
69 |
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
|
70 |
{debug = debug, verbose = false, overlord = overlord, blocking = true, |
41138
eb80538166b6
implemented partially-typed "tags" type encoding
blanchet
parents:
41134
diff
changeset
|
71 |
provers = provers, type_sys = type_sys, explicit_apply = explicit_apply, |
eb80538166b6
implemented partially-typed "tags" type encoding
blanchet
parents:
41134
diff
changeset
|
72 |
relevance_thresholds = (1.01, 1.01), max_relevant = NONE, |
eb80538166b6
implemented partially-typed "tags" type encoding
blanchet
parents:
41134
diff
changeset
|
73 |
isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, |
eb80538166b6
implemented partially-typed "tags" type encoding
blanchet
parents:
41134
diff
changeset
|
74 |
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
|
75 |
val facts = |
41090 | 76 |
facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n)) |
40065 | 77 |
val problem = |
78 |
{state = state, goal = goal, subgoal = i, subgoal_count = n, |
|
41741 | 79 |
facts = facts, smt_filter = NONE} |
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
|
80 |
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
|
81 |
in |
41277
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
82 |
print silent (fn () => |
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
83 |
case outcome of |
41744 | 84 |
SOME failure => |
85 |
(if verbose then string_for_failure else short_string_for_failure) |
|
86 |
failure |
|
41277
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
87 |
| NONE => |
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
88 |
if length used_facts = length facts then "Found proof." |
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
89 |
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
|
90 |
result |
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36143
diff
changeset
|
91 |
end |
31236 | 92 |
|
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 |
(* minimalization of facts *) |
31236 | 94 |
|
40977 | 95 |
(* The sublinear algorithm works well in almost all situations, except when the |
96 |
external prover cannot return the list of used facts and hence returns all |
|
41267
958fee9ec275
lower threshold where the binary algorithm kick in and use the same value for automatic minimization
blanchet
parents:
41265
diff
changeset
|
97 |
facts as used. In that case, the binary algorithm is much more appropriate. |
958fee9ec275
lower threshold where the binary algorithm kick in and use the same value for automatic minimization
blanchet
parents:
41265
diff
changeset
|
98 |
We can usually detect the situation by looking at the number of used facts |
958fee9ec275
lower threshold where the binary algorithm kick in and use the same value for automatic minimization
blanchet
parents:
41265
diff
changeset
|
99 |
reported by the prover. *) |
41335
66edbd0f7a2e
added "smt_triggers" option to experiment with triggers in Sledgehammer;
blanchet
parents:
41277
diff
changeset
|
100 |
val binary_min_facts = Unsynchronized.ref 20 |
40977 | 101 |
|
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
|
102 |
fun filter_used_facts used = filter (member (op =) used o fst) |
38015 | 103 |
|
104 |
fun sublinear_minimize _ [] p = p |
|
105 |
| sublinear_minimize test (x :: xs) (seen, result) = |
|
106 |
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
|
107 |
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
|
108 |
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
|
109 |
(filter_used_facts used_facts seen, result) |
38015 | 110 |
| _ => sublinear_minimize test xs (x :: seen, result) |
111 |
||
40977 | 112 |
fun binary_minimize test xs = |
113 |
let |
|
114 |
fun p xs = #outcome (test xs : prover_result) = NONE |
|
115 |
fun split [] p = p |
|
116 |
| split [h] (l, r) = (h :: l, r) |
|
117 |
| split (h1 :: h2 :: t) (l, r) = split t (h1 :: l, h2 :: r) |
|
41743 | 118 |
fun min _ _ [] = raise Empty |
119 |
| min _ _ [s0] = [s0] |
|
120 |
| min depth sup xs = |
|
121 |
let |
|
122 |
(* |
|
123 |
val _ = warning (replicate_string depth " " ^ "{" ^ (" " ^ |
|
124 |
n_facts (map fst sup) ^ " and " ^ |
|
125 |
n_facts (map fst xs))) |
|
126 |
*) |
|
127 |
val (l0, r0) = split xs ([], []) |
|
128 |
in |
|
40977 | 129 |
if p (sup @ l0) then |
41743 | 130 |
min (depth + 1) sup l0 |
40977 | 131 |
else if p (sup @ r0) then |
41743 | 132 |
min (depth + 1) sup r0 |
40977 | 133 |
else |
134 |
let |
|
41743 | 135 |
val l = min (depth + 1) (sup @ r0) l0 |
136 |
val r = min (depth + 1) (sup @ l) r0 |
|
40977 | 137 |
in l @ r end |
138 |
end |
|
41743 | 139 |
(* |
140 |
|> tap (fn _ => warning (replicate_string depth " " ^ "}")) |
|
141 |
*) |
|
40977 | 142 |
val xs = |
41743 | 143 |
case min 0 [] xs of |
40977 | 144 |
[x] => if p [] then [] else [x] |
145 |
| xs => xs |
|
146 |
in (xs, test xs) end |
|
147 |
||
148 |
(* Give the external prover some slack. The ATP gets further slack because the |
|
149 |
Sledgehammer preprocessing time is included in the estimate below but isn't |
|
150 |
part of the timeout. *) |
|
41277
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
151 |
val slack_msecs = 200 |
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
|
152 |
|
41742
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
153 |
fun minimize_facts prover_name (params as {timeout, ...}) explicit_apply_opt |
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
154 |
silent i n state facts = |
31236 | 155 |
let |
36378 | 156 |
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
|
157 |
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
|
158 |
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
|
159 |
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
|
160 |
val _ = print silent (fn () => "Sledgehammer minimize: " ^ |
40977 | 161 |
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
|
162 |
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
|
163 |
fun do_test timeout = |
41742
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
164 |
test_facts params explicit_apply_opt silent prover 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
|
165 |
val timer = Timer.startRealTimer () |
31236 | 166 |
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
|
167 |
(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
|
168 |
result as {outcome = NONE, used_facts, ...} => |
38015 | 169 |
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
|
170 |
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
|
171 |
val new_timeout = |
41277
1369c27c6966
reduce the minimizer slack and add verbose information
blanchet
parents:
41267
diff
changeset
|
172 |
Int.min (msecs, Time.toMilliseconds time + slack_msecs) |
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
|
173 |
|> Time.fromMilliseconds |
40977 | 174 |
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
|
175 |
val (min_thms, {message, ...}) = |
41335
66edbd0f7a2e
added "smt_triggers" option to experiment with triggers in Sledgehammer;
blanchet
parents:
41277
diff
changeset
|
176 |
if length facts >= !binary_min_facts then |
40977 | 177 |
binary_minimize (do_test new_timeout) facts |
178 |
else |
|
179 |
sublinear_minimize (do_test new_timeout) facts ([], result) |
|
38094 | 180 |
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
|
181 |
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
|
182 |
["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^ |
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38745
diff
changeset
|
183 |
(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
|
184 |
0 => "" |
41491 | 185 |
| n => " (including " ^ string_of_int n ^ " chained)") ^ ".") |
40061
71cc5aac8b76
generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
blanchet
parents:
40060
diff
changeset
|
186 |
in (SOME min_thms, message) end |
38015 | 187 |
| {outcome = SOME TimedOut, ...} => |
188 |
(NONE, "Timeout: You can increase the time limit using the \"timeout\" \ |
|
189 |
\option (e.g., \"timeout = " ^ |
|
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40205
diff
changeset
|
190 |
string_of_int (10 + msecs div 1000) ^ "\").") |
41259
13972ced98d9
more precise error messages in "verbose" (or "debug") mode, following this morning's permission debacle
blanchet
parents:
41255
diff
changeset
|
191 |
| {outcome = SOME (UnknownError _), ...} => |
38015 | 192 |
(* Failure sometimes mean timeout, unfortunately. *) |
193 |
(NONE, "Failure: No proof was found with the current time limit. You \ |
|
194 |
\can increase the time limit using the \"timeout\" \ |
|
195 |
\option (e.g., \"timeout = " ^ |
|
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40205
diff
changeset
|
196 |
string_of_int (10 + msecs div 1000) ^ "\").") |
40977 | 197 |
| {message, ...} => (NONE, "Prover error: " ^ message)) |
37994
b04307085a09
make TPTP generator accept full first-order formulas
blanchet
parents:
37926
diff
changeset
|
198 |
handle ERROR msg => (NONE, "Error: " ^ msg) |
31236 | 199 |
end |
200 |
||
41265
a393d6d8e198
let each prover minimizes its own stuff (rather than taking the first prover of the list to minimize every prover's stuff)
blanchet
parents:
41259
diff
changeset
|
201 |
fun run_minimize (params as {provers, ...}) i refs state = |
38045 | 202 |
let |
203 |
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
|
204 |
val reserved = reserved_isar_keyword_table () |
38045 | 205 |
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
|
206 |
val facts = |
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
207 |
refs |
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41090
diff
changeset
|
208 |
|> maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths) |
38045 | 209 |
in |
210 |
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
|
211 |
0 => Output.urgent_message "No subgoal!" |
41265
a393d6d8e198
let each prover minimizes its own stuff (rather than taking the first prover of the list to minimize every prover's stuff)
blanchet
parents:
41259
diff
changeset
|
212 |
| n => case provers of |
a393d6d8e198
let each prover minimizes its own stuff (rather than taking the first prover of the list to minimize every prover's stuff)
blanchet
parents:
41259
diff
changeset
|
213 |
[] => error "No prover is set." |
a393d6d8e198
let each prover minimizes its own stuff (rather than taking the first prover of the list to minimize every prover's stuff)
blanchet
parents:
41259
diff
changeset
|
214 |
| prover :: _ => |
a393d6d8e198
let each prover minimizes its own stuff (rather than taking the first prover of the list to minimize every prover's stuff)
blanchet
parents:
41259
diff
changeset
|
215 |
(kill_provers (); |
41742
11e862c68b40
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41741
diff
changeset
|
216 |
minimize_facts prover params NONE false i n state facts |
41265
a393d6d8e198
let each prover minimizes its own stuff (rather than taking the first prover of the list to minimize every prover's stuff)
blanchet
parents:
41259
diff
changeset
|
217 |
|> #2 |> Output.urgent_message) |
38045 | 218 |
end |
219 |
||
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
220 |
end; |