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