1(* Title: HOL/Tools/Sledgehammer/sledgehammer_prover.ML 2 Author: Fabian Immler, TU Muenchen 3 Author: Makarius 4 Author: Jasmin Blanchette, TU Muenchen 5 6Generic prover abstraction for Sledgehammer. 7*) 8 9signature SLEDGEHAMMER_PROVER = 10sig 11 type atp_failure = ATP_Proof.atp_failure 12 type stature = ATP_Problem_Generate.stature 13 type type_enc = ATP_Problem_Generate.type_enc 14 type fact = Sledgehammer_Fact.fact 15 type proof_method = Sledgehammer_Proof_Methods.proof_method 16 type play_outcome = Sledgehammer_Proof_Methods.play_outcome 17 18 datatype mode = Auto_Try | Try | Normal | Minimize | MaSh 19 20 type params = 21 {debug : bool, 22 verbose : bool, 23 overlord : bool, 24 spy : bool, 25 provers : string list, 26 type_enc : string option, 27 strict : bool, 28 lam_trans : string option, 29 uncurried_aliases : bool option, 30 learn : bool, 31 fact_filter : string option, 32 max_facts : int option, 33 fact_thresholds : real * real, 34 max_mono_iters : int option, 35 max_new_mono_instances : int option, 36 isar_proofs : bool option, 37 compress : real option, 38 try0 : bool, 39 smt_proofs : bool option, 40 slice : bool, 41 minimize : bool, 42 timeout : Time.time, 43 preplay_timeout : Time.time, 44 expect : string} 45 46 type prover_problem = 47 {comment : string, 48 state : Proof.state, 49 goal : thm, 50 subgoal : int, 51 subgoal_count : int, 52 factss : (string * fact list) list, 53 found_proof : unit -> unit} 54 55 type prover_result = 56 {outcome : atp_failure option, 57 used_facts : (string * stature) list, 58 used_from : fact list, 59 preferred_methss : proof_method * proof_method list list, 60 run_time : Time.time, 61 message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string} 62 63 type prover = params -> prover_problem -> prover_result 64 65 val SledgehammerN : string 66 val str_of_mode : mode -> string 67 val overlord_file_location_of_prover : string -> string * string 68 val proof_banner : mode -> string -> string 69 val is_atp : theory -> string -> bool 70 val bunches_of_proof_methods : bool -> bool -> bool -> string -> proof_method list list 71 val is_fact_chained : (('a * stature) * 'b) -> bool 72 val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list -> 73 ((''a * stature) * 'b) list 74 val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context -> 75 Proof.context 76 val supported_provers : Proof.context -> unit 77end; 78 79structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER = 80struct 81 82open ATP_Proof 83open ATP_Util 84open ATP_Systems 85open ATP_Problem 86open ATP_Problem_Generate 87open ATP_Proof_Reconstruct 88open Metis_Tactic 89open Sledgehammer_Fact 90open Sledgehammer_Proof_Methods 91 92(* Identifier that distinguishes Sledgehammer from other tools that could use "Async_Manager". *) 93val SledgehammerN = "Sledgehammer" 94 95datatype mode = Auto_Try | Try | Normal | Minimize | MaSh 96 97fun str_of_mode Auto_Try = "Auto Try" 98 | str_of_mode Try = "Try" 99 | str_of_mode Normal = "Normal" 100 | str_of_mode Minimize = "Minimize" 101 | str_of_mode MaSh = "MaSh" 102 103val is_atp = member (op =) o supported_atps 104 105type params = 106 {debug : bool, 107 verbose : bool, 108 overlord : bool, 109 spy : bool, 110 provers : string list, 111 type_enc : string option, 112 strict : bool, 113 lam_trans : string option, 114 uncurried_aliases : bool option, 115 learn : bool, 116 fact_filter : string option, 117 max_facts : int option, 118 fact_thresholds : real * real, 119 max_mono_iters : int option, 120 max_new_mono_instances : int option, 121 isar_proofs : bool option, 122 compress : real option, 123 try0 : bool, 124 smt_proofs : bool option, 125 slice : bool, 126 minimize : bool, 127 timeout : Time.time, 128 preplay_timeout : Time.time, 129 expect : string} 130 131type prover_problem = 132 {comment : string, 133 state : Proof.state, 134 goal : thm, 135 subgoal : int, 136 subgoal_count : int, 137 factss : (string * fact list) list, 138 found_proof : unit -> unit} 139 140type prover_result = 141 {outcome : atp_failure option, 142 used_facts : (string * stature) list, 143 used_from : fact list, 144 preferred_methss : proof_method * proof_method list list, 145 run_time : Time.time, 146 message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string} 147 148type prover = params -> prover_problem -> prover_result 149 150fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover) 151 152fun proof_banner mode name = 153 (case mode of 154 Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof" 155 | Try => "Sledgehammer (" ^ quote name ^ ") found a proof" 156 | _ => "Try this") 157 158fun bunches_of_proof_methods try0 smt_method needs_full_types desperate_lam_trans = 159 (if try0 then 160 [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method], 161 [Meson_Method, Fastforce_Method, Force_Method, Presburger_Method]] 162 else 163 []) @ 164 [[Metis_Method (if needs_full_types then SOME full_typesN else NONE, NONE)], 165 (if needs_full_types then 166 [Metis_Method (NONE, NONE), 167 Metis_Method (SOME really_full_type_enc, NONE), 168 Metis_Method (SOME full_typesN, SOME desperate_lam_trans), 169 Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)] 170 else 171 [Metis_Method (SOME full_typesN, NONE), 172 Metis_Method (SOME no_typesN, SOME desperate_lam_trans), 173 Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)])] @ 174 (if smt_method then [[SMT_Method]] else []) 175 176fun is_fact_chained ((_, (sc, _)), _) = sc = Chained 177 178fun filter_used_facts keep_chained used = 179 filter ((member (eq_fst (op =)) used o fst) orf 180 (if keep_chained then is_fact_chained else K false)) 181 182val max_fact_instances = 10 (* FUDGE *) 183 184fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances = 185 Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters) 186 #> Config.put Monomorph.max_new_instances 187 (max_new_instances |> the_default best_max_new_instances) 188 #> Config.put Monomorph.max_thm_instances max_fact_instances 189 190fun supported_provers ctxt = 191 let 192 val thy = Proof_Context.theory_of ctxt 193 val (remote_provers, local_provers) = 194 sort_strings (supported_atps thy) @ sort_strings (SMT_Config.available_solvers_of ctxt) 195 |> List.partition (String.isPrefix remote_prefix) 196 in 197 writeln ("Supported provers: " ^ commas (local_provers @ remote_provers)) 198 end 199 200end; 201