author | wenzelm |
Sat, 16 Aug 2014 13:23:50 +0200 | |
changeset 57948 | 75724d71013c |
parent 57777 | 563df8185d98 |
child 58061 | 3d060f43accb |
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 | |
56852
b38c5b9cf590
added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')
blanchet
parents:
56093
diff
changeset
|
16 |
SATx_Method | |
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
17 |
Blast_Method | |
55285 | 18 |
Simp_Method | |
19 |
Simp_Size_Method | |
|
20 |
Auto_Method | |
|
57744
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset
|
21 |
Auto_Choice_Method | |
55285 | 22 |
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
|
23 |
Linarith_Method | |
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
24 |
Presburger_Method | |
55285 | 25 |
Algebra_Method |
52555 | 26 |
|
54824 | 27 |
datatype play_outcome = |
28 |
Played of Time.time | |
|
29 |
Play_Timed_Out of Time.time | |
|
56093 | 30 |
Play_Failed |
52555 | 31 |
|
54824 | 32 |
type one_line_params = |
57739 | 33 |
((string * stature) list * (proof_method * play_outcome)) * string * int * int |
52555 | 34 |
|
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
35 |
val is_proof_method_direct : proof_method -> bool |
56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset
|
36 |
val string_of_proof_method : Proof.context -> string list -> proof_method -> string |
57054 | 37 |
val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic |
57720 | 38 |
val thms_influence_proof_method : Proof.context -> proof_method -> thm list -> bool |
55211 | 39 |
val string_of_play_outcome : play_outcome -> string |
55269 | 40 |
val play_outcome_ord : play_outcome * play_outcome -> order |
56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset
|
41 |
val one_line_proof_text : Proof.context -> int -> one_line_params -> string |
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 | |
|
56081 | 54 |
SMT2_Method | |
56852
b38c5b9cf590
added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')
blanchet
parents:
56093
diff
changeset
|
55 |
SATx_Method | |
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
56 |
Blast_Method | |
55285 | 57 |
Simp_Method | |
58 |
Simp_Size_Method | |
|
59 |
Auto_Method | |
|
57744
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset
|
60 |
Auto_Choice_Method | |
55285 | 61 |
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
|
62 |
Linarith_Method | |
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset
|
63 |
Presburger_Method | |
55285 | 64 |
Algebra_Method |
52555 | 65 |
|
54824 | 66 |
datatype play_outcome = |
67 |
Played of Time.time | |
|
68 |
Play_Timed_Out of Time.time | |
|
56093 | 69 |
Play_Failed |
52555 | 70 |
|
57739 | 71 |
type one_line_params = |
72 |
((string * stature) list * (proof_method * play_outcome)) * string * int * int |
|
55211 | 73 |
|
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
74 |
fun is_proof_method_direct (Metis_Method _) = true |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
75 |
| is_proof_method_direct Meson_Method = true |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
76 |
| is_proof_method_direct SMT2_Method = true |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
77 |
| is_proof_method_direct Simp_Method = true |
57465 | 78 |
| is_proof_method_direct Simp_Size_Method = true |
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
79 |
| is_proof_method_direct _ = false |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
80 |
|
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
81 |
fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
82 |
|
56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset
|
83 |
fun string_of_proof_method ctxt ss meth = |
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
84 |
let |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
85 |
val meth_s = |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
86 |
(case meth of |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
87 |
Metis_Method (NONE, NONE) => "metis" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
88 |
| Metis_Method (type_enc_opt, lam_trans_opt) => |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
89 |
"metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
90 |
| Meson_Method => "meson" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
91 |
| SMT2_Method => "smt2" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
92 |
| SATx_Method => "satx" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
93 |
| Blast_Method => "blast" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
94 |
| Simp_Method => if null ss then "simp" else "simp add:" |
56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset
|
95 |
| Simp_Size_Method => "simp add: " ^ short_thm_name ctxt @{thm size_ne_size_imp_ne} |
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
96 |
| Auto_Method => "auto" |
57744
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset
|
97 |
| Auto_Choice_Method => "atomize_elim, auto intro!: " ^ short_thm_name ctxt @{thm choice} |
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
98 |
| Force_Method => "force" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
99 |
| Linarith_Method => "linarith" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
100 |
| Presburger_Method => "presburger" |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
101 |
| Algebra_Method => "algebra") |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
102 |
in |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
103 |
maybe_paren (space_implode " " (meth_s :: ss)) |
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset
|
104 |
end |
55285 | 105 |
|
57465 | 106 |
val silence_methods = Try0.silence_methods false |
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57287
diff
changeset
|
107 |
|
57054 | 108 |
fun tac_of_proof_method ctxt (local_facts, global_facts) meth = |
56965
222f46a4dbec
new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents:
56951
diff
changeset
|
109 |
Method.insert_tac local_facts THEN' |
222f46a4dbec
new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents:
56951
diff
changeset
|
110 |
(case meth of |
222f46a4dbec
new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents:
56951
diff
changeset
|
111 |
Metis_Method (type_enc_opt, lam_trans_opt) => |
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57287
diff
changeset
|
112 |
let val ctxt = Config.put Metis_Tactic.verbose false ctxt in |
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57287
diff
changeset
|
113 |
Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)] |
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57287
diff
changeset
|
114 |
(lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts |
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57287
diff
changeset
|
115 |
end |
57465 | 116 |
| Meson_Method => Meson_Tactic.meson_general_tac (silence_methods ctxt) global_facts |
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57287
diff
changeset
|
117 |
| SMT2_Method => |
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57287
diff
changeset
|
118 |
let val ctxt = Config.put SMT2_Config.verbose false ctxt in |
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57287
diff
changeset
|
119 |
SMT2_Solver.smt2_tac ctxt global_facts |
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57287
diff
changeset
|
120 |
end |
57465 | 121 |
| Simp_Method => Simplifier.asm_full_simp_tac (silence_methods ctxt addsimps global_facts) |
122 |
| Simp_Size_Method => |
|
57674 | 123 |
Simplifier.asm_full_simp_tac |
124 |
(silence_methods ctxt addsimps (@{thm size_ne_size_imp_ne} :: global_facts)) |
|
56965
222f46a4dbec
new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents:
56951
diff
changeset
|
125 |
| _ => |
222f46a4dbec
new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents:
56951
diff
changeset
|
126 |
Method.insert_tac global_facts THEN' |
55285 | 127 |
(case meth of |
56965
222f46a4dbec
new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents:
56951
diff
changeset
|
128 |
SATx_Method => SAT.satx_tac ctxt |
222f46a4dbec
new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents:
56951
diff
changeset
|
129 |
| Blast_Method => blast_tac ctxt |
57744
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset
|
130 |
| Auto_Method => SELECT_GOAL (Clasimp.auto_tac (silence_methods ctxt)) |
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset
|
131 |
| Auto_Choice_Method => |
57948 | 132 |
Atomize_Elim.atomize_elim_tac ctxt THEN' |
57744
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset
|
133 |
SELECT_GOAL (Clasimp.auto_tac (silence_methods ctxt addSIs @{thms choice})) |
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset
|
134 |
| Force_Method => SELECT_GOAL (Clasimp.auto_tac (silence_methods ctxt)) |
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57287
diff
changeset
|
135 |
| Linarith_Method => |
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet
parents:
57287
diff
changeset
|
136 |
let val ctxt = Config.put Lin_Arith.verbose false ctxt in Lin_Arith.tac ctxt end |
56965
222f46a4dbec
new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents:
56951
diff
changeset
|
137 |
| Presburger_Method => Cooper.tac true [] [] ctxt |
222f46a4dbec
new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents:
56951
diff
changeset
|
138 |
| Algebra_Method => Groebner.algebra_tac [] [] ctxt)) |
55211 | 139 |
|
57744
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset
|
140 |
val simp_based_methods = |
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset
|
141 |
[Simp_Method, Simp_Size_Method, Auto_Method, Auto_Choice_Method, Force_Method] |
57675
47336af5d2b2
faster minimization by not adding facts that are already in the simpset
blanchet
parents:
57674
diff
changeset
|
142 |
|
57720 | 143 |
fun thms_influence_proof_method ctxt meth ths = |
57675
47336af5d2b2
faster minimization by not adding facts that are already in the simpset
blanchet
parents:
57674
diff
changeset
|
144 |
not (member (op =) simp_based_methods meth) orelse |
47336af5d2b2
faster minimization by not adding facts that are already in the simpset
blanchet
parents:
57674
diff
changeset
|
145 |
let val ctxt' = silence_methods ctxt in |
47336af5d2b2
faster minimization by not adding facts that are already in the simpset
blanchet
parents:
57674
diff
changeset
|
146 |
(* unfortunate pointer comparison -- but it's always safe to consider a theorem useful *) |
47336af5d2b2
faster minimization by not adding facts that are already in the simpset
blanchet
parents:
57674
diff
changeset
|
147 |
not (pointer_eq (ctxt' addsimps ths, ctxt')) |
47336af5d2b2
faster minimization by not adding facts that are already in the simpset
blanchet
parents:
57674
diff
changeset
|
148 |
end |
47336af5d2b2
faster minimization by not adding facts that are already in the simpset
blanchet
parents:
57674
diff
changeset
|
149 |
|
54828 | 150 |
fun string_of_play_outcome (Played time) = string_of_ext_time (false, time) |
56093 | 151 |
| string_of_play_outcome (Play_Timed_Out time) = |
152 |
if time = Time.zeroTime then "" else string_of_ext_time (true, time) ^ ", timed out" |
|
54828 | 153 |
| string_of_play_outcome Play_Failed = "failed" |
154 |
||
55269 | 155 |
fun play_outcome_ord (Played time1, Played time2) = |
156 |
int_ord (pairself Time.toMilliseconds (time1, time2)) |
|
157 |
| play_outcome_ord (Played _, _) = LESS |
|
158 |
| play_outcome_ord (_, Played _) = GREATER |
|
159 |
| play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) = |
|
160 |
int_ord (pairself Time.toMilliseconds (time1, time2)) |
|
161 |
| play_outcome_ord (Play_Timed_Out _, _) = LESS |
|
162 |
| play_outcome_ord (_, Play_Timed_Out _) = GREATER |
|
163 |
| play_outcome_ord (Play_Failed, Play_Failed) = EQUAL |
|
164 |
||
55211 | 165 |
fun apply_on_subgoal _ 1 = "by " |
166 |
| apply_on_subgoal 1 _ = "apply " |
|
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
167 |
| apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n |
55211 | 168 |
|
55285 | 169 |
(* FIXME *) |
56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset
|
170 |
fun proof_method_command ctxt meth i n _(*used_chaineds*) _(*num_chained*) ss = |
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
171 |
let val (indirect_ss, direct_ss) = if is_proof_method_direct meth then ([], ss) else (ss, []) in |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
172 |
(if null indirect_ss then "" else "using " ^ space_implode " " indirect_ss ^ " ") ^ |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
173 |
apply_on_subgoal i n ^ string_of_proof_method ctxt direct_ss meth |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57054
diff
changeset
|
174 |
end |
55211 | 175 |
|
56093 | 176 |
fun try_command_line banner play command = |
177 |
let val s = string_of_play_outcome play in |
|
178 |
banner ^ ": " ^ Active.sendback_markup [Markup.padding_command] command ^ |
|
179 |
(s |> s <> "" ? enclose " (" ")") ^ "." |
|
180 |
end |
|
52555 | 181 |
|
56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset
|
182 |
fun one_line_proof_text ctxt num_chained |
57739 | 183 |
((used_facts, (meth, play)), banner, subgoal, subgoal_count) = |
57777 | 184 |
let val (chained, extra) = List.partition (fn (_, (sc, _)) => sc = Chained) used_facts in |
57735
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57720
diff
changeset
|
185 |
map fst extra |
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57720
diff
changeset
|
186 |
|> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained |
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57720
diff
changeset
|
187 |
|> (if play = Play_Failed then enclose "One-line proof reconstruction failed: " "." |
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57720
diff
changeset
|
188 |
else try_command_line banner play) |
55211 | 189 |
end |
52555 | 190 |
|
54495 | 191 |
end; |