author | blanchet |
Thu, 13 Feb 2014 13:16:16 +0100 | |
changeset 55451 | ea1d9408a233 |
parent 55323 | 253a029335a2 |
child 55452 | 29ec8680e61f |
permissions | -rw-r--r-- |
55287 | 1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML |
52555 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
Author: Steffen Juilf Smolka, TU Muenchen |
|
4 |
||
5 |
Reconstructors. |
|
6 |
*) |
|
7 |
||
55287 | 8 |
signature SLEDGEHAMMER_PROOF_METHODS = |
52555 | 9 |
sig |
10 |
type stature = ATP_Problem_Generate.stature |
|
11 |
||
55285 | 12 |
datatype proof_method = |
13 |
Metis_Method of string option * string option | |
|
14 |
Meson_Method | |
|
15 |
SMT_Method | |
|
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
16 |
Blast_Method | |
55285 | 17 |
Simp_Method | |
18 |
Simp_Size_Method | |
|
19 |
Auto_Method | |
|
20 |
Fastforce_Method | |
|
21 |
Force_Method | |
|
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
22 |
Linarith_Method | |
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
23 |
Presburger_Method | |
55285 | 24 |
Algebra_Method |
52555 | 25 |
|
54824 | 26 |
datatype play_outcome = |
27 |
Played of Time.time | |
|
28 |
Play_Timed_Out of Time.time | |
|
29 |
Play_Failed | |
|
30 |
Not_Played |
|
52555 | 31 |
|
32 |
type minimize_command = string list -> string |
|
54824 | 33 |
type one_line_params = |
55285 | 34 |
(proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int |
52555 | 35 |
|
55285 | 36 |
val string_of_proof_method : proof_method -> string |
37 |
val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic |
|
55211 | 38 |
val string_of_play_outcome : play_outcome -> string |
55269 | 39 |
val play_outcome_ord : play_outcome * play_outcome -> order |
55211 | 40 |
val one_line_proof_text : int -> one_line_params -> string |
55285 | 41 |
val silence_proof_methods : bool -> Proof.context -> Proof.context |
54495 | 42 |
end; |
52555 | 43 |
|
55287 | 44 |
structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS = |
52555 | 45 |
struct |
46 |
||
54828 | 47 |
open ATP_Util |
52555 | 48 |
open ATP_Problem_Generate |
55211 | 49 |
open ATP_Proof_Reconstruct |
52555 | 50 |
|
55285 | 51 |
datatype proof_method = |
52 |
Metis_Method of string option * string option | |
|
53 |
Meson_Method | |
|
54 |
SMT_Method | |
|
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
55 |
Blast_Method | |
55285 | 56 |
Simp_Method | |
57 |
Simp_Size_Method | |
|
58 |
Auto_Method | |
|
59 |
Fastforce_Method | |
|
60 |
Force_Method | |
|
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
61 |
Linarith_Method | |
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
62 |
Presburger_Method | |
55285 | 63 |
Algebra_Method |
52555 | 64 |
|
54824 | 65 |
datatype play_outcome = |
66 |
Played of Time.time | |
|
67 |
Play_Timed_Out of Time.time | |
|
68 |
Play_Failed | |
|
69 |
Not_Played |
|
52555 | 70 |
|
55211 | 71 |
type minimize_command = string list -> string |
72 |
type one_line_params = |
|
55285 | 73 |
(proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int |
55211 | 74 |
|
55285 | 75 |
fun string_of_proof_method meth = |
76 |
(case meth of |
|
77 |
Metis_Method (NONE, NONE) => "metis" |
|
78 |
| Metis_Method (type_enc_opt, lam_trans_opt) => |
|
79 |
"metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")" |
|
80 |
| Meson_Method => "meson" |
|
81 |
| SMT_Method => "smt" |
|
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
82 |
| Blast_Method => "blast" |
55285 | 83 |
| Simp_Method => "simp" |
84 |
| Simp_Size_Method => "simp add: size_ne_size_imp_ne" |
|
85 |
| Auto_Method => "auto" |
|
86 |
| Fastforce_Method => "fastforce" |
|
87 |
| Force_Method => "force" |
|
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
88 |
| Linarith_Method => "linarith" |
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
89 |
| Presburger_Method => "presburger" |
55285 | 90 |
| Algebra_Method => "algebra") |
91 |
||
92 |
fun tac_of_proof_method ctxt (local_facts, global_facts) meth = |
|
93 |
Method.insert_tac local_facts THEN' |
|
94 |
(case meth of |
|
95 |
Metis_Method (type_enc_opt, lam_trans_opt) => |
|
55315 | 96 |
Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)] |
55314 | 97 |
(lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts |
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
98 |
| Meson_Method => Meson.meson_tac ctxt global_facts |
55285 | 99 |
| SMT_Method => SMT_Solver.smt_tac ctxt global_facts |
100 |
| _ => |
|
101 |
Method.insert_tac global_facts THEN' |
|
102 |
(case meth of |
|
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
103 |
Blast_Method => blast_tac ctxt |
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
104 |
| Simp_Method => Simplifier.asm_full_simp_tac ctxt |
55285 | 105 |
| Simp_Size_Method => |
106 |
Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt) |
|
107 |
| Auto_Method => K (Clasimp.auto_tac ctxt) |
|
108 |
| Fastforce_Method => Clasimp.fast_force_tac ctxt |
|
109 |
| Force_Method => Clasimp.force_tac ctxt |
|
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
110 |
| Linarith_Method => Lin_Arith.tac ctxt |
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
111 |
| Presburger_Method => Cooper.tac true [] [] ctxt |
55285 | 112 |
| Algebra_Method => Groebner.algebra_tac [] [] ctxt)) |
55211 | 113 |
|
54828 | 114 |
fun string_of_play_outcome (Played time) = string_of_ext_time (false, time) |
115 |
| string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out" |
|
116 |
| string_of_play_outcome Play_Failed = "failed" |
|
117 |
| string_of_play_outcome _ = "unknown" |
|
118 |
||
55269 | 119 |
fun play_outcome_ord (Played time1, Played time2) = |
120 |
int_ord (pairself Time.toMilliseconds (time1, time2)) |
|
121 |
| play_outcome_ord (Played _, _) = LESS |
|
122 |
| play_outcome_ord (_, Played _) = GREATER |
|
123 |
| play_outcome_ord (Not_Played, Not_Played) = EQUAL |
|
124 |
| play_outcome_ord (Not_Played, _) = LESS |
|
125 |
| play_outcome_ord (_, Not_Played) = GREATER |
|
126 |
| play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) = |
|
127 |
int_ord (pairself Time.toMilliseconds (time1, time2)) |
|
128 |
| play_outcome_ord (Play_Timed_Out _, _) = LESS |
|
129 |
| play_outcome_ord (_, Play_Timed_Out _) = GREATER |
|
130 |
| play_outcome_ord (Play_Failed, Play_Failed) = EQUAL |
|
131 |
||
55211 | 132 |
(* FIXME: Various bugs, esp. with "unfolding" |
133 |
fun unusing_chained_facts _ 0 = "" |
|
134 |
| unusing_chained_facts used_chaineds num_chained = |
|
135 |
if length used_chaineds = num_chained then "" |
|
136 |
else if null used_chaineds then "(* using no facts *) " |
|
137 |
else "(* using only " ^ space_implode " " used_chaineds ^ " *) " |
|
138 |
*) |
|
139 |
||
140 |
fun apply_on_subgoal _ 1 = "by " |
|
141 |
| apply_on_subgoal 1 _ = "apply " |
|
142 |
| apply_on_subgoal i n = |
|
143 |
"prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n |
|
144 |
||
145 |
fun command_call name [] = |
|
146 |
name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")" |
|
147 |
| command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" |
|
148 |
||
55285 | 149 |
(* FIXME *) |
150 |
fun proof_method_command meth i n used_chaineds num_chained ss = |
|
55211 | 151 |
(* unusing_chained_facts used_chaineds num_chained ^ *) |
55285 | 152 |
apply_on_subgoal i n ^ command_call (string_of_proof_method meth) ss |
55211 | 153 |
|
154 |
fun show_time NONE = "" |
|
155 |
| show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")" |
|
156 |
||
157 |
fun try_command_line banner time command = |
|
158 |
banner ^ ": " ^ Active.sendback_markup [Markup.padding_command] command ^ show_time time ^ "." |
|
52555 | 159 |
|
55211 | 160 |
fun minimize_line _ [] = "" |
161 |
| minimize_line minimize_command ss = |
|
162 |
(case minimize_command ss of |
|
163 |
"" => "" |
|
164 |
| command => "\nTo minimize: " ^ Active.sendback_markup [Markup.padding_command] command ^ ".") |
|
165 |
||
166 |
fun split_used_facts facts = |
|
167 |
facts |
|
168 |
|> List.partition (fn (_, (sc, _)) => sc = Chained) |
|
169 |
|> pairself (sort_distinct (string_ord o pairself fst)) |
|
170 |
||
171 |
fun one_line_proof_text num_chained |
|
55285 | 172 |
((meth, play), banner, used_facts, minimize_command, subgoal, subgoal_count) = |
55211 | 173 |
let |
174 |
val (chained, extra) = split_used_facts used_facts |
|
175 |
||
176 |
val (failed, ext_time) = |
|
177 |
(case play of |
|
178 |
Played time => (false, (SOME (false, time))) |
|
179 |
| Play_Timed_Out time => (false, SOME (true, time)) |
|
180 |
| Play_Failed => (true, NONE) |
|
181 |
| Not_Played => (false, NONE)) |
|
182 |
||
183 |
val try_line = |
|
184 |
map fst extra |
|
55285 | 185 |
|> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained |
55451 | 186 |
|> (if failed then enclose "One-line proof reconstruction failed: " "." |
187 |
else try_command_line banner ext_time) |
|
55211 | 188 |
in |
189 |
try_line ^ minimize_line minimize_command (map fst (extra @ chained)) |
|
190 |
end |
|
52555 | 191 |
|
55285 | 192 |
(* Makes proof methods as silent as possible. The "set_visible" calls suppresses "Unification bound |
193 |
exceeded" warnings and the like. *) |
|
194 |
fun silence_proof_methods debug = |
|
55180 | 195 |
Try0.silence_methods debug |
55170 | 196 |
#> Config.put SMT_Config.verbose debug |
197 |
||
54495 | 198 |
end; |