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