blanchet@56629
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
|
smolkas@53692
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
smolkas@53692
|
3 |
Author: Steffen Juilf Smolka, TU Muenchen
|
smolkas@53692
|
4 |
|
smolkas@53692
|
5 |
Reconstructors.
|
smolkas@53692
|
6 |
*)
|
smolkas@53692
|
7 |
|
blanchet@56629
|
8 |
signature SLEDGEHAMMER_PROOF_METHODS =
|
smolkas@53692
|
9 |
sig
|
smolkas@53692
|
10 |
type stature = ATP_Problem_Generate.stature
|
smolkas@53692
|
11 |
|
blanchet@56627
|
12 |
datatype proof_method =
|
blanchet@56627
|
13 |
Metis_Method of string option * string option |
|
blanchet@56627
|
14 |
Meson_Method |
|
blanchet@57423
|
15 |
SMT2_Method |
|
blanchet@58194
|
16 |
SATx_Method |
|
blanchet@56665
|
17 |
Blast_Method |
|
blanchet@56627
|
18 |
Simp_Method |
|
blanchet@56627
|
19 |
Simp_Size_Method |
|
blanchet@56627
|
20 |
Auto_Method |
|
blanchet@56627
|
21 |
Fastforce_Method |
|
blanchet@56627
|
22 |
Force_Method |
|
blanchet@56665
|
23 |
Linarith_Method |
|
blanchet@56665
|
24 |
Presburger_Method |
|
blanchet@56627
|
25 |
Algebra_Method
|
smolkas@53692
|
26 |
|
blanchet@56166
|
27 |
datatype play_outcome =
|
blanchet@56166
|
28 |
Played of Time.time |
|
blanchet@56166
|
29 |
Play_Timed_Out of Time.time |
|
blanchet@57435
|
30 |
Play_Failed
|
smolkas@53692
|
31 |
|
smolkas@53692
|
32 |
type minimize_command = string list -> string
|
blanchet@56166
|
33 |
type one_line_params =
|
blanchet@56627
|
34 |
(proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
|
smolkas@53692
|
35 |
|
blanchet@58629
|
36 |
val is_proof_method_direct : proof_method -> bool
|
blanchet@58327
|
37 |
val string_of_proof_method : Proof.context -> string list -> proof_method -> string
|
blanchet@58396
|
38 |
val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
|
blanchet@56553
|
39 |
val string_of_play_outcome : play_outcome -> string
|
blanchet@56611
|
40 |
val play_outcome_ord : play_outcome * play_outcome -> order
|
blanchet@58327
|
41 |
val one_line_proof_text : Proof.context -> int -> one_line_params -> string
|
blanchet@55868
|
42 |
end;
|
smolkas@53692
|
43 |
|
blanchet@56629
|
44 |
structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS =
|
smolkas@53692
|
45 |
struct
|
smolkas@53692
|
46 |
|
blanchet@56170
|
47 |
open ATP_Util
|
smolkas@53692
|
48 |
open ATP_Problem_Generate
|
blanchet@56553
|
49 |
open ATP_Proof_Reconstruct
|
smolkas@53692
|
50 |
|
blanchet@56627
|
51 |
datatype proof_method =
|
blanchet@56627
|
52 |
Metis_Method of string option * string option |
|
blanchet@56627
|
53 |
Meson_Method |
|
blanchet@57423
|
54 |
SMT2_Method |
|
blanchet@58194
|
55 |
SATx_Method |
|
blanchet@56665
|
56 |
Blast_Method |
|
blanchet@56627
|
57 |
Simp_Method |
|
blanchet@56627
|
58 |
Simp_Size_Method |
|
blanchet@56627
|
59 |
Auto_Method |
|
blanchet@56627
|
60 |
Fastforce_Method |
|
blanchet@56627
|
61 |
Force_Method |
|
blanchet@56665
|
62 |
Linarith_Method |
|
blanchet@56665
|
63 |
Presburger_Method |
|
blanchet@56627
|
64 |
Algebra_Method
|
smolkas@53692
|
65 |
|
blanchet@56166
|
66 |
datatype play_outcome =
|
blanchet@56166
|
67 |
Played of Time.time |
|
blanchet@56166
|
68 |
Play_Timed_Out of Time.time |
|
blanchet@57435
|
69 |
Play_Failed
|
smolkas@53692
|
70 |
|
blanchet@56553
|
71 |
type minimize_command = string list -> string
|
blanchet@56553
|
72 |
type one_line_params =
|
blanchet@56627
|
73 |
(proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
|
blanchet@56553
|
74 |
|
blanchet@58629
|
75 |
fun is_proof_method_direct (Metis_Method _) = true
|
blanchet@58629
|
76 |
| is_proof_method_direct Meson_Method = true
|
blanchet@58629
|
77 |
| is_proof_method_direct SMT2_Method = true
|
blanchet@58629
|
78 |
| is_proof_method_direct Simp_Method = true
|
blanchet@58807
|
79 |
| is_proof_method_direct Simp_Size_Method = true
|
blanchet@58629
|
80 |
| is_proof_method_direct _ = false
|
blanchet@58629
|
81 |
|
blanchet@58325
|
82 |
fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")"
|
blanchet@58325
|
83 |
|
blanchet@58327
|
84 |
fun string_of_proof_method ctxt ss meth =
|
blanchet@58325
|
85 |
let
|
blanchet@58325
|
86 |
val meth_s =
|
blanchet@58325
|
87 |
(case meth of
|
blanchet@58325
|
88 |
Metis_Method (NONE, NONE) => "metis"
|
blanchet@58325
|
89 |
| Metis_Method (type_enc_opt, lam_trans_opt) =>
|
blanchet@58325
|
90 |
"metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
|
blanchet@58325
|
91 |
| Meson_Method => "meson"
|
blanchet@58325
|
92 |
| SMT2_Method => "smt2"
|
blanchet@58325
|
93 |
| SATx_Method => "satx"
|
blanchet@58325
|
94 |
| Blast_Method => "blast"
|
blanchet@58325
|
95 |
| Simp_Method => if null ss then "simp" else "simp add:"
|
blanchet@58327
|
96 |
| Simp_Size_Method => "simp add: " ^ short_thm_name ctxt @{thm size_ne_size_imp_ne}
|
blanchet@58325
|
97 |
| Auto_Method => "auto"
|
blanchet@58325
|
98 |
| Fastforce_Method => "fastforce"
|
blanchet@58325
|
99 |
| Force_Method => "force"
|
blanchet@58325
|
100 |
| Linarith_Method => "linarith"
|
blanchet@58325
|
101 |
| Presburger_Method => "presburger"
|
blanchet@58325
|
102 |
| Algebra_Method => "algebra")
|
blanchet@58325
|
103 |
in
|
blanchet@58325
|
104 |
maybe_paren (space_implode " " (meth_s :: ss))
|
blanchet@58325
|
105 |
end
|
blanchet@56627
|
106 |
|
blanchet@58807
|
107 |
val silence_methods = Try0.silence_methods false
|
blanchet@58632
|
108 |
|
blanchet@58396
|
109 |
fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
|
blanchet@58307
|
110 |
Method.insert_tac local_facts THEN'
|
blanchet@58307
|
111 |
(case meth of
|
blanchet@58307
|
112 |
Metis_Method (type_enc_opt, lam_trans_opt) =>
|
blanchet@58632
|
113 |
let val ctxt = Config.put Metis_Tactic.verbose false ctxt in
|
blanchet@58632
|
114 |
Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)]
|
blanchet@58632
|
115 |
(lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
|
blanchet@58632
|
116 |
end
|
blanchet@58807
|
117 |
| Meson_Method => Meson_Tactic.meson_general_tac (silence_methods ctxt) global_facts
|
blanchet@58632
|
118 |
| SMT2_Method =>
|
blanchet@58632
|
119 |
let val ctxt = Config.put SMT2_Config.verbose false ctxt in
|
blanchet@58632
|
120 |
SMT2_Solver.smt2_tac ctxt global_facts
|
blanchet@58632
|
121 |
end
|
blanchet@58807
|
122 |
| Simp_Method => Simplifier.asm_full_simp_tac (silence_methods ctxt addsimps global_facts)
|
blanchet@58807
|
123 |
| Simp_Size_Method =>
|
blanchet@59016
|
124 |
Simplifier.asm_full_simp_tac
|
blanchet@59016
|
125 |
(silence_methods ctxt addsimps (@{thm size_ne_size_imp_ne} :: global_facts))
|
blanchet@58307
|
126 |
| _ =>
|
blanchet@58307
|
127 |
Method.insert_tac global_facts THEN'
|
blanchet@56627
|
128 |
(case meth of
|
blanchet@58307
|
129 |
SATx_Method => SAT.satx_tac ctxt
|
blanchet@58307
|
130 |
| Blast_Method => blast_tac ctxt
|
blanchet@58807
|
131 |
| Auto_Method => K (Clasimp.auto_tac (silence_methods ctxt))
|
blanchet@58807
|
132 |
| Fastforce_Method => Clasimp.fast_force_tac (silence_methods ctxt)
|
blanchet@58807
|
133 |
| Force_Method => Clasimp.force_tac (silence_methods ctxt)
|
blanchet@58632
|
134 |
| Linarith_Method =>
|
blanchet@58632
|
135 |
let val ctxt = Config.put Lin_Arith.verbose false ctxt in Lin_Arith.tac ctxt end
|
blanchet@58307
|
136 |
| Presburger_Method => Cooper.tac true [] [] ctxt
|
blanchet@58307
|
137 |
| Algebra_Method => Groebner.algebra_tac [] [] ctxt))
|
blanchet@56553
|
138 |
|
blanchet@56170
|
139 |
fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
|
blanchet@57435
|
140 |
| string_of_play_outcome (Play_Timed_Out time) =
|
blanchet@57435
|
141 |
if time = Time.zeroTime then "" else string_of_ext_time (true, time) ^ ", timed out"
|
blanchet@56170
|
142 |
| string_of_play_outcome Play_Failed = "failed"
|
blanchet@56170
|
143 |
|
blanchet@56611
|
144 |
fun play_outcome_ord (Played time1, Played time2) =
|
blanchet@56611
|
145 |
int_ord (pairself Time.toMilliseconds (time1, time2))
|
blanchet@56611
|
146 |
| play_outcome_ord (Played _, _) = LESS
|
blanchet@56611
|
147 |
| play_outcome_ord (_, Played _) = GREATER
|
blanchet@56611
|
148 |
| play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) =
|
blanchet@56611
|
149 |
int_ord (pairself Time.toMilliseconds (time1, time2))
|
blanchet@56611
|
150 |
| play_outcome_ord (Play_Timed_Out _, _) = LESS
|
blanchet@56611
|
151 |
| play_outcome_ord (_, Play_Timed_Out _) = GREATER
|
blanchet@56611
|
152 |
| play_outcome_ord (Play_Failed, Play_Failed) = EQUAL
|
blanchet@56611
|
153 |
|
blanchet@56553
|
154 |
fun apply_on_subgoal _ 1 = "by "
|
blanchet@56553
|
155 |
| apply_on_subgoal 1 _ = "apply "
|
blanchet@58629
|
156 |
| apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
|
blanchet@56553
|
157 |
|
blanchet@56627
|
158 |
(* FIXME *)
|
blanchet@58327
|
159 |
fun proof_method_command ctxt meth i n _(*used_chaineds*) _(*num_chained*) ss =
|
blanchet@58629
|
160 |
let val (indirect_ss, direct_ss) = if is_proof_method_direct meth then ([], ss) else (ss, []) in
|
blanchet@58629
|
161 |
(if null indirect_ss then "" else "using " ^ space_implode " " indirect_ss ^ " ") ^
|
blanchet@58629
|
162 |
apply_on_subgoal i n ^ string_of_proof_method ctxt direct_ss meth
|
blanchet@58629
|
163 |
end
|
blanchet@56553
|
164 |
|
blanchet@57435
|
165 |
fun try_command_line banner play command =
|
blanchet@57435
|
166 |
let val s = string_of_play_outcome play in
|
blanchet@57435
|
167 |
banner ^ ": " ^ Active.sendback_markup [Markup.padding_command] command ^
|
blanchet@57435
|
168 |
(s |> s <> "" ? enclose " (" ")") ^ "."
|
blanchet@57435
|
169 |
end
|
blanchet@56553
|
170 |
|
blanchet@56553
|
171 |
fun minimize_line _ [] = ""
|
blanchet@56553
|
172 |
| minimize_line minimize_command ss =
|
blanchet@56553
|
173 |
(case minimize_command ss of
|
blanchet@56553
|
174 |
"" => ""
|
blanchet@56553
|
175 |
| command => "\nTo minimize: " ^ Active.sendback_markup [Markup.padding_command] command ^ ".")
|
blanchet@56553
|
176 |
|
blanchet@56553
|
177 |
fun split_used_facts facts =
|
blanchet@56553
|
178 |
facts
|
blanchet@56553
|
179 |
|> List.partition (fn (_, (sc, _)) => sc = Chained)
|
blanchet@56553
|
180 |
|> pairself (sort_distinct (string_ord o pairself fst))
|
blanchet@56553
|
181 |
|
blanchet@58327
|
182 |
fun one_line_proof_text ctxt num_chained
|
blanchet@56627
|
183 |
((meth, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
|
blanchet@56553
|
184 |
let
|
blanchet@56553
|
185 |
val (chained, extra) = split_used_facts used_facts
|
blanchet@56553
|
186 |
|
blanchet@56553
|
187 |
val try_line =
|
blanchet@56553
|
188 |
map fst extra
|
blanchet@58327
|
189 |
|> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained
|
blanchet@57435
|
190 |
|> (if play = Play_Failed then enclose "One-line proof reconstruction failed: " "."
|
blanchet@57435
|
191 |
else try_command_line banner play)
|
blanchet@56553
|
192 |
in
|
blanchet@56553
|
193 |
try_line ^ minimize_line minimize_command (map fst (extra @ chained))
|
blanchet@56553
|
194 |
end
|
smolkas@53692
|
195 |
|
blanchet@55868
|
196 |
end;
|