1(* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML 2 Author: Fabian Immler, TU Muenchen 3 Author: Makarius 4 Author: Jasmin Blanchette, TU Muenchen 5 6SMT solvers as Sledgehammer provers. 7*) 8 9signature SLEDGEHAMMER_PROVER_SMT = 10sig 11 type stature = ATP_Problem_Generate.stature 12 type mode = Sledgehammer_Prover.mode 13 type prover = Sledgehammer_Prover.prover 14 15 val smt_builtins : bool Config.T 16 val smt_triggers : bool Config.T 17 val smt_max_slices : int Config.T 18 val smt_slice_fact_frac : real Config.T 19 val smt_slice_time_frac : real Config.T 20 val smt_slice_min_secs : int Config.T 21 22 val is_smt_prover : Proof.context -> string -> bool 23 val run_smt_solver : mode -> string -> prover 24end; 25 26structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT = 27struct 28 29open ATP_Util 30open ATP_Proof 31open ATP_Systems 32open ATP_Problem_Generate 33open ATP_Proof_Reconstruct 34open Sledgehammer_Util 35open Sledgehammer_Proof_Methods 36open Sledgehammer_Isar 37open Sledgehammer_Prover 38 39val smt_builtins = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_builtins\<close> (K true) 40val smt_triggers = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_triggers\<close> (K true) 41 42val is_smt_prover = member (op =) o SMT_Config.available_solvers_of 43 44(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out 45 properly in the SMT module, we must interpret these here. *) 46val z3_failures = 47 [(101, OutOfResources), 48 (103, MalformedInput), 49 (110, MalformedInput), 50 (112, TimedOut)] 51val unix_failures = 52 [(134, Crashed), 53 (138, Crashed), 54 (139, Crashed)] 55val smt_failures = z3_failures @ unix_failures 56 57fun failure_of_smt_failure (SMT_Failure.Counterexample genuine) = 58 if genuine then Unprovable else GaveUp 59 | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut 60 | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) = 61 (case AList.lookup (op =) smt_failures code of 62 SOME failure => failure 63 | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code)) 64 | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources 65 | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s 66 67(* FUDGE *) 68val smt_max_slices = Attrib.setup_config_int \<^binding>\<open>sledgehammer_smt_max_slices\<close> (K 8) 69val smt_slice_fact_frac = 70 Attrib.setup_config_real \<^binding>\<open>sledgehammer_smt_slice_fact_frac\<close> (K 0.667) 71val smt_slice_time_frac = 72 Attrib.setup_config_real \<^binding>\<open>sledgehammer_smt_slice_time_frac\<close> (K 0.333) 73val smt_slice_min_secs = Attrib.setup_config_int \<^binding>\<open>sledgehammer_smt_slice_min_secs\<close> (K 3) 74 75val is_boring_builtin_typ = 76 not o exists_subtype (member (op =) [\<^typ>\<open>nat\<close>, \<^typ>\<open>int\<close>, HOLogic.realT]) 77 78fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice, 79 ...} : params) state goal i = 80 let 81 fun repair_context ctxt = 82 ctxt |> Context.proof_map (SMT_Config.select_solver name) 83 |> Config.put SMT_Config.verbose debug 84 |> (if overlord then 85 Config.put SMT_Config.debug_files 86 (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name)) 87 else 88 I) 89 |> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers) 90 |> not (Config.get ctxt smt_builtins) 91 ? (SMT_Builtin.filter_builtins is_boring_builtin_typ 92 #> Config.put SMT_Systems.z3_extensions false) 93 |> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances 94 default_max_new_mono_instances 95 96 val state = Proof.map_context (repair_context) state 97 val ctxt = Proof.context_of state 98 val max_slices = if slice then Config.get ctxt smt_max_slices else 1 99 100 fun do_slice timeout slice outcome0 time_so_far (factss as (fact_filter, facts) :: _) = 101 let 102 val timer = Timer.startRealTimer () 103 val slice_timeout = 104 if slice < max_slices then 105 let val ms = Time.toMilliseconds timeout in 106 Int.min (ms, Int.max (1000 * Config.get ctxt smt_slice_min_secs, 107 Real.ceil (Config.get ctxt smt_slice_time_frac * Real.fromInt ms))) 108 |> Time.fromMilliseconds 109 end 110 else 111 timeout 112 val num_facts = length facts 113 val _ = 114 if debug then 115 quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^ 116 " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout 117 |> writeln 118 else 119 () 120 val birth = Timer.checkRealTimer timer 121 122 val filter_result as {outcome, ...} = 123 SMT_Solver.smt_filter ctxt goal facts i slice_timeout 124 handle exn => 125 if Exn.is_interrupt exn orelse debug then 126 Exn.reraise exn 127 else 128 {outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)), 129 fact_ids = NONE, atp_proof = K []} 130 131 val death = Timer.checkRealTimer timer 132 val outcome0 = if is_none outcome0 then SOME outcome else outcome0 133 val time_so_far = time_so_far + (death - birth) 134 val timeout = timeout - Timer.checkRealTimer timer 135 136 val too_many_facts_perhaps = 137 (case outcome of 138 NONE => false 139 | SOME (SMT_Failure.Counterexample _) => false 140 | SOME SMT_Failure.Time_Out => slice_timeout <> timeout 141 | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *) 142 | SOME SMT_Failure.Out_Of_Memory => true 143 | SOME (SMT_Failure.Other_Failure _) => true) 144 in 145 if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso 146 timeout > Time.zeroTime then 147 let 148 val new_num_facts = 149 Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts) 150 val factss as (new_fact_filter, _) :: _ = 151 factss 152 |> (fn (x :: xs) => xs @ [x]) 153 |> app_hd (apsnd (take new_num_facts)) 154 val show_filter = fact_filter <> new_fact_filter 155 156 fun num_of_facts fact_filter num_facts = 157 string_of_int num_facts ^ (if show_filter then " " ^ quote fact_filter else "") ^ 158 " fact" ^ plural_s num_facts 159 160 val _ = 161 if debug then 162 quote name ^ " invoked with " ^ 163 num_of_facts fact_filter num_facts ^ ": " ^ 164 string_of_atp_failure (failure_of_smt_failure (the outcome)) ^ 165 " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^ 166 "..." 167 |> writeln 168 else 169 () 170 in 171 do_slice timeout (slice + 1) outcome0 time_so_far factss 172 end 173 else 174 {outcome = if is_none outcome then NONE else the outcome0, filter_result = filter_result, 175 used_from = facts, run_time = time_so_far} 176 end 177 in 178 do_slice timeout 1 NONE Time.zeroTime 179 end 180 181fun run_smt_solver mode name (params as {debug, verbose, isar_proofs, compress, try0, smt_proofs, 182 minimize, preplay_timeout, ...}) 183 ({state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) = 184 let 185 val thy = Proof.theory_of state 186 val ctxt = Proof.context_of state 187 188 val factss = map (apsnd (map (apsnd (Thm.transfer thy)))) factss 189 190 val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} = 191 smt_filter_loop name params state goal subgoal factss 192 val used_facts = 193 (case fact_ids of 194 NONE => map fst used_from 195 | SOME ids => sort_by fst (map (fst o snd) ids)) 196 val outcome = Option.map failure_of_smt_failure outcome 197 198 val (preferred_methss, message) = 199 (case outcome of 200 NONE => 201 let 202 val _ = found_proof (); 203 val smt_method = smt_proofs <> SOME false 204 val preferred_methss = 205 (if smt_method then SMT_Method else Metis_Method (NONE, NONE), 206 bunches_of_proof_methods try0 smt_method false liftingN) 207 in 208 (preferred_methss, 209 fn preplay => 210 let 211 val _ = if verbose then writeln "Generating proof text..." else () 212 213 fun isar_params () = 214 (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (), 215 goal) 216 217 val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count) 218 val num_chained = length (#facts (Proof.goal state)) 219 in 220 proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained 221 one_line_params 222 end) 223 end 224 | SOME failure => ((Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)) 225 in 226 {outcome = outcome, used_facts = used_facts, used_from = used_from, 227 preferred_methss = preferred_methss, run_time = run_time, message = message} 228 end 229 230end; 231